1st commit

Author: xroblot

Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

@@ -188,4 +188,126 @@ theorem mulEquivCongr_apply_smul [IsGaloisGroup G K L] [Finite G] [IsGaloisGroup
     (g : G) (x : L) : mulEquivCongr G H K L g • x = g • x :=
   AlgEquiv.ext_iff.mp ((mulEquivAlgEquiv H K L).apply_symm_apply (mulEquivAlgEquiv G K L g)) x
 
+@[simp]
+theorem map_mulEquivAlgEquiv_fixingSubgroup
+    [IsGaloisGroup G K L] [Finite G] (F : IntermediateField K L) :
+    (fixingSubgroup G (F : Set L)).map (mulEquivAlgEquiv G K L) = F.fixingSubgroup := by
+  ext g
+  obtain ⟨g, rfl⟩ := (mulEquivAlgEquiv G K L).surjective g
+  simp [mem_fixingSubgroup_iff]
+
+variable (H H' : Subgroup G) (F F' : IntermediateField K L)
+
+instance to_subgroup [hGKL : IsGaloisGroup G K L] :
+    IsGaloisGroup H (FixedPoints.intermediateField H : IntermediateField K L) L where
+  faithful := have := hGKL.faithful; inferInstance
+  commutes := inferInstanceAs <| SMulCommClass H (FixedPoints.subfield H L) L
+  isInvariant := ⟨fun x h ↦ ⟨⟨x, h⟩, rfl⟩⟩
+
+theorem card_subgroup_eq_finrank_fixedpoints [IsGaloisGroup G K L] :
+    Nat.card H = Module.finrank (FixedPoints.intermediateField H : IntermediateField K L) L :=
+  card_eq_finrank H (FixedPoints.intermediateField H) L
+
+variable {G K L} in
+theorem of_mulEquiv_algEquiv [IsGalois K L] (e : G ≃* Gal(L/K)) (he : ∀ g x, e g x = g • x) :
+    IsGaloisGroup G K L where
+  faithful := ⟨fun {g₁ g₂} h ↦ e.injective <| AlgEquiv.ext <| by simpa [he]⟩
+  commutes := ⟨by simp [← he]⟩
+  isInvariant := ⟨fun y hy ↦ (InfiniteGalois.mem_bot_iff_fixed y).mpr <|
+    e.surjective.forall.mpr <| by simpa [he]⟩
+
+instance of_fixed_field [Finite G] [FaithfulSMul G L] :
+    IsGaloisGroup G (FixedPoints.subfield G L) L :=
+  of_mulEquiv_algEquiv (FixedPoints.toAlgAutMulEquiv _ _) fun _ _ ↦ rfl
+
+instance to_intermediateField [Finite G] [hGKL : IsGaloisGroup G K L] :
+    IsGaloisGroup (fixingSubgroup G (F : Set L)) F L :=
+  let e := ((mulEquivAlgEquiv G K L).subgroupMap (fixingSubgroup G (F : Set L))).trans <|
+    (MulEquiv.subgroupCongr (map_mulEquivAlgEquiv_fixingSubgroup ..)).trans <|
+    IntermediateField.fixingSubgroupEquiv F
+  have := hGKL.isGalois
+  .of_mulEquiv_algEquiv e fun _ _ ↦ rfl
+
+theorem card_fixingSubgroup_eq_finrank [Finite G] [IsGaloisGroup G K L] :
+    Nat.card (fixingSubgroup G (F : Set L)) = Module.finrank F L :=
+  card_eq_finrank ..
+
+section GaloisCorrespondence
+
+theorem fixingSubgroup_le_of_le (h : F ≤ F') :
+    fixingSubgroup G (F' : Set L) ≤ fixingSubgroup G (F : Set L) :=
+  fun _ hσ ⟨x, hx⟩ ↦ hσ ⟨x, h hx⟩
+
+section SMulCommClass
+
+variable [SMulCommClass G K L]
+
+theorem fixingSubgroup_bot : fixingSubgroup G ((⊥ : IntermediateField K L) : Set L) = ⊤ := by
+  simp [Subgroup.ext_iff, mem_fixingSubgroup_iff, IntermediateField.mem_bot]
+
+theorem fixedPoints_bot :
+    (FixedPoints.intermediateField (⊥ : Subgroup G) : IntermediateField K L) = ⊤ := by
+  simp [IntermediateField.ext_iff]
+
+theorem le_fixedPoints_iff_le_fixingSubgroup :
+    F ≤ FixedPoints.intermediateField H ↔ H ≤ fixingSubgroup G (F : Set L) :=
+  ⟨fun h g hg x ↦ h x.2 ⟨g, hg⟩, fun h x hx g ↦ h g.2 ⟨x, hx⟩⟩
+
+theorem fixedPoints_le_of_le (h : H ≤ H') :
+    FixedPoints.intermediateField H' ≤ (FixedPoints.intermediateField H : IntermediateField K L) :=
+  fun _ hσ ⟨x, hx⟩ ↦ hσ ⟨x, h hx⟩
+
+end SMulCommClass
+
+section IsGaloisGroup
+
+variable [hGKL : IsGaloisGroup G K L]
+
+theorem fixingSubgroup_top : fixingSubgroup G ((⊤ : IntermediateField K L) : Set L) = ⊥ := by
+  have := hGKL.faithful
+  ext; simpa [mem_fixingSubgroup_iff, Set.ext_iff] using MulAction.fixedBy_eq_univ_iff_eq_one
+
+theorem fixedPoints_top :
+    (FixedPoints.intermediateField (⊤ : Subgroup G) : IntermediateField K L) = ⊥ := by
+  convert IsGaloisGroup.fixedPoints_eq_bot G K L
+  ext; simp
+
+/-- The Galois correspondence from intermediate fields to subgroups. -/
+noncomputable def intermediateFieldEquivSubgroup [Finite G] :
+    IntermediateField K L ≃o (Subgroup G)ᵒᵈ :=
+  have := isGalois G K L
+  have := finiteDimensional G K L
+  IsGalois.intermediateFieldEquivSubgroup.trans <| (mulEquivAlgEquiv G K L).comapSubgroup.dual
+
+@[simp] lemma intermediateFieldEquivSubgroup_apply [Finite G] {F} :
+    intermediateFieldEquivSubgroup G K L F = .toDual (fixingSubgroup G (F : Set L)) := rfl
+
+lemma ofDual_intermediateFieldEquivSubgroup_apply [Finite G] {F} :
+    (intermediateFieldEquivSubgroup G K L F).ofDual = fixingSubgroup G (F : Set L) := rfl
+
+@[simp] lemma intermediateFieldEquivSubgroup_symm_apply [Finite G] {H} :
+    (intermediateFieldEquivSubgroup G K L).symm H = FixedPoints.intermediateField H.ofDual := by
+  obtain ⟨H, rfl⟩ := OrderDual.toDual.surjective H
+  simp [IntermediateField.ext_iff, intermediateFieldEquivSubgroup,
+    (mulEquivAlgEquiv G K L).surjective.forall, -mulEquivAlgEquiv_symm_apply]
+
+lemma intermediateFieldEquivSubgroup_symm_apply_toDual [Finite G] {H} :
+    (intermediateFieldEquivSubgroup G K L).symm (.toDual H) = FixedPoints.intermediateField H :=
+  intermediateFieldEquivSubgroup_symm_apply ..
+
+theorem fixingSubgroup_fixedPoints [Finite G] :
+    fixingSubgroup G ((FixedPoints.intermediateField H : IntermediateField K L) : Set L) = H := by
+  rw [← intermediateFieldEquivSubgroup_symm_apply_toDual,
+    ← ofDual_intermediateFieldEquivSubgroup_apply,
+    OrderIso.apply_symm_apply, OrderDual.ofDual_toDual]
+
+theorem fixedPoints_fixingSubgroup [Finite G] :
+    FixedPoints.intermediateField (fixingSubgroup G (F : Set L)) = F := by
+  rw [← ofDual_intermediateFieldEquivSubgroup_apply, ← intermediateFieldEquivSubgroup_symm_apply,
+    OrderIso.symm_apply_apply]
+
+end IsGaloisGroup
+
+end GaloisCorrespondence
+
 end IsGaloisGroup

Mathlib/NumberTheory/NumberField/CMField.lean

@@ -5,20 +5,22 @@ 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
-public import Mathlib.RingTheory.RootsOfUnity.Complex
 
 /-!
 # CM-extension of number fields
 
-A CM-extension `K/F` of number fields is an extension where `K` is totally complex, `F` is
+A CM-extension `K/F` of fields is an extension where `K` is totally complex, `F` is
 totally real and `K` is a quadratic extension of `F`. In this situation, the totally real
 subfield `F` is (isomorphic to) the maximal real subfield `K⁺` of `K`.
 
 ## Main definitions and results
 
-* `NumberField.IsCMField`: A predicate that says that if a number field is CM, then it is a totally
+* `NumberField.IsCMField`: A predicate that says that if a field is CM, then it is a totally
   complex quadratic extension of its totally real subfield
 
 * `NumberField.CMExtension.equivMaximalRealSubfield`: Any field `F` such that `K/F` is a
@@ -61,18 +63,18 @@ namespace NumberField
 section maximalRealSubfield
 
 /--
-A number field `K` is `CM` if `K` is a totally complex quadratic extension of its maximal
+A field `K` is `CM` if `K` is a totally complex quadratic extension of its maximal
 real subfield `K⁺`.
 -/
-class IsCMField (K : Type*) [Field K] [NumberField K] : Prop where
+class IsCMField (K : Type*) [Field K] [CharZero K] : Prop where
   [to_isTotallyComplex : IsTotallyComplex K]
   [is_quadratic : IsQuadraticExtension (maximalRealSubfield K) K]
 
 namespace IsCMField
 
 open ComplexEmbedding
 
-variable (K : Type*) [Field K] [NumberField K] [IsCMField K]
+variable (K : Type*) [Field K] [CharZero K] [IsCMField K]
 
 local notation3 "K⁺" => maximalRealSubfield K
 
@@ -82,7 +84,7 @@ instance isQuadraticExtension : IsQuadraticExtension K⁺ K :=
 instance isTotallyComplex : IsTotallyComplex K :=
   IsCMField.to_isTotallyComplex
 
-theorem card_infinitePlace_eq_card_infinitePlace :
+theorem card_infinitePlace_eq_card_infinitePlace [NumberField K] :
     Fintype.card (InfinitePlace K⁺) = Fintype.card (InfinitePlace K) := by
   rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
     IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add,
@@ -94,24 +96,26 @@ theorem card_infinitePlace_eq_card_infinitePlace :
 The equiv between the infinite places of `K` and the infinite places of `K⁺` induced by the
 restriction to `K⁺`, see `equivInfinitePlace_apply`.
 -/
-noncomputable def equivInfinitePlace : InfinitePlace K ≃ InfinitePlace K⁺ :=
+noncomputable def equivInfinitePlace [NumberField K] : InfinitePlace K ≃ InfinitePlace K⁺ :=
   Equiv.ofBijective (fun w ↦ w.comap (algebraMap K⁺ K)) <|
     (Fintype.bijective_iff_surjective_and_card _).mpr
       ⟨comap_surjective, (card_infinitePlace_eq_card_infinitePlace K).symm⟩
 
 @[simp]
-theorem equivInfinitePlace_apply (w : InfinitePlace K) :
+theorem equivInfinitePlace_apply [NumberField K] (w : InfinitePlace K) :
     equivInfinitePlace K w = w.comap (algebraMap K⁺ K) := rfl
 
 @[simp]
-theorem equivInfinitePlace_symm_apply (w : InfinitePlace K⁺) (x : K⁺) :
+theorem equivInfinitePlace_symm_apply [NumberField K] (w : InfinitePlace K⁺) (x : K⁺) :
     (equivInfinitePlace K).symm w (algebraMap K⁺ K x) = w x := by
   rw [← comap_apply, ← equivInfinitePlace_apply, Equiv.apply_symm_apply]
 
-theorem units_rank_eq_units_rank :
+theorem units_rank_eq_units_rank [NumberField K] :
     Units.rank K⁺ = Units.rank K := by
   rw [Units.rank, Units.rank, card_infinitePlace_eq_card_infinitePlace K]
 
+section complexConj
+
 theorem exists_isConj (φ : K →+* ℂ) :
     ∃ σ : K ≃ₐ[K⁺] K, IsConj φ σ :=
   exists_isConj_of_isRamified <|
@@ -129,6 +133,8 @@ theorem isConj_eq_isConj {φ ψ : K →+* ℂ} {σ τ : K ≃ₐ[K⁺] K}
     ((isConj_ne_one_iff hφ).mpr <| IsTotallyComplex.complexEmbedding_not_isReal φ)
     ((isConj_ne_one_iff hψ).mpr <| IsTotallyComplex.complexEmbedding_not_isReal ψ)
 
+variable [Algebra.IsIntegral ℚ K]
+
 /--
 The complex conjugation of the CM-field `K`.
 -/
@@ -244,13 +250,15 @@ theorem ringOfIntegersComplexConj_eq_self_iff (x : 𝓞 K) :
   · rintro ⟨y, rfl⟩
     simp
 
+end complexConj
+
 section units
 
 open Units
 
 /--
 The complex conjugation as an isomorphism of the units of `K`. -/
-noncomputable abbrev unitsComplexConj : (𝓞 K)ˣ ≃* (𝓞 K)ˣ :=
+noncomputable abbrev unitsComplexConj [Algebra.IsIntegral ℚ K] : (𝓞 K)ˣ ≃* (𝓞 K)ˣ :=
   Units.mapEquiv <| RingOfIntegers.mapRingEquiv (complexConj K).toRingEquiv
 
 /--
@@ -259,18 +267,20 @@ by the complex conjugation, see `IsCMField.unitsComplexConj_eq_self_iff`.
 -/
 def realUnits : Subgroup (𝓞 K)ˣ := (Units.map (algebraMap (𝓞 K⁺) (𝓞 K)).toMonoidHom).range
 
-omit [IsCMField K] in
+omit [IsCMField K] [CharZero K] in
 theorem mem_realUnits_iff (u : (𝓞 K)ˣ) :
     u ∈ realUnits K ↔ ∃ v : (𝓞 K⁺)ˣ, algebraMap (𝓞 K⁺) (𝓞 K) v = u := by
   simp [realUnits, MonoidHom.mem_range, RingHom.toMonoidHom_eq_coe, Units.ext_iff]
 
-theorem unitsComplexConj_eq_self_iff (u : (𝓞 K)ˣ) :
+theorem unitsComplexConj_eq_self_iff [Algebra.IsIntegral ℚ K] (u : (𝓞 K)ˣ) :
     unitsComplexConj K u = u ↔ u ∈ realUnits K := by
   simp_rw [Units.ext_iff,  mem_realUnits_iff, RingOfIntegers.ext_iff, Units.coe_mapEquiv,
     AlgEquiv.toRingEquiv_eq_coe, RingEquiv.coe_toMulEquiv, RingOfIntegers.mapRingEquiv_apply,
     AlgEquiv.coe_ringEquiv, Units.complexConj_eq_self_iff,
     IsScalarTower.algebraMap_apply (𝓞 K⁺) (𝓞 K) K]
 
+variable [NumberField K]
+
 /--
 The image of a root of unity by the complex conjugation is its inverse.
 This is the version of `Complex.conj_rootsOfUnity` for CM-fields.
@@ -440,7 +450,7 @@ end maximalRealSubfield
 
 namespace CMExtension
 
-variable (F K : Type*) [Field F] [NumberField F] [IsTotallyReal F] [Field K] [NumberField K]
+variable (F K : Type*) [Field F] [IsTotallyReal F] [Field K] [CharZero K] [Algebra.IsIntegral ℚ K]
   [IsTotallyComplex K] [Algebra F K] [IsQuadraticExtension F K]
 
 theorem eq_maximalRealSubfield (E : Subfield K) [IsTotallyReal E] [IsQuadraticExtension E K] :
@@ -457,6 +467,8 @@ theorem eq_maximalRealSubfield (E : Subfield K) [IsTotallyReal E] [IsQuadraticEx
       rw [← SetLike.coe_set_eq, Subfield.coe_toIntermediateField] at h
       rw [← sup_eq_left, ← SetLike.coe_set_eq, h, IntermediateField.coe_bot]
       aesop
+  have : Algebra.IsAlgebraic (maximalRealSubfield K) K :=
+    Algebra.IsAlgebraic.tower_top (K := ℚ) (maximalRealSubfield K)
   have : IsTotallyReal K := (h' ▸ isTotallyReal_sup).ofRingEquiv Subring.topEquiv
   obtain w : InfinitePlace K := Classical.choice (inferInstance : Nonempty _)
   exact (not_isReal_iff_isComplex.mpr (IsTotallyComplex.isComplex w)) (IsTotallyReal.isReal w)
@@ -484,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)⟩
@@ -497,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 {σ : 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 [IsGalois ℚ K] [IsMulCommutative Gal(K/ℚ)] :
+instance of_isAbelianGalois [IsAbelianGalois ℚ K] :
     IsCMField K := by
   let φ : K →+* ℂ := Classical.choice (inferInstance : Nonempty _)
   obtain ⟨σ, hσ₁⟩ : ∃ σ : Gal(K/ℚ), ComplexEmbedding.IsConj φ σ :=
@@ -527,6 +551,30 @@ instance of_isMulCommutative [IsGalois ℚ K] [IsMulCommutative Gal(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