From c48c769c3e1d68c84f814c1a9f060c493336c817 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Fri, 8 Sep 2023 11:01:40 +0000 Subject: [PATCH] feat: flesh out the API for `realPart` and `imaginaryPart` (#7023) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Improve API for the `realPart` and `imaginaryPart` maps in a star module over `ℂ`. 1. remove the `simp` attribute on `realPart_apply_coe` and `imaginaryPart_apply_coe` 2. construct the `ℝ`-linear equivalence `Complex.selfAdjointEquiv` between `selfAdjoint ℂ` and `ℝ`. In fact, this would be an algebra equivalence, but that requires `selfAdjoint ℂ` to have an `algebra ℝ (selfAdjoint ℂ)` structure, which it doesn't have. 3. show the span (over `ℂ`) of `selfAdjoint A` is `⊤ : Submodule ℂ A` --- Mathlib/Data/Complex/Module.lean | 101 ++++++++++++++++++++++++++++--- 1 file changed, 91 insertions(+), 10 deletions(-) diff --git a/Mathlib/Data/Complex/Module.lean b/Mathlib/Data/Complex/Module.lean index 0dcc0342cb6db..495727a8d94b8 100644 --- a/Mathlib/Data/Complex/Module.lean +++ b/Mathlib/Data/Complex/Module.lean @@ -410,18 +410,18 @@ noncomputable def imaginaryPart : A →ₗ[ℝ] selfAdjoint A := skewAdjoint.negISMul.comp (skewAdjointPart ℝ) #align imaginary_part imaginaryPart +@[inherit_doc] scoped[ComplexStarModule] notation "ℜ" => realPart +@[inherit_doc] scoped[ComplexStarModule] notation "ℑ" => imaginaryPart open ComplexStarModule -@[simp] theorem realPart_apply_coe (a : A) : (ℜ a : A) = (2 : ℝ)⁻¹ • (a + star a) := by unfold realPart simp only [selfAdjointPart_apply_coe, invOf_eq_inv] #align real_part_apply_coe realPart_apply_coe -@[simp] theorem imaginaryPart_apply_coe (a : A) : (ℑ a : A) = -I • (2 : ℝ)⁻¹ • (a - star a) := by unfold imaginaryPart simp only [LinearMap.coe_comp, Function.comp_apply, skewAdjoint.negISMul_apply_coe, @@ -458,19 +458,100 @@ set_option linter.uppercaseLean3 false in #align imaginary_part_I_smul imaginaryPart_I_smul theorem realPart_smul (z : ℂ) (a : A) : ℜ (z • a) = z.re • ℜ a - z.im • ℑ a := by - -- Porting note: was `nth_rw 1 [← re_add_im z]` - conv_lhs => - rw [← re_add_im z] - simp [-re_add_im, add_smul, ← smul_smul, sub_eq_add_neg] + have := by congrm(ℜ ($((re_add_im z).symm) • a)) + simpa [-re_add_im, add_smul, ← smul_smul, sub_eq_add_neg] #align real_part_smul realPart_smul theorem imaginaryPart_smul (z : ℂ) (a : A) : ℑ (z • a) = z.re • ℑ a + z.im • ℜ a := by - -- Porting note: was `nth_rw 1 [← re_add_im z]` - conv_lhs => - rw [← re_add_im z] - simp [-re_add_im, add_smul, ← smul_smul] + have := by congrm(ℑ ($((re_add_im z).symm) • a)) + simpa [-re_add_im, add_smul, ← smul_smul] #align imaginary_part_smul imaginaryPart_smul +lemma skewAdjointPart_eq_I_smul_imaginaryPart (x : A) : + (skewAdjointPart ℝ x : A) = I • (imaginaryPart x : A) := by + simp [imaginaryPart_apply_coe, smul_smul] + +lemma imaginaryPart_eq_neg_I_smul_skewAdjointPart (x : A) : + (imaginaryPart x : A) = -I • (skewAdjointPart ℝ x : A) := + rfl + +lemma IsSelfAdjoint.coe_realPart {x : A} (hx : IsSelfAdjoint x) : + (ℜ x : A) = x := + hx.coe_selfAdjointPart_apply ℝ + +lemma IsSelfAdjoint.imaginaryPart {x : A} (hx : IsSelfAdjoint x) : + ℑ x = 0 := by + rw [imaginaryPart, LinearMap.comp_apply, hx.skewAdjointPart_apply _, map_zero] + +lemma realPart_comp_subtype_selfAdjoint : + realPart.comp (selfAdjoint.submodule ℝ A).subtype = LinearMap.id := + selfAdjointPart_comp_subtype_selfAdjoint ℝ + +lemma imaginaryPart_comp_subtype_selfAdjoint : + imaginaryPart.comp (selfAdjoint.submodule ℝ A).subtype = 0 := by + rw [imaginaryPart, LinearMap.comp_assoc, skewAdjointPart_comp_subtype_selfAdjoint, + LinearMap.comp_zero] + +@[simp] +lemma imaginaryPart_realPart {x : A} : ℑ (ℜ x : A) = 0 := + (ℜ x).property.imaginaryPart + +@[simp] +lemma imaginaryPart_imaginaryPart {x : A} : ℑ (ℑ x : A) = 0 := + (ℑ x).property.imaginaryPart + +@[simp] +lemma realPart_idem {x : A} : ℜ (ℜ x : A) = ℜ x := + Subtype.ext <| (ℜ x).property.coe_realPart + +@[simp] +lemma realPart_imaginaryPart {x : A} : ℜ (ℑ x : A) = ℑ x := + Subtype.ext <| (ℑ x).property.coe_realPart + +lemma realPart_surjective : Function.Surjective (realPart (A := A)) := + fun x ↦ ⟨(x : A), Subtype.ext x.property.coe_realPart⟩ + +lemma imaginaryPart_surjective : Function.Surjective (imaginaryPart (A := A)) := + fun x ↦ + ⟨I • (x : A), Subtype.ext <| by simp only [imaginaryPart_I_smul, x.property.coe_realPart]⟩ + +open Submodule + +lemma span_selfAdjoint : span ℂ (selfAdjoint A : Set A) = ⊤ := by + refine eq_top_iff'.mpr fun x ↦ ?_ + rw [←realPart_add_I_smul_imaginaryPart x] + exact add_mem (subset_span (ℜ x).property) <| + SMulMemClass.smul_mem _ <| subset_span (ℑ x).property + +/-- The natural `ℝ`-linear equivalence between `selfAdjoint ℂ` and `ℝ`. -/ +@[simps apply symm_apply] +def Complex.selfAdjointEquiv : selfAdjoint ℂ ≃ₗ[ℝ] ℝ where + toFun := fun z ↦ (z : ℂ).re + invFun := fun x ↦ ⟨x, conj_ofReal x⟩ + left_inv := fun z ↦ Subtype.ext <| conj_eq_iff_re.mp z.property.star_eq + right_inv := fun x ↦ rfl + map_add' := by simp + map_smul' := by simp + +lemma Complex.coe_selfAdjointEquiv (z : selfAdjoint ℂ) : + (selfAdjointEquiv z : ℂ) = z := by + simpa [selfAdjointEquiv_symm_apply] + using (congr_arg Subtype.val <| Complex.selfAdjointEquiv.left_inv z) + +@[simp] +lemma realPart_ofReal (r : ℝ) : (ℜ (r : ℂ) : ℂ) = r := by + rw [realPart_apply_coe, star_def, conj_ofReal, ←two_smul ℝ (r : ℂ)] + simp + +@[simp] +lemma imaginaryPart_ofReal (r : ℝ) : ℑ (r : ℂ) = 0 := by + ext1; simp [imaginaryPart_apply_coe, conj_ofReal] + +lemma Complex.coe_realPart (z : ℂ) : (ℜ z : ℂ) = z.re := calc + (ℜ z : ℂ) = _ := by congrm(ℜ $((re_add_im z).symm)) + _ = z.re := by + rw [map_add, AddSubmonoid.coe_add, mul_comm, ←smul_eq_mul, realPart_I_smul] + simp [conj_ofReal, ←two_mul] end RealImaginaryPart section Rational