feat(NumberField/CanonicalEmbedding): make the mixedSpace explicit (#16634)

For `K`, a number field, the mixed space is the space `ℝ^r₁ × ℂ^r₂` where `(r₁, r₂)` is the signature of `K`. This space is heavily used in the files about the canonical embedding but was never explicit (only used a notation). 

For further developments (and just to make things clearer), I think it is better to define it explicitly. This is what is done in this PR.

Author: xroblot

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

@@ -24,11 +24,11 @@ sending `x : K` to the vector `(φ x)` indexed by `φ : K →+* ℂ`.
 image of the ring of integers by the canonical embedding and any ball centered at `0` of finite
 radius is finite.
 
-* `NumberField.mixedEmbedding`: the ring homomorphism from `K →+* ({ w // IsReal w } → ℝ) ×
-({ w // IsComplex w } → ℂ)` that sends `x ∈ K` to `(φ_w x)_w` where `φ_w` is the embedding
-associated to the infinite place `w`. In particular, if `w` is real then `φ_w : K →+* ℝ` and, if
-`w` is complex, `φ_w` is an arbitrary choice between the two complex embeddings defining the place
-`w`.
+* `NumberField.mixedEmbedding`: the ring homomorphism from `K` to the mixed space
+`K →+* ({ w // IsReal w } → ℝ) × ({ w // IsComplex w } → ℂ)` that sends `x ∈ K` to `(φ_w x)_w`
+where `φ_w` is the embedding associated to the infinite place `w`. In particular, if `w` is real
+then `φ_w : K →+* ℝ` and, if `w` is complex, `φ_w` is an arbitrary choice between the two complex
+embeddings defining the place `w`.
 
 ## Tags
 
@@ -39,8 +39,6 @@ variable (K : Type*) [Field K]
 
 namespace NumberField.canonicalEmbedding
 
---open NumberField
-
 /-- The canonical embedding of a number field `K` of degree `n` into `ℂ^n`. -/
 def _root_.NumberField.canonicalEmbedding : K →+* ((K →+* ℂ) → ℂ) := Pi.ringHom fun φ => φ
 
@@ -180,24 +178,24 @@ namespace NumberField.mixedEmbedding
 
 open NumberField.InfinitePlace FiniteDimensional Finset
 
-/-- The space `ℝ^r₁ × ℂ^r₂` with `(r₁, r₂)` the signature of `K`. -/
-local notation "E" K =>
+/-- The mixed space `ℝ^r₁ × ℂ^r₂` with `(r₁, r₂)` the signature of `K`. -/
+abbrev mixedSpace :=
   ({w : InfinitePlace K // IsReal w} → ℝ) × ({w : InfinitePlace K // IsComplex w} → ℂ)
 
-/-- The mixed embedding of a number field `K` of signature `(r₁, r₂)` into `ℝ^r₁ × ℂ^r₂`. -/
-noncomputable def _root_.NumberField.mixedEmbedding : K →+* (E K) :=
+/-- The mixed embedding of a number field `K` into the mixed space of `K`. -/
+noncomputable def _root_.NumberField.mixedEmbedding : K →+* (mixedSpace K) :=
   RingHom.prod (Pi.ringHom fun w => embedding_of_isReal w.prop)
     (Pi.ringHom fun w => w.val.embedding)
 
-instance [NumberField K] : Nontrivial (E K) := by
+instance [NumberField K] : Nontrivial (mixedSpace K) := by
   obtain ⟨w⟩ := (inferInstance : Nonempty (InfinitePlace K))
   obtain hw | hw := w.isReal_or_isComplex
   · have : Nonempty {w : InfinitePlace K // IsReal w} := ⟨⟨w, hw⟩⟩
     exact nontrivial_prod_left
   · have : Nonempty {w : InfinitePlace K // IsComplex w} := ⟨⟨w, hw⟩⟩
     exact nontrivial_prod_right
 
-protected theorem finrank [NumberField K] : finrank ℝ (E K) = finrank ℚ K := by
+protected theorem finrank [NumberField K] : finrank ℝ (mixedSpace K) = finrank ℚ K := by
   classical
   rw [finrank_prod, finrank_pi, finrank_pi_fintype, Complex.finrank_real_complex, sum_const,
     card_univ, ← NrRealPlaces, ← NrComplexPlaces, ← card_real_embeddings, Algebra.id.smul_eq_mul,
@@ -212,7 +210,7 @@ section commMap
 
 /-- The linear map that makes `canonicalEmbedding` and `mixedEmbedding` commute, see
 `commMap_canonical_eq_mixed`. -/
-noncomputable def commMap : ((K →+* ℂ) → ℂ) →ₗ[ℝ] (E K) where
+noncomputable def commMap : ((K →+* ℂ) → ℂ) →ₗ[ℝ] (mixedSpace K) where
   toFun := fun x => ⟨fun w => (x w.val.embedding).re, fun w => x w.val.embedding⟩
   map_add' := by
     simp only [Pi.add_apply, Complex.add_re, Prod.mk_add_mk, Prod.mk.injEq]
@@ -236,7 +234,7 @@ theorem commMap_canonical_eq_mixed (x : K) :
   exact ⟨rfl, rfl⟩
 
 /-- This is a technical result to ensure that the image of the `ℂ`-basis of `ℂ^n` defined in
-`canonicalEmbedding.latticeBasis` is a `ℝ`-basis of `ℝ^r₁ × ℂ^r₂`,
+`canonicalEmbedding.latticeBasis` is a `ℝ`-basis of the mixed space `ℝ^r₁ × ℂ^r₂`,
 see `mixedEmbedding.latticeBasis`. -/
 theorem disjoint_span_commMap_ker [NumberField K] :
     Disjoint (Submodule.span ℝ (Set.range (canonicalEmbedding.latticeBasis K)))
@@ -270,46 +268,45 @@ open scoped Classical
 
 variable {K}
 
-/-- The norm at the infinite place `w` of an element of
-`({w // IsReal w} → ℝ) × ({ w // IsComplex w } → ℂ)`. -/
-def normAtPlace (w : InfinitePlace K) : (E K) →*₀ ℝ where
+/-- The norm at the infinite place `w` of an element of the mixed space. --/
+def normAtPlace (w : InfinitePlace K) : (mixedSpace K) →*₀ ℝ where
   toFun x := if hw : IsReal w then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, not_isReal_iff_isComplex.mp hw⟩‖
   map_zero' := by simp
   map_one' := by simp
   map_mul' x y := by split_ifs <;> simp
 
-theorem normAtPlace_nonneg (w : InfinitePlace K) (x : E K) :
+theorem normAtPlace_nonneg (w : InfinitePlace K) (x : mixedSpace K) :
     0 ≤ normAtPlace w x := by
   rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
   split_ifs <;> exact norm_nonneg _
 
-theorem normAtPlace_neg (w : InfinitePlace K) (x : E K)  :
+theorem normAtPlace_neg (w : InfinitePlace K) (x : mixedSpace K)  :
     normAtPlace w (- x) = normAtPlace w x := by
   rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
   split_ifs <;> simp
 
-theorem normAtPlace_add_le (w : InfinitePlace K) (x y : E K) :
+theorem normAtPlace_add_le (w : InfinitePlace K) (x y : mixedSpace K) :
     normAtPlace w (x + y) ≤ normAtPlace w x + normAtPlace w y := by
   rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
   split_ifs <;> exact norm_add_le _ _
 
-theorem normAtPlace_smul (w : InfinitePlace K) (x : E K) (c : ℝ) :
+theorem normAtPlace_smul (w : InfinitePlace K) (x : mixedSpace K) (c : ℝ) :
     normAtPlace w (c • x) = |c| * normAtPlace w x := by
   rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
   split_ifs
   · rw [Prod.smul_fst, Pi.smul_apply, norm_smul, Real.norm_eq_abs]
   · rw [Prod.smul_snd, Pi.smul_apply, norm_smul, Real.norm_eq_abs, Complex.norm_eq_abs]
 
 theorem normAtPlace_real (w : InfinitePlace K) (c : ℝ) :
-    normAtPlace w ((fun _ ↦ c, fun _ ↦ c) : (E K)) = |c| := by
-  rw [show ((fun _ ↦ c, fun _ ↦ c) : (E K)) = c • 1 by ext <;> simp, normAtPlace_smul, map_one,
-    mul_one]
+    normAtPlace w ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = |c| := by
+  rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, normAtPlace_smul,
+    map_one, mul_one]
 
-theorem normAtPlace_apply_isReal {w : InfinitePlace K} (hw : IsReal w) (x : E K) :
+theorem normAtPlace_apply_isReal {w : InfinitePlace K} (hw : IsReal w) (x : mixedSpace K) :
     normAtPlace w x = ‖x.1 ⟨w, hw⟩‖ := by
   rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, dif_pos]
 
-theorem normAtPlace_apply_isComplex {w : InfinitePlace K} (hw : IsComplex w) (x : E K) :
+theorem normAtPlace_apply_isComplex {w : InfinitePlace K} (hw : IsComplex w) (x : mixedSpace K) :
     normAtPlace w x = ‖x.2 ⟨w, hw⟩‖ := by
   rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk,
     dif_neg (not_isReal_iff_isComplex.mpr hw)]
@@ -321,7 +318,7 @@ theorem normAtPlace_apply (w : InfinitePlace K) (x : K) :
     RingHom.prod_apply, Pi.ringHom_apply, norm_embedding_of_isReal, norm_embedding_eq, dite_eq_ite,
     ite_id]
 
-theorem normAtPlace_eq_zero {x : E K} :
+theorem normAtPlace_eq_zero {x : mixedSpace K} :
     (∀ w, normAtPlace w x = 0) ↔ x = 0 := by
   refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
   · ext w
@@ -331,7 +328,7 @@ theorem normAtPlace_eq_zero {x : E K} :
 
 variable [NumberField K]
 
-theorem nnnorm_eq_sup_normAtPlace (x : E K) :
+theorem nnnorm_eq_sup_normAtPlace (x : mixedSpace K) :
     ‖x‖₊ = univ.sup fun w ↦ ⟨normAtPlace w x, normAtPlace_nonneg w x⟩ := by
   have :
       (univ : Finset (InfinitePlace K)) =
@@ -346,7 +343,7 @@ theorem nnnorm_eq_sup_normAtPlace (x : E K) :
   · ext w
     simp [normAtPlace_apply_isComplex w.prop]
 
-theorem norm_eq_sup'_normAtPlace (x : E K) :
+theorem norm_eq_sup'_normAtPlace (x : mixedSpace K) :
     ‖x‖ = univ.sup' univ_nonempty fun w ↦ normAtPlace w x := by
   rw [← coe_nnnorm, nnnorm_eq_sup_normAtPlace, ← sup'_eq_sup univ_nonempty, ← NNReal.val_eq_coe,
     ← OrderHom.Subtype.val_coe, map_finset_sup', OrderHom.Subtype.val_coe]
@@ -355,43 +352,44 @@ theorem norm_eq_sup'_normAtPlace (x : E K) :
 /-- The norm of `x` is `∏ w, (normAtPlace x) ^ mult w`. It is defined such that the norm of
 `mixedEmbedding K a` for `a : K` is equal to the absolute value of the norm of `a` over `ℚ`,
 see `norm_eq_norm`. -/
-protected def norm : (E K) →*₀ ℝ where
+protected def norm : (mixedSpace K) →*₀ ℝ where
   toFun x := ∏ w, (normAtPlace w x) ^ (mult w)
   map_one' := by simp only [map_one, one_pow, prod_const_one]
   map_zero' := by simp [mult]
   map_mul' _ _ := by simp only [map_mul, mul_pow, prod_mul_distrib]
 
-protected theorem norm_apply (x : E K) :
+protected theorem norm_apply (x : mixedSpace K) :
     mixedEmbedding.norm x = ∏ w, (normAtPlace w x) ^ (mult w) := rfl
 
-protected theorem norm_nonneg (x : E K) :
+protected theorem norm_nonneg (x : mixedSpace K) :
     0 ≤ mixedEmbedding.norm x := univ.prod_nonneg fun _ _ ↦ pow_nonneg (normAtPlace_nonneg _ _) _
 
-protected theorem norm_eq_zero_iff {x : E K} :
+protected theorem norm_eq_zero_iff {x : mixedSpace K} :
     mixedEmbedding.norm x = 0 ↔ ∃ w, normAtPlace w x = 0 := by
   simp_rw [mixedEmbedding.norm, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, prod_eq_zero_iff,
     mem_univ, true_and, pow_eq_zero_iff mult_ne_zero]
 
-protected theorem norm_ne_zero_iff {x : E K} :
+protected theorem norm_ne_zero_iff {x : mixedSpace K} :
     mixedEmbedding.norm x ≠ 0 ↔ ∀ w, normAtPlace w x ≠ 0 := by
   rw [← not_iff_not]
   simp_rw [ne_eq, mixedEmbedding.norm_eq_zero_iff, not_not, not_forall, not_not]
 
-theorem norm_smul (c : ℝ) (x : E K) :
+theorem norm_smul (c : ℝ) (x : mixedSpace K) :
     mixedEmbedding.norm (c • x) = |c| ^ finrank ℚ K * (mixedEmbedding.norm x) := by
   simp_rw [mixedEmbedding.norm_apply, normAtPlace_smul, mul_pow, prod_mul_distrib,
     prod_pow_eq_pow_sum, sum_mult_eq]
 
 theorem norm_real (c : ℝ) :
-    mixedEmbedding.norm ((fun _ ↦ c, fun _ ↦ c) : (E K)) = |c| ^ finrank ℚ K := by
-  rw [show ((fun _ ↦ c, fun _ ↦ c) : (E K)) = c • 1 by ext <;> simp, norm_smul, map_one, mul_one]
+    mixedEmbedding.norm ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = |c| ^ finrank ℚ K := by
+  rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, norm_smul, map_one,
+    mul_one]
 
 @[simp]
 theorem norm_eq_norm (x : K) :
     mixedEmbedding.norm (mixedEmbedding K x) = |Algebra.norm ℚ x| := by
   simp_rw [mixedEmbedding.norm_apply, normAtPlace_apply, prod_eq_abs_norm]
 
-theorem norm_eq_zero_iff' {x : E K} (hx : x ∈ Set.range (mixedEmbedding K)) :
+theorem norm_eq_zero_iff' {x : mixedSpace K} (hx : x ∈ Set.range (mixedEmbedding K)) :
     mixedEmbedding.norm x = 0 ↔ x = 0 := by
   obtain ⟨a, rfl⟩ := hx
   rw [norm_eq_norm, Rat.cast_abs, abs_eq_zero, Rat.cast_eq_zero, Algebra.norm_eq_zero_iff,
@@ -410,25 +408,27 @@ variable [NumberField K]
 /-- The type indexing the basis `stdBasis`. -/
 abbrev index := {w : InfinitePlace K // IsReal w} ⊕ ({w : InfinitePlace K // IsComplex w}) × (Fin 2)
 
-/-- The `ℝ`-basis of `({w // IsReal w} → ℝ) × ({ w // IsComplex w } → ℂ)` formed by the vector
-equal to `1` at `w` and `0` elsewhere for `IsReal w` and by the couple of vectors equal to `1`
-(resp. `I`) at `w` and `0` elsewhere for `IsComplex w`. -/
-def stdBasis : Basis (index K) ℝ (E K) :=
+/-- The `ℝ`-basis of the mixed space of `K` formed by the vector equal to `1` at `w` and `0`
+elsewhere for `IsReal w` and by the couple of vectors equal to `1` (resp. `I`) at `w` and `0`
+elsewhere for `IsComplex w`. -/
+def stdBasis : Basis (index K) ℝ (mixedSpace K) :=
   Basis.prod (Pi.basisFun ℝ _)
     (Basis.reindex (Pi.basis fun _ => basisOneI) (Equiv.sigmaEquivProd _ _))
 
 variable {K}
 
 @[simp]
-theorem stdBasis_apply_ofIsReal (x : E K) (w : {w : InfinitePlace K // IsReal w}) :
+theorem stdBasis_apply_ofIsReal (x : mixedSpace K) (w : {w : InfinitePlace K // IsReal w}) :
     (stdBasis K).repr x (Sum.inl w) = x.1 w := rfl
 
 @[simp]
-theorem stdBasis_apply_ofIsComplex_fst (x : E K) (w : {w : InfinitePlace K // IsComplex w}) :
+theorem stdBasis_apply_ofIsComplex_fst (x : mixedSpace K)
+    (w : {w : InfinitePlace K // IsComplex w}) :
     (stdBasis K).repr x (Sum.inr ⟨w, 0⟩) = (x.2 w).re := rfl
 
 @[simp]
-theorem stdBasis_apply_ofIsComplex_snd (x : E K) (w : {w : InfinitePlace K // IsComplex w}) :
+theorem stdBasis_apply_ofIsComplex_snd (x : mixedSpace K)
+    (w : {w : InfinitePlace K // IsComplex w}) :
     (stdBasis K).repr x (Sum.inr ⟨w, 1⟩) = (x.2 w).im := rfl
 
 variable (K)
@@ -547,9 +547,9 @@ open Module.Free
 
 open scoped nonZeroDivisors
 
-/-- A `ℝ`-basis of `ℝ^r₁ × ℂ^r₂` that is also a `ℤ`-basis of the image of `𝓞 K`. -/
+/-- A `ℝ`-basis of the mixed space that is also a `ℤ`-basis of the image of `𝓞 K`. -/
 def latticeBasis :
-    Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (E K) := by
+    Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K) := by
   classical
     -- We construct an `ℝ`-linear independent family from the image of
     -- `canonicalEmbedding.lattice_basis` by `commMap`
@@ -571,7 +571,7 @@ theorem latticeBasis_apply (i : ChooseBasisIndex ℤ (𝓞 K)) :
   simp only [latticeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, Function.comp_apply,
     canonicalEmbedding.latticeBasis_apply, integralBasis_apply, commMap_canonical_eq_mixed]
 
-theorem mem_span_latticeBasis (x : (E K)) :
+theorem mem_span_latticeBasis (x : (mixedSpace K)) :
     x ∈ Submodule.span ℤ (Set.range (latticeBasis K)) ↔
       x ∈ ((mixedEmbedding K).comp (algebraMap (𝓞 K) K)).range := by
   rw [show Set.range (latticeBasis K) =
@@ -611,8 +611,8 @@ variable (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ)
 /-- The generalized index of the lattice generated by `I` in the lattice generated by
 `𝓞 K` is equal to the norm of the ideal `I`. The result is stated in terms of base change
 determinant and is the translation of `NumberField.det_basisOfFractionalIdeal_eq_absNorm` in
-`ℝ^r₁ × ℂ^r₂`. This is useful, in particular, to prove that the family obtained from
-the `ℤ`-basis of `I` is actually an `ℝ`-basis of `ℝ^r₁ × ℂ^r₂`, see
+the mixed space. This is useful, in particular, to prove that the family obtained from
+the `ℤ`-basis of `I` is actually an `ℝ`-basis of the mixed space, see
 `fractionalIdealLatticeBasis`. -/
 theorem det_basisOfFractionalIdeal_eq_norm
     (e : (ChooseBasisIndex ℤ (𝓞 K)) ≃ (ChooseBasisIndex ℤ I)) :
@@ -628,10 +628,10 @@ theorem det_basisOfFractionalIdeal_eq_norm
   simp_rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply, Function.comp_apply]
   exact latticeBasis_repr_apply K _ i
 
-/-- A `ℝ`-basis of `ℝ^r₁ × ℂ^r₂` that is also a `ℤ`-basis of the image of the fractional
+/-- A `ℝ`-basis of the mixed space of `K` that is also a `ℤ`-basis of the image of the fractional
 ideal `I`. -/
 def fractionalIdealLatticeBasis :
-    Basis (ChooseBasisIndex ℤ I) ℝ (E K) := by
+    Basis (ChooseBasisIndex ℤ I) ℝ (mixedSpace K) := by
   let e : (ChooseBasisIndex ℤ (𝓞 K)) ≃ (ChooseBasisIndex ℤ I) := by
     refine Fintype.equivOfCardEq ?_
     rw [← finrank_eq_card_chooseBasisIndex, ← finrank_eq_card_chooseBasisIndex,
@@ -650,7 +650,7 @@ theorem fractionalIdealLatticeBasis_apply (i : ChooseBasisIndex ℤ I) :
   simp only [fractionalIdealLatticeBasis, Basis.coe_reindex, Basis.coe_mk, Function.comp_apply,
     Equiv.apply_symm_apply]
 
-theorem mem_span_fractionalIdealLatticeBasis (x : (E K)) :
+theorem mem_span_fractionalIdealLatticeBasis (x : (mixedSpace K)) :
     x ∈ Submodule.span ℤ (Set.range (fractionalIdealLatticeBasis K I)) ↔
       x ∈ mixedEmbedding K '' I := by
   rw [show Set.range (fractionalIdealLatticeBasis K I) =