1st commit

Author: xroblot

Mathlib/NumberTheory/NumberField/CMField.lean

@@ -6,7 +6,9 @@ Authors: Xavier Roblot
 module
 
 public import Mathlib.FieldTheory.Galois.Abelian
+public import Mathlib.FieldTheory.Galois.IsGaloisGroup
 public import Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
+public import Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
 public import Mathlib.NumberTheory.NumberField.Units.Regulator
 
 /-!
@@ -494,11 +496,18 @@ theorem algebraMap_equivMaximalRealSubfield_symm_apply (x : maximalRealSubfield
       algebraMap (maximalRealSubfield K) K x := by
   simpa using (equivMaximalRealSubfield_apply F K ((equivMaximalRealSubfield F K).symm x)).symm
 
+end CMExtension
+
+namespace IsCMField
+
+variable (F K : Type*) [Field F] [IsTotallyReal F] [Field K] [CharZero K] [Algebra.IsIntegral ℚ K]
+  [IsTotallyComplex K] [Algebra F K] [IsQuadraticExtension F K]
+
 include F in
 /--
 If `K/F` is a CM-extension then `K` is a CM-field.
 -/
-theorem _root_.NumberField.IsCMField.ofCMExtension :
+theorem ofCMExtension :
     IsCMField K where
   is_quadratic := ⟨(IsQuadraticExtension.finrank_eq_two F K) ▸ finrank_eq_of_equiv_equiv
       (CMExtension.equivMaximalRealSubfield F K).symm (RingEquiv.refl K) (by ext; simp)⟩
@@ -507,24 +516,29 @@ open IntermediateField in
 /--
 A totally complex field that has a unique complex conjugation is CM.
 -/
-theorem _root_.NumberField.IsCMField.of_forall_isConj [NumberField K] {σ : Gal(K/ℚ)}
+theorem of_forall_isConj [IsGalois ℚ K] {σ : Gal(K/ℚ)}
     (hσ : ∀ φ : K →+* ℂ, IsConj φ σ) : IsCMField K := by
-  have : IsTotallyReal (fixedField (Subgroup.zpowers σ)) := ⟨fun w ↦ by
+  let φ : K →+* ℂ := Classical.choice (inferInstance : Nonempty _)
+  have hσ' : Nat.card (Subgroup.zpowers σ) = 2 := by
+    rw [Nat.card_zpowers, orderOf_isConj_two_of_ne_one (hσ φ)]
+    exact (isConj_ne_one_iff (hσ φ)).mpr <| IsTotallyComplex.complexEmbedding_not_isReal φ
+  have : Finite (Subgroup.zpowers σ) := Nat.finite_of_card_ne_zero (by positivity)
+  let L := (FixedPoints.intermediateField (Subgroup.zpowers σ) : IntermediateField ℚ K)
+  have : IsTotallyReal L := ⟨fun w ↦ by
     obtain ⟨W, rfl⟩ := w.comap_surjective (K := K)
-    let τ := subgroupEquivAlgEquiv _ ⟨σ, Subgroup.mem_zpowers σ⟩
-    have hτ : IsConj W.embedding τ := hσ _
-    simpa [← isReal_mk_iff, ← InfinitePlace.comap_mk, mk_embedding] using hτ.isReal_comp⟩
-  have : IsQuadraticExtension (fixedField (Subgroup.zpowers σ)) K := ⟨by
-    let φ : K →+* ℂ := Classical.choice (inferInstance : Nonempty _)
-    have hσ' : σ ≠ 1 :=
-      (isConj_ne_one_iff (hσ φ)).mpr <| IsTotallyComplex.complexEmbedding_not_isReal φ
-    rw [finrank_fixedField_eq_card, Nat.card_zpowers, orderOf_isConj_two_of_ne_one (hσ φ) hσ']⟩
-  exact IsCMField.ofCMExtension (fixedField (Subgroup.zpowers σ)) K
+    dsimp only
+    rw [← mk_embedding W, comap_mk, isReal_mk_iff]
+    exact ComplexEmbedding.IsConj.isReal_comp
+     (σ := IsGaloisGroup.mulEquivAlgEquiv (Subgroup.zpowers σ) L K ⟨σ, Subgroup.mem_zpowers σ⟩)
+      (hσ W.embedding)⟩
+  have : IsQuadraticExtension L K := ⟨by
+    rw [← IsGaloisGroup.card_subgroup_eq_finrank_fixedpoints, hσ']⟩
+  exact IsCMField.ofCMExtension L K
 
 /--
 A totally complex abelian extension of `ℚ` is CM.
 -/
-instance of_isMulCommutative [NumberField K] [IsAbelianGalois ℚ K] :
+instance of_isAbelianGalois [IsAbelianGalois ℚ K] :
     IsCMField K := by
   let φ : K →+* ℂ := Classical.choice (inferInstance : Nonempty _)
   obtain ⟨σ, hσ₁⟩ : ∃ σ : Gal(K/ℚ), ComplexEmbedding.IsConj φ σ :=
@@ -537,7 +551,30 @@ instance of_isMulCommutative [NumberField K] [IsAbelianGalois ℚ K] :
     exact hσ₁.comp _
   exact IsCMField.of_forall_isConj K hσ₂
 
-end CMExtension
+@[deprecated (since := "2025-11-19")] alias NumberField.CMExtension.of_isMulCommutative :=
+  NumberField.IsCMField.of_isAbelianGalois
 
-end NumberField
+end NumberField.IsCMField
+namespace IsCyclotomicExtension.Rat
 
+variable (K : Type*) [Field K] [CharZero K]
+
+open IntermediateField in
+theorem isCMField {S : Set ℕ} (hS : ∃ n ∈ S, 2 < n) [IsCyclotomicExtension S ℚ K] :
+    IsCMField K := by
+  have : Algebra.IsIntegral ℚ K := integral S ℚ K
+  obtain ⟨n, hn₁, hn₂⟩ := hS
+  have : NeZero n := ⟨by positivity⟩
+  obtain ⟨ζ, hζ⟩ := exists_isPrimitiveRoot ℚ K hn₁ (by grind)
+  have : IsTotallyComplex K := by
+    have : IsCyclotomicExtension {n} ℚ ℚ⟮ζ⟯ := hζ.intermediateField_adjoin_isCyclotomicExtension ℚ
+    have : IsTotallyComplex ℚ⟮ζ⟯ := isTotallyComplex ℚ⟮ζ⟯ hn₂
+    exact isTotallyComplex_of_algebra ℚ⟮ζ⟯ _
+  have := isAbelianGalois S ℚ K
+  exact IsCMField.of_isAbelianGalois K
+
+instance [IsCyclotomicExtension ⊤ ℚ K] :
+    IsCMField K :=
+  isCMField K (S := ⊤) ⟨3, trivial, Nat.lt_succ_self 2⟩
+
+end IsCyclotomicExtension.Rat

Mathlib/NumberTheory/NumberField/Cyclotomic/Embeddings.lean

@@ -6,7 +6,7 @@ Authors: Riccardo Brasca
 module
 
 public import Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
-public import Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
+public import Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
 
 /-!
 # Cyclotomic extensions of `ℚ` are totally complex number fields.
@@ -30,13 +30,17 @@ variable {n : ℕ} [NeZero n] (K : Type u) [Field K] [CharZero K]
 
 /-- If `K` is a `n`-th cyclotomic extension of `ℚ`, where `2 < n`, then there are no real places
 of `K`. -/
-theorem nrRealPlaces_eq_zero [IsCyclotomicExtension {n} ℚ K]
-    (hn : 2 < n) :
+theorem nrRealPlaces_eq_zero [IsCyclotomicExtension {n} ℚ K] (hn : 2 < n) :
     haveI := IsCyclotomicExtension.numberField {n} ℚ K
     nrRealPlaces K = 0 := by
   have := IsCyclotomicExtension.numberField {n} ℚ K
   apply (IsCyclotomicExtension.zeta_spec n ℚ K).nrRealPlaces_eq_zero_of_two_lt hn
 
+theorem isTotallyComplex [IsCyclotomicExtension {n} ℚ K] (hn : 2 < n) :
+    IsTotallyComplex K := by
+  have := IsCyclotomicExtension.numberField {n} ℚ K
+  exact nrRealPlaces_eq_zero_iff.mp <| nrRealPlaces_eq_zero K hn
+
 variable (n)
 
 /-- If `K` is a `n`-th cyclotomic extension of `ℚ`, then there are `φ n / n` complex places

Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

@@ -72,6 +72,11 @@ lemma IsReal.comap (f : k →+* K) {w : InfinitePlace K} (hφ : IsReal w) :
   rw [← mk_embedding w, isReal_mk_iff] at hφ
   exact hφ.comp f
 
+lemma IsComplex.of_comap (f : k →+* K) {w : InfinitePlace K} (hf : IsComplex (w.comap f)) :
+    IsComplex w := by
+  rw [← not_isReal_iff_isComplex] at hf ⊢
+  exact (IsReal.comap f).mt hf
+
 lemma isReal_comap_iff (f : k ≃+* K) {w : InfinitePlace K} :
     IsReal (w.comap (f : k →+* K)) ↔ IsReal w := by
   rw [← mk_embedding w, comap_mk, isReal_mk_iff, isReal_mk_iff, ComplexEmbedding.isReal_comp_iff]

Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean

@@ -212,7 +212,7 @@ A field `K` is totally complex if all of its infinite places are complex.
 @[mk_iff] class IsTotallyComplex (K : Type*) [Field K] where
   isComplex : ∀ v : InfinitePlace K, v.IsComplex
 
-variable {F : Type*} [Field F] {K : Type*} [Field K] [Algebra F K]
+variable (F : Type*) [Field F] {K : Type*} [Field K] [Algebra F K]
 
 theorem nrRealPlaces_eq_zero_iff [NumberField K] :
     nrRealPlaces K = 0 ↔ IsTotallyComplex K := by
@@ -228,6 +228,10 @@ theorem IsTotallyComplex.mult_eq [IsTotallyComplex K] (w : InfinitePlace K) : mu
 
 variable (K)
 
+theorem isTotallyComplex_of_algebra [IsTotallyComplex F] :
+    IsTotallyComplex K where
+  isComplex _ := IsComplex.of_comap (algebraMap F K) <| IsTotallyComplex.isComplex _
+
 @[simp]
 theorem IsTotallyComplex.nrRealPlaces_eq_zero [NumberField K] [h : IsTotallyComplex K] :
     nrRealPlaces K = 0 :=