1.7. Involution
Conjugation in ℚ[i] is the ring endomorphism in a StarRing
instance : StarRing ℚ[i] where
star z := ⟨z.re, -z.im⟩
star_involutive x := x:ℚ[i]⊢ (fun z => { re := z.re, im := -z.im }) ((fun z => { re := z.re, im := -z.im }) x) = x All goals completed! 🐙
star_mul a b := a:ℚ[i]b:ℚ[i]⊢ { re := (a * b).re, im := -(a * b).im } = { re := b.re, im := -b.im } * { re := a.re, im := -a.im } a:ℚ[i]b:ℚ[i]⊢ { re := (a * b).re, im := -(a * b).im }.re = ({ re := b.re, im := -b.im } * { re := a.re, im := -a.im }).rea:ℚ[i]b:ℚ[i]⊢ { re := (a * b).re, im := -(a * b).im }.im = ({ re := b.re, im := -b.im } * { re := a.re, im := -a.im }).im a:ℚ[i]b:ℚ[i]⊢ { re := (a * b).re, im := -(a * b).im }.re = ({ re := b.re, im := -b.im } * { re := a.re, im := -a.im }).rea:ℚ[i]b:ℚ[i]⊢ { re := (a * b).re, im := -(a * b).im }.im = ({ re := b.re, im := -b.im } * { re := a.re, im := -a.im }).im a:ℚ[i]b:ℚ[i]⊢ -(a.re * b.im) + -(a.im * b.re) = -(b.re * a.im) + -(b.im * a.re) a:ℚ[i]b:ℚ[i]⊢ a.re * b.re - a.im * b.im = b.re * a.re - b.im * a.ima:ℚ[i]b:ℚ[i]⊢ -(a.re * b.im) + -(a.im * b.re) = -(b.re * a.im) + -(b.im * a.re) All goals completed! 🐙
star_add a b := a:ℚ[i]b:ℚ[i]⊢ { re := (a + b).re, im := -(a + b).im } = { re := a.re, im := -a.im } + { re := b.re, im := -b.im } a:ℚ[i]b:ℚ[i]⊢ { re := (a + b).re, im := -(a + b).im }.re = ({ re := a.re, im := -a.im } + { re := b.re, im := -b.im }).rea:ℚ[i]b:ℚ[i]⊢ { re := (a + b).re, im := -(a + b).im }.im = ({ re := a.re, im := -a.im } + { re := b.re, im := -b.im }).im a:ℚ[i]b:ℚ[i]⊢ { re := (a + b).re, im := -(a + b).im }.re = ({ re := a.re, im := -a.im } + { re := b.re, im := -b.im }).rea:ℚ[i]b:ℚ[i]⊢ { re := (a + b).re, im := -(a + b).im }.im = ({ re := a.re, im := -a.im } + { re := b.re, im := -b.im }).im All goals completed! 🐙
-- One we have set up ℚ[i] as a StarRing,
-- the conjugation function `starRingEnd ℚ[i]`
-- can be invoked by `conj` in the
-- namespace `ComplexConjugate`
open ComplexConjugate
-- notation "conj" => (starRingEnd ℂ)
@[simp]
lemma conj_re (z : ℚ[i]) : (conj z).re = z.re := rfl
@[simp]
lemma conj_im (z : ℚ[i]) : (conj z).im = -z.im := rfl
theorem conj_ofReal (r : ℚ) : conj (r : ℚ[i]) = r :=
ext_iff.mpr <| r:ℚ⊢ ((starRingEnd ℚ[i]) ↑r).re = (↑r).re ∧ ((starRingEnd ℚ[i]) ↑r).im = (↑r).im All goals completed! 🐙
@[simp]
lemma conj_I : conj I = -I := ⊢ (starRingEnd ℚ[i]) I = -I
All goals completed! 🐙
theorem conj_natCast (n : ℕ) :
conj (n : ℚ[i]) = n := map_natCast _ _
theorem conj_ofNat (n : ℕ) [n.AtLeastTwo]
: conj (no_index (OfNat.ofNat n : ℚ[i]))
= OfNat.ofNat n :=
map_ofNat _ _
theorem conj_neg_I : conj (-I) = I :=
ext_iff.2 <| ⊢ ((starRingEnd ℚ[i]) (-I)).re = I.re ∧ ((starRingEnd ℚ[i]) (-I)).im = I.im All goals completed! 🐙
theorem conj_eq_iff_real {z : ℚ[i]}
: conj z = z ↔ ∃ r : ℚ, z = r :=
⟨fun h => ⟨z.re, ext rfl <|
eq_zero_of_neg_eq
(congr_arg (fun z:ℚ[i]=> z.im) h)⟩, fun ⟨h, e⟩ => z:ℚ[i]x✝:∃ r, z = ↑rh:ℚe:z = ↑h⊢ (starRingEnd ℚ[i]) z = z
All goals completed! 🐙⟩
@[simp]
theorem star_def : (Star.star : ℂ → ℂ) = conj :=
rfl