MAT3253 Complex Variables

1.1. Construction🔗

We construct complex numbers as pairs (x, y) of rational numbers. In effect, this extends the rational number system by adjoining a distinguished element i, represented by (0, 1). Working over the rationals allows us to carry out explicit operations and calculations.

Mathlib provides the standard construction of the complex number system using real numbers as coordinates. The development there follows the same conceptual steps as the construction presented below.

@[ext] structure complexQ where
  re : ℚ   -- real part
  im : ℚ   -- imaginary part
 deriving Repr

notation "ℚ[i]" => complexQ

-- Display a complex number as x+y*I
unsafe instance instRepr : Repr complexQ where
  reprPrec z _  :=
    reprPrec z.re 20 ++ " + " ++ reprPrec z.im 20 ++ "*I"


-- examples of constructors

-- complex number -2+4i
def sample1 := complexQ.mk (-2) (2/3)

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

-- complex number -3i
def sample2 : complexQ where
  re := 0
  im := (-3)

def sample3 : complexQ := ⟨0, -3⟩    -- complex number 0-3i

def sample4 : ℚ[i] :=   -- complex 1.5 + (3/2)i
{
 re := 1.5
 im := 3/2
}

-2 + (2 : Rat)/3*I#eval sample1   -- -2 + (2 : Rat)/3*I
0 + -3*I#eval sample2   -- 0 + -3*I
0 + -3*I#eval sample3   -- 0 + -3*I
(3 : Rat)/2 + (3 : Rat)/2*I#eval sample4   -- (3 : Rat)/2 + (3 : Rat)/2*I


-- Two complex numbers are equal if and only if the real and
-- imaginary parts are the same
example : sample2 = sample3 := by⊢ sample2 = sample3 rflAll goals completed! 🐙

-- #eval sample2 = sample3   -- no meaning at this point

def sample5 : ℚ := (complexQ.mk 2 4).re
  -- this term is the rational number 2

2#eval sample5   -- 2

-- The real part of 2+4i is equal to 2
example :  (complexQ.mk 2 4).re = 2 := rfl

-- The imaginary part of 2+4i is equal to 4
example :  (complexQ.mk 2 4).im = 4 := rfl


-- Two complex numbers are the same
-- iff the real and imaginary parts are the same
lemma ext_iff {z w : ℚ[i]}
  : z = w ↔ z.re = w.re ∧ z.im = w.im
  := byz:ℚ[i]w:ℚ[i]⊢ z = w ↔ z.re = w.re ∧ z.im = w.im
  constructormpz:ℚ[i]w:ℚ[i]⊢ z = w → z.re = w.re ∧ z.im = w.immprz:ℚ[i]w:ℚ[i]⊢ z.re = w.re ∧ z.im = w.im → z = w
  ·mpz:ℚ[i]w:ℚ[i]⊢ z = w → z.re = w.re ∧ z.im = w.im intro hmpz:ℚ[i]w:ℚ[i]h:z = w⊢ z.re = w.re ∧ z.im = w.im
    simp [h]All goals completed! 🐙
  ·mprz:ℚ[i]w:ℚ[i]⊢ z.re = w.re ∧ z.im = w.im → z = w intro ⟨h1, h2⟩mprz:ℚ[i]w:ℚ[i]h1:z.re = w.reh2:z.im = w.im⊢ z = w
    extmpr.rez:ℚ[i]w:ℚ[i]h1:z.re = w.reh2:z.im = w.im⊢ z.re = w.rempr.imz:ℚ[i]w:ℚ[i]h1:z.re = w.reh2:z.im = w.im⊢ z.im = w.im
    ·mpr.rez:ℚ[i]w:ℚ[i]h1:z.re = w.reh2:z.im = w.im⊢ z.re = w.re exact h1All goals completed! 🐙
    ·mpr.imz:ℚ[i]w:ℚ[i]h1:z.re = w.reh2:z.im = w.im⊢ z.im = w.im exact h2All goals completed! 🐙

/-
 special elements in complexQ
-/

-- Define the numeral 0 explicitly
instance : OfNat complexQ 0 where
  ofNat := ⟨0, 0⟩

-- Define the numeral 1 explicitly
instance : OfNat complexQ 1 where
  ofNat := ⟨1, 0⟩

-- the complex number 0
def zero : ℚ[i] := ⟨0,0⟩

-- the complex number 0
def one : ℚ[i] := ⟨1,0⟩

-- the complex number i
def I : ℚ[i] := ⟨0,1⟩

-- ⟨0,0⟩ is the zero element
instance : Zero ℚ[i] := ⟨zero⟩

-- ⟨1,0⟩ is the unit
instance : One ℚ[i] := ⟨one⟩


0 + 0*I#eval zero
1 + 0*I#eval one
0 + 1*I#eval I