feat(NumberTheory/RamificationInertia): ramificationIdx and `inerti…

…aDeg` in Galois extensions (#20899) Assume `B/A` is a finite extension of Dedekind domains, `K` is the fraction ring of `A`, `L` is the fraction ring of `K`. We show that if `L/K` is a Galois extension, then 1. All `Ideal.ramificationIdx`(resp. `Ideal.inertiaDeg`) over a fixed maximal ideal `p` of `A` are the same, which we define as `Ideal.ramificationIdxIn`(resp. `Ideal.inertiaDegIn`). 2. Let `p` be a maximal ideal of `A`, `r` be the number of prime ideals lying over `p`, `e` be the ramification index of `p` in `B`, and `f` be the inertia degree of `p` in `B`. Then `r * (e * f) = [L : K]`. It is the form of [Ideal.sum_ramification_inertia](https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/RamificationInertia.html#Ideal.sum_ramification_inertia) in the case of Galois extension. This is adapted from the proof in [the case of number fields](https://github.com/jjdishere/neukirch/blob/8fdb75f7ebab8a20eea902058956d7dece648959/AlgebraicNumberTheory/AlgebraicIntegersPart2/HilbertRamificationTheory.lean#L591). Co-authored-by: Jiedong Jiang @jjdishere Co-authored-by: Yongle Hu <[email protected]> Co-authored-by: Yongle Hu <[email protected]>
leanprover-community · Feb 13, 2025 · e2c6f0e · e2c6f0e
1 parent 3412f5c
commit e2c6f0e
Show file tree

Hide file tree

Showing 3 changed files with 203 additions and 2 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -4172,6 +4172,7 @@ import Mathlib.NumberTheory.PrimesCongruentOne
 import Mathlib.NumberTheory.Primorial
 import Mathlib.NumberTheory.PythagoreanTriples
 import Mathlib.NumberTheory.RamificationInertia.Basic
+import Mathlib.NumberTheory.RamificationInertia.Galois
 import Mathlib.NumberTheory.Rayleigh
 import Mathlib.NumberTheory.SiegelsLemma
 import Mathlib.NumberTheory.SmoothNumbers

diff --git a/Mathlib/NumberTheory/RamificationInertia/Galois.lean b/Mathlib/NumberTheory/RamificationInertia/Galois.lean
@@ -0,0 +1,197 @@
+/-
+Copyright (c) 2024 Yongle Hu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yongle Hu, Jiedong Jiang
+-/
+import Mathlib.NumberTheory.RamificationInertia.Basic
+import Mathlib.RingTheory.Invariant
+
+/-!
+# Ramification theory in Galois extensions of Dedekind domains
+
+In this file, we discuss the ramification theory in Galois extensions of Dedekind domains, which is
+  also called Hilbert's Ramification Theory.
+
+Assume `B / A` is a finite extension of Dedekind domains, `K` is the fraction ring of `A`,
+  `L` is the fraction ring of `K`, `L / K` is a Galois extension.
+
+## Main definitions
+
+* `Ideal.ramificationIdxIn`: It can be seen from
+  the theorem `Ideal.ramificationIdx_eq_of_IsGalois` that all `Ideal.ramificationIdx` over a fixed
+  maximal ideal `p` of `A` are the same, which we define as `Ideal.ramificationIdxIn`.
+
+* `Ideal.inertiaDegIn`: It can be seen from
+  the theorem `Ideal.inertiaDeg_eq_of_IsGalois` that all `Ideal.inertiaDeg` over a fixed
+  maximal ideal `p` of `A` are the same, which we define as `Ideal.inertiaDegIn`.
+
+## Main results
+
+* `ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn`: Let `p` be a maximal ideal of `A`,
+  `r` be the number of prime ideals lying over `p`, `e` be the ramification index of `p` in `B`,
+  and `f` be the inertia degree of `p` in `B`. Then `r * (e * f) = [L : K]`. It is the form of the
+  `Ideal.sum_ramification_inertia` in the case of Galois extension.
+
+## References
+
+* [J Neukirch, *Algebraic Number Theory*][Neukirch1992]
+
+-/
+
+open Algebra
+
+attribute [local instance] FractionRing.liftAlgebra
+
+namespace Ideal
+
+open scoped Classical in
+/-- If `L / K` is a Galois extension, it can be seen from the theorem
+  `Ideal.ramificationIdx_eq_of_IsGalois` that all `Ideal.ramificationIdx` over a fixed
+  maximal ideal `p` of `A` are the same, which we define as `Ideal.ramificationIdxIn`. -/
+noncomputable def ramificationIdxIn {A : Type*} [CommRing A] (p : Ideal A)
+    (B : Type*) [CommRing B] [Algebra A B] : ℕ :=
+  if h : ∃ P : Ideal B, P.IsPrime ∧ P.LiesOver p then p.ramificationIdx (algebraMap A B) h.choose
+  else 0
+
+open scoped Classical in
+/-- If `L / K` is a Galois extension, it can be seen from
+  the theorem `Ideal.inertiaDeg_eq_of_IsGalois` that all `Ideal.inertiaDeg` over a fixed
+  maximal ideal `p` of `A` are the same, which we define as `Ideal.inertiaDegIn`. -/
+noncomputable def inertiaDegIn {A : Type*} [CommRing A] (p : Ideal A)
+    (B : Type*) [CommRing B] [Algebra A B] : ℕ :=
+  if h : ∃ P : Ideal B, P.IsPrime ∧ P.LiesOver p then p.inertiaDeg h.choose else 0
+
+section MulAction
+
+variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A}
+
+instance : MulAction (B ≃ₐ[A] B) (primesOver p B) where
+  smul σ Q := primesOver.mk p (map σ Q.1)
+  one_smul Q := Subtype.val_inj.mp (map_id Q.1)
+  mul_smul σ τ Q := Subtype.val_inj.mp (Q.1.map_map τ.toRingHom σ.toRingHom).symm
+
+@[simp]
+theorem coe_smul_primesOver (σ : B ≃ₐ[A] B) (P : primesOver p B): (σ • P).1 = map σ P :=
+  rfl
+
+@[simp]
+theorem coe_smul_primesOver_mk (σ : B ≃ₐ[A] B) (P : Ideal B) [P.IsPrime] [P.LiesOver p] :
+    (σ • primesOver.mk p P).1 = map σ P :=
+  rfl
+
+variable (K L : Type*) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L]
+  [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L]
+  [IsIntegralClosure B A L] [FiniteDimensional K L]
+
+instance : MulAction (L ≃ₐ[K] L) (primesOver p B) where
+  smul σ Q := primesOver.mk p (map (galRestrict A K L B σ) Q.1)
+  one_smul Q := by
+    apply Subtype.val_inj.mp
+    show map _ Q.1 = Q.1
+    simpa only [map_one] using map_id Q.1
+  mul_smul σ τ Q := by
+    apply Subtype.val_inj.mp
+    show map _ Q.1 = map _ (map _ Q.1)
+    rw [_root_.map_mul]
+    exact (Q.1.map_map ((galRestrict A K L B) τ).toRingHom ((galRestrict A K L B) σ).toRingHom).symm
+
+theorem coe_smul_primesOver_eq_map_galRestrict (σ : L ≃ₐ[K] L) (P : primesOver p B):
+    (σ • P).1 = map (galRestrict A K L B σ) P :=
+  rfl
+
+theorem coe_smul_primesOver_mk_eq_map_galRestrict (σ : L ≃ₐ[K] L) (P : Ideal B) [P.IsPrime]
+    [P.LiesOver p] : (σ • primesOver.mk p P).1 = map (galRestrict A K L B σ) P :=
+  rfl
+
+end MulAction
+
+section RamificationInertia
+
+variable {A B : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [CommRing B] [IsDomain B]
+  [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] (p : Ideal A) (P Q : Ideal B)
+  [hPp : P.IsPrime] [hp : P.LiesOver p] [hQp : Q.IsPrime] [Q.LiesOver p]
+  (K L : Type*) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L]
+  [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L]
+  [FiniteDimensional K L]
+
+include p in
+/-- If `p` is a maximal ideal of `A`, `P` and `Q` are prime ideals
+  lying over `p`, then there exists `σ ∈ Aut (B / A)` such that `σ P = Q`. In other words,
+  the Galois group `Gal(L / K)` acts transitively on the set of all prime ideals lying over `p`. -/
+theorem exists_map_eq_of_isGalois [IsGalois K L] : ∃ σ : B ≃ₐ[A] B, map σ P = Q := by
+  have : FaithfulSMul A B := FaithfulSMul.of_field_isFractionRing A B K L
+  have : IsInvariant A B (B ≃ₐ[A] B) := isInvariant_of_isGalois' A K L B
+  rcases IsInvariant.exists_smul_of_under_eq A B (B ≃ₐ[A] B) P Q <|
+    (over_def P p).symm.trans (over_def Q p) with ⟨σ, hs⟩
+  exact ⟨σ, hs.symm⟩
+
+theorem isPretransitive_of_isGalois [IsGalois K L] :
+    MulAction.IsPretransitive (B ≃ₐ[A] B) (primesOver p B) where
+  exists_smul_eq := by
+    intro ⟨P, _, _⟩ ⟨Q, _, _⟩
+    rcases exists_map_eq_of_isGalois p P Q K L with ⟨σ, hs⟩
+    exact ⟨σ, Subtype.val_inj.mp hs⟩
+
+instance [IsGalois K L] : MulAction.IsPretransitive (L ≃ₐ[K] L) (primesOver p B) where
+  exists_smul_eq := by
+    intro ⟨P, _, _⟩ ⟨Q, _, _⟩
+    rcases exists_map_eq_of_isGalois p P Q K L with ⟨σ, hs⟩
+    exact ⟨(galRestrict A K L B).symm σ, Subtype.val_inj.mp <|
+      (congrFun (congrArg map ((galRestrict A K L B).apply_symm_apply σ)) P).trans hs⟩
+
+/-- All the `ramificationIdx` over a fixed maximal ideal are the same. -/
+theorem ramificationIdx_eq_of_isGalois [IsGalois K L] :
+    ramificationIdx (algebraMap A B) p P = ramificationIdx (algebraMap A B) p Q := by
+  rcases exists_map_eq_of_isGalois p P Q K L with ⟨σ, hs⟩
+  rw [← hs]
+  exact (ramificationIdx_map_eq p P σ).symm
+
+/-- All the `inertiaDeg` over a fixed maximal ideal are the same. -/
+theorem inertiaDeg_eq_of_isGalois [p.IsMaximal] [IsGalois K L] :
+    inertiaDeg p P = inertiaDeg p Q := by
+  rcases exists_map_eq_of_isGalois p P Q K L with ⟨σ, hs⟩
+  rw [← hs]
+  exact (inertiaDeg_map_eq p P σ).symm
+
+/-- The `ramificationIdxIn` is equal to any ramification index over the same ideal. -/
+theorem ramificationIdxIn_eq_ramificationIdx [IsGalois K L] :
+    ramificationIdxIn p B = ramificationIdx (algebraMap A B) p P := by
+  have h : ∃ P : Ideal B, P.IsPrime ∧ P.LiesOver p := ⟨P, hPp, hp⟩
+  obtain ⟨_, _⟩ := h.choose_spec
+  rw [ramificationIdxIn, dif_pos h]
+  exact ramificationIdx_eq_of_isGalois p h.choose P K L
+
+/-- The `inertiaDegIn` is equal to any ramification index over the same ideal. -/
+theorem inertiaDegIn_eq_inertiaDeg [p.IsMaximal] [IsGalois K L] :
+    inertiaDegIn p B = inertiaDeg p P := by
+  have h : ∃ P : Ideal B, P.IsPrime ∧ P.LiesOver p := ⟨P, hPp, hp⟩
+  obtain ⟨_, _⟩ := h.choose_spec
+  rw [inertiaDegIn, dif_pos h]
+  exact inertiaDeg_eq_of_isGalois p h.choose P K L
+
+end RamificationInertia
+
+section fundamental_identity
+
+variable {A : Type*} [CommRing A] [IsDedekindDomain A] {p : Ideal A} (hpb : p ≠ ⊥) [p.IsMaximal]
+  (B : Type*) [CommRing B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B]
+  (K L : Type*) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L]
+  [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L]
+  [FiniteDimensional K L]
+
+include hpb in
+/-- The form of the **fundamental identity** in the case of Galois extension. -/
+theorem ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn [IsGalois K L] :
+    (primesOver p B).ncard * (ramificationIdxIn p B * inertiaDegIn p B) = Module.finrank K L := by
+  have : FaithfulSMul A B := FaithfulSMul.of_field_isFractionRing A B K L
+  rw [← smul_eq_mul, ← coe_primesOverFinset hpb B, Set.ncard_coe_Finset, ← Finset.sum_const]
+  rw [← sum_ramification_inertia B p K L hpb]
+  apply Finset.sum_congr rfl
+  intro P hp
+  rw [← Finset.mem_coe, coe_primesOverFinset hpb B] at hp
+  obtain ⟨_, _⟩ := hp
+  rw [ramificationIdxIn_eq_ramificationIdx p P K L, inertiaDegIn_eq_inertiaDeg p P K L]
+
+end fundamental_identity
+
+end Ideal
diff --git a/Mathlib/RingTheory/Invariant.lean b/Mathlib/RingTheory/Invariant.lean
@@ -3,8 +3,6 @@ Copyright (c) 2024 Thomas Browning. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 -/
-import Mathlib.FieldTheory.Galois.Basic
-import Mathlib.RingTheory.Ideal.Over
 import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 
 /-!
@@ -79,6 +77,11 @@ theorem Algebra.isInvariant_of_isGalois [FiniteDimensional K L] [h : IsGalois K
     (FaithfulSMul.algebraMap_injective B L).eq_iff] at hk
   exact ⟨a, hk⟩
 
+/-- A variant of `Algebra.isInvariant_of_isGalois`, replacing `Gal(L/K)` by `Aut(B/A)`. -/
+theorem Algebra.isInvariant_of_isGalois' [FiniteDimensional K L] [IsGalois K L] :
+    Algebra.IsInvariant A B (B ≃ₐ[A] B) :=
+  ⟨fun b h ↦ (isInvariant_of_isGalois A K L B).1 b (fun g ↦ h (galRestrict A K L B g))⟩
+
 end Galois
 
 section transitivity