feat: Ideal.ramificationIdx_mul_inertiaDeg_of_isLocalRing (#29729)

We add the special case `Ideal.ramificationIdx_mul_inertiaDeg_of_isLocalRing` of `Ideal.sum_ramification_inertia` in the local (DVR) case: the product of the ramification index and the inertia degree equals the degree of the field extension.

Also make the argument `p` implicit in `Ideal.sum_ramification_inertia`.

Co-authored-by: Matthew Jasper <mjjasper1@gmail.com>
Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com>

Author: 3 people

Mathlib/NumberTheory/RamificationInertia/Basic.lean

@@ -872,7 +872,7 @@ is maximal. -/
 theorem sum_ramification_inertia (K L : Type*) [Field K] [Field L] [IsDedekindDomain R]
     [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L]
     [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S]
-    [p.IsMaximal] (hp0 : p ≠ ⊥) :
+    {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) :
     ∑ P ∈ primesOverFinset p S,
         ramificationIdx (algebraMap R S) p P * inertiaDeg p P = finrank K L := by
   set e := ramificationIdx (algebraMap R S) p
@@ -894,6 +894,18 @@ theorem sum_ramification_inertia (K L : Type*) [Field K] [Field L] [IsDedekindDo
       algebraMap_injective_of_field_isFractionRing R S K L, le_bot_iff]
   · exact finrank_quotient_map p K L
 
+/-- `Ideal.sum_ramification_inertia`, in the local (DVR) case. -/
+lemma ramificationIdx_mul_inertiaDeg_of_isLocalRing
+    (K L : Type*) [Field K] [Field L] [IsLocalRing S]
+    [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [Algebra S L]
+    [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L]
+    [IsScalarTower R K L] [Module.Finite R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) :
+    ramificationIdx (algebraMap R S) p (IsLocalRing.maximalIdeal S) *
+      p.inertiaDeg (IsLocalRing.maximalIdeal S) = Module.finrank K L := by
+  have := FaithfulSMul.of_field_isFractionRing R S K L
+  simp_rw [← sum_ramification_inertia S K L hp0, IsLocalRing.primesOverFinset_eq S hp0,
+    Finset.sum_singleton]
+
 end FactorsMap
 
 section tower

Mathlib/NumberTheory/RamificationInertia/Galois.lean

@@ -198,7 +198,7 @@ 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]
+  rw [← sum_ramification_inertia B K L hpb]
   apply Finset.sum_congr rfl
   intro P hp
   rw [← Finset.mem_coe, coe_primesOverFinset hpb B] at hp

Mathlib/RingTheory/DedekindDomain/Basic.lean

@@ -154,3 +154,12 @@ instance (priority := 100) IsPrincipalIdealRing.isDedekindDomain
     IsDedekindDomain A :=
   { PrincipalIdealRing.isNoetherianRing, Ring.DimensionLEOne.principal_ideal_ring A,
     UniqueFactorizationMonoid.instIsIntegrallyClosed with }
+
+variable {R} in
+theorem IsLocalRing.primesOver_eq [IsLocalRing A] [IsDedekindDomain A] [Algebra R A]
+    [FaithfulSMul R A] [Module.Finite R A] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) :
+    Ideal.primesOver p A = {IsLocalRing.maximalIdeal A} := by
+  refine Set.eq_singleton_iff_nonempty_unique_mem.mpr ⟨?_, fun P hP ↦ ?_⟩
+  · obtain ⟨w', hmax, hover⟩ := Ideal.exists_ideal_liesOver_maximal_of_isIntegral p A
+    exact ⟨w', hmax.isPrime, hover⟩
+  · exact IsLocalRing.eq_maximalIdeal <| hP.1.isMaximal (Ideal.ne_bot_of_mem_primesOver hp0 hP)

Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

@@ -1011,6 +1011,12 @@ theorem coe_primesOverFinset : primesOverFinset p B = primesOver p B := by
     (fun ⟨hPp, h⟩ => ⟨hPp, ⟨hpm.eq_of_le (comap_ne_top _ hPp.ne_top) (le_comap_of_map_le h)⟩⟩)
     (fun ⟨hPp, h⟩ => ⟨hPp, map_le_of_le_comap h.1.le⟩)
 
+variable {R} (A) in
+theorem IsLocalRing.primesOverFinset_eq [IsLocalRing A] [IsDedekindDomain A]
+    [Algebra R A] [FaithfulSMul R A] [Module.Finite R A] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) :
+    primesOverFinset p A = {IsLocalRing.maximalIdeal A} := by
+  rw [← Finset.coe_eq_singleton, coe_primesOverFinset hp0, IsLocalRing.primesOver_eq A hp0]
+
 namespace IsDedekindDomain.HeightOneSpectrum
 
 /--