MAT3253 Complex Variables

1.3. Coercion🔗

Every rational number can be regarded as a number in ℚ[i] Rational number r is identified with the complex number ⟨r,0⟩
@[coe]
def ofRational (r: ℚ) : ℚ[i] := ⟨r,0⟩

instance : Coe ℚ ℚ[i] := ⟨ofRational⟩

1 + (2 : Rat)/3*I#eval sample1 + (3 : ℚ)


def sample6 := complexQ.mk 5 0

--The complex number 5+0i is the same as rational number 5
example : sample6 = (5:ℚ) := by⊢ sample6 = ↑5 rflAll goals completed! 🐙


@[simp, norm_cast]
lemma ofRational_re (r: ℚ)  : (r:ℚ[i]).re = r := rfl

@[simp, norm_cast]
lemma ofRational_im (r: ℚ)  : (r:ℚ[i]).im = 0 := rfl

@[simp, norm_cast]
lemma ofRational_inj {r s : ℚ} :
   (r : ℚ[i]) = s ↔ r = s := byr:ℚs:ℚ⊢ ↑r = ↑s ↔ r = s
  constructormpr:ℚs:ℚ⊢ ↑r = ↑s → r = smprr:ℚs:ℚ⊢ r = s → ↑r = ↑s
  ·mpr:ℚs:ℚ⊢ ↑r = ↑s → r = s intro hmpr:ℚs:ℚh:↑r = ↑s⊢ r = s
    have h1: (ofRational r).re = (ofRational s).re := byr:ℚs:ℚ⊢ ↑r = ↑s ↔ r = s
      congrAll goals completed! 🐙
    rw [ofRational_re r] at h1mpr:ℚs:ℚh:↑r = ↑sh1:r = (↑s).re⊢ r = s
    rw [ofRational_re s] at h1mpr:ℚs:ℚh:↑r = ↑sh1:r = s⊢ r = s
    exact h1All goals completed! 🐙
  ·mprr:ℚs:ℚ⊢ r = s → ↑r = ↑s intro hmprr:ℚs:ℚh:r = s⊢ ↑r = ↑s
    congrAll goals completed! 🐙

@[simp]
lemma ofRational_def (r:ℚ) :
  (complexQ.mk r 0) = (r:ℚ[i]) := byr:ℚ⊢ { re := r, im := 0 } = ↑r
  rflAll goals completed! 🐙

@[simp]
lemma rational_eq_coe' (r:ℚ) : r = (r : ℚ[i]) := byr:ℚ⊢ ↑r = ↑r rflAll goals completed! 🐙


example (r s : ℚ) (h: (r:ℚ[i])=s) : r = s := byr:ℚs:ℚh:↑r = ↑s⊢ r = s
  exact ofRational_inj.mp hAll goals completed! 🐙

@[simp, norm_cast]
lemma ofRational_zero : ((0:ℚ) : ℚ[i]) = 0 := rfl


@[simp]
lemma ofRational_eq_zero {z:ℚ} : (z:ℚ[i]) = 0 ↔ z=0 :=
  ofRational_inj

lemma ofRational_ne_zero {z:ℚ} : (z:ℚ[i])≠ 0 ↔ z≠0 :=
  not_congr ofRational_eq_zero

@[simp]
lemma ofRational_eq_one {z:ℚ} : (z:ℚ[i]) = 1 ↔ z=1 :=
  ofRational_inj

lemma ofRational_ne_one {z:ℚ} : (z:ℚ[i]) ≠ 1 ↔ z ≠ 1 :=
  not_congr ofRational_eq_one

@[simp, norm_cast]
theorem ofRational_neg (r : ℚ) : ((-r : ℚ) : ℚ[i]) = -r
  := byr:ℚ⊢ ↑(-r) = -↑r
  apply ext_iff.mprr:ℚ⊢ (↑(-r)).re = (-↑r).re ∧ (↑(-r)).im = (-↑r).im
  simpAll goals completed! 🐙



lemma ofRational_add (r s : ℚ) : ( (r+s :ℚ) : ℚ[i]) = r+s
  := byr:ℚs:ℚ⊢ ↑(r + s) = ↑r + ↑s
  refine ext_iff.2 ?_r:ℚs:ℚ⊢ (↑(r + s)).re = (↑r + ↑s).re ∧ (↑(r + s)).im = (↑r + ↑s).im
  constructorleftr:ℚs:ℚ⊢ (↑(r + s)).re = (↑r + ↑s).rerightr:ℚs:ℚ⊢ (↑(r + s)).im = (↑r + ↑s).im
  ·leftr:ℚs:ℚ⊢ (↑(r + s)).re = (↑r + ↑s).re simp [ofRational_re]All goals completed! 🐙
  ·rightr:ℚs:ℚ⊢ (↑(r + s)).im = (↑r + ↑s).im simp [ofRational_im]All goals completed! 🐙

@[simp, norm_cast]
theorem ofRational_mul (r s : ℚ) :
    ((r * s : ℚ) : ℚ[i]) = r * s := byr:ℚs:ℚ⊢ ↑(r * s) = ↑r * ↑s
  apply ext_iff.mprr:ℚs:ℚ⊢ (↑(r * s)).re = (↑r * ↑s).re ∧ (↑(r * s)).im = (↑r * ↑s).im
  constructorleftr:ℚs:ℚ⊢ (↑(r * s)).re = (↑r * ↑s).rerightr:ℚs:ℚ⊢ (↑(r * s)).im = (↑r * ↑s).im
  repeat dsimprightr:ℚs:ℚ⊢ 0 = r * 0 + 0 * s <;>rightr:ℚs:ℚ⊢ 0 = r * 0 + 0 * s
  simp [mul_zero, sub_zero]All goals completed! 🐙

theorem re_ofRational_mul (r : ℚ) (z : ℚ[i])
  : (r * z).re = r * z.re := byr:ℚz:ℚ[i]⊢ (↑r * z).re = r * z.re
  dsimpr:ℚz:ℚ[i]⊢ r * z.re - 0 * z.im = r * z.re
  simp only [zero_mul, sub_zero]All goals completed! 🐙

theorem im_ofRational_mul (r : ℚ) (z : ℚ[i])
  : (r * z).im = r * z.im := byr:ℚz:ℚ[i]⊢ (↑r * z).im = r * z.im
  dsimpr:ℚz:ℚ[i]⊢ r * z.im + 0 * z.re = r * z.im
  simp only [zero_mul, add_zero]All goals completed! 🐙

lemma re_mul_ofRational (z : ℚ[i]) (r : ℚ)
  : (z * r).re = z.re *  r := byz:ℚ[i]r:ℚ⊢ (z * ↑r).re = z.re * r
  dsimpz:ℚ[i]r:ℚ⊢ z.re * r - z.im * 0 = z.re * r; simp only [mul_zero, sub_zero]All goals completed! 🐙

lemma im_mul_ofRational (z : ℚ[i]) (r : ℚ)
  : (z * r).im = z.im *  r := byz:ℚ[i]r:ℚ⊢ (z * ↑r).im = z.im * r
  dsimpz:ℚ[i]r:ℚ⊢ z.re * 0 + z.im * r = z.im * r; simp only [mul_zero, zero_add]All goals completed! 🐙

@[simp]
theorem ofRational_mul' (r : ℚ) (z : ℚ[i])
  : ↑r * z = ⟨r * z.re, r * z.im⟩ :=
  ext (re_ofRational_mul _ _) (im_ofRational_mul _ _)

theorem mk_eq_add_mul_I (a b : ℚ)
  : (complexQ.mk a b) = a + b * I :=
  ext_iff.2 <| bya:ℚb:ℚ⊢ { re := a, im := b }.re = (↑a + ↑b * I).re ∧ { re := a, im := b }.im = (↑a + ↑b * I).im dsimpa:ℚb:ℚ⊢ a = a + (b * 0 - 0 * 1) ∧ b = 0 + (b * 1 + 0 * 0) ; simp only
    [mul_zero, mul_one, sub_self,
    add_zero, zero_add, and_self]All goals completed! 🐙

@[simp]
theorem re_add_im (z : ℚ[i])
  : (z.re : ℚ[i]) + z.im * I = z :=
  ext_iff.2 <| byz:ℚ[i]⊢ (↑z.re + ↑z.im * I).re = z.re ∧ (↑z.re + ↑z.im * I).im = z.im
    dsimpz:ℚ[i]⊢ z.re + (z.im * 0 - 0 * 1) = z.re ∧ 0 + (z.im * 1 + 0 * 0) = z.im;
    simp only [mul_zero, mul_one, sub_self,
      add_zero, zero_add, and_self]All goals completed! 🐙

theorem mul_I_re (z : ℚ[i])
  : (z * I).re = -z.im := byz:ℚ[i]⊢ (z * I).re = -z.im simpAll goals completed! 🐙

theorem mul_I_im (z : ℚ[i])
  : (z * I).im = z.re := byz:ℚ[i]⊢ (z * I).im = z.re simpAll goals completed! 🐙

theorem I_mul_re (z : ℚ[i])
  : (I * z).re = -z.im := byz:ℚ[i]⊢ (I * z).re = -z.im simpAll goals completed! 🐙

theorem I_mul_im (z : ℚ[i])
  : (I * z).im = z.re := byz:ℚ[i]⊢ (I * z).im = z.re simpAll goals completed! 🐙


-- Prove that 0 ≠ 1 in ℚ[i]
instance : Nontrivial ℚ[i] := by⊢ Nontrivial ℚ[i]
  use 0, 1h⊢ 0 ≠ 1
  refine (ofRational_ne_one).mpr ?_h⊢ 0 ≠ 1
  norm_numAll goals completed! 🐙