refactor(RingTheory/RamificationInertia/Inertia): remove last occurances of inertiaDeg_eq_inertiaDeg' (leanprover-community#41320)

This PR adds a bit more API for `RingTheory/RamificationInertia/Inertia` in order to remove the last occurances of `inertiaDeg_eq_inertiaDeg'`.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/NumberTheory/NumberField/Completion/Ramification.lean

@@ -6,7 +6,7 @@ Authors: Salvatore Mercuri
 module
 
 public import Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances
-public import Mathlib.NumberTheory.RamificationInertia.Basic
+public import Mathlib.RingTheory.RamificationInertia.Inertia
 
 /-!
 # Ramification theory of completions of number fields
@@ -86,16 +86,15 @@ variable (w)
 open scoped Classical in
 /-- The inertia degree of `w` over `v`. -/
 protected noncomputable def inertiaDeg : ℕ :=
-  if _ : w.1.LiesOver v.1 then (⊥ : Ideal v.Completion).inertiaDeg (⊥ : Ideal w.Completion) else 0
+  if _ : w.1.LiesOver v.1 then (⊥ : Ideal w.Completion).inertiaDeg' v.Completion else 0
 
 theorem inertiaDeg_of_liesOver [w.1.LiesOver v.1] :
-    v.inertiaDeg w = (⊥ : Ideal v.Completion).inertiaDeg (⊥ : Ideal w.Completion) := by
+    v.inertiaDeg w = (⊥ : Ideal w.Completion).inertiaDeg' v.Completion := by
   simp only [InfinitePlace.inertiaDeg, dif_pos]
 
 theorem inertiaDeg_eq_finrank [w.1.LiesOver v.1] :
     v.inertiaDeg w = Module.finrank v.Completion w.Completion := by
-  simp only [inertiaDeg_of_liesOver, Ideal.inertiaDeg, Ideal.comap_bot_of_injective _ <|
-    FaithfulSMul.algebraMap_injective v.Completion w.Completion]
+  rw [inertiaDeg_of_liesOver, Ideal.inertiaDeg'_eq_of_isMaximal ⊥]
   exact Algebra.finrank_eq_of_equiv_equiv (RingEquiv.quotientBot v.Completion)
     (RingEquiv.quotientBot w.Completion) (by ext; simp [RingHom.algebraMap_toAlgebra])
 

Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean

@@ -218,7 +218,7 @@ theorem inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply (hp : ¬ p ∣
     apply Ideal.primesOver.isMaximal
   have := liesOver_primesOverSpanEquivMonicFactorsMod_symm hp hQ
   rw [primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span,
-    ← inertiaDeg_eq_inertiaDeg' (span {(p : ℤ)}), inertiaDeg_algebraMap,
+    inertiaDeg'_eq_of_isMaximal (span {(p : ℤ)}),
     ← finrank_quotient_span_eq_natDegree]
   refine Algebra.finrank_eq_of_equiv_equiv (Int.quotientSpanNatEquivZMod p) ?_ (by ext; simp)
   exact (ZModXQuotSpanEquivQuotSpanPair hp hQ).symm

Mathlib/NumberTheory/RamificationInertia/HilbertTheory.lean

@@ -283,7 +283,6 @@ private lemma instances (hp : p ≠ ⊥) :
   exact ⟨inst₁, inst₂, inst₃, inst₄, inst₅, Ideal.ne_bot_of_liesOver_of_ne_bot hp 𝓟D⟩
 
 variable [FiniteDimensional K L] [Ring.HasFiniteQuotients A] [𝓟D.IsMaximal] [P.IsMaximal]
-  [p.IsMaximal]
 
 include K L D P in
 private lemma ramificationIdxIn_eq_and_inertiaDegIn_eq (hp : p ≠ ⊥) :
@@ -297,8 +296,7 @@ private lemma ramificationIdxIn_eq_and_inertiaDegIn_eq (hp : p ≠ ⊥) :
     exact 𝓟D.ramificationIdx_above_le P
   · rw [inertiaDegIn_eq_inertiaDeg p P Gal(L/K),
       inertiaDegIn_eq_inertiaDeg _ P (stabilizer Gal(L/K) P)]
-    rw [← inertiaDeg_eq_inertiaDeg' p, ← inertiaDeg_eq_inertiaDeg' 𝓟D]
-    exact inertiaDeg_le_inertiaDeg p 𝓟D P
+    exact inertiaDeg'_above_le 𝓟D P
   · have := ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn 𝓟D B (stabilizer Gal(L/K) P)
     rw [primesOver_eq_singleton K L P D 𝓞D, Set.ncard_singleton, one_mul] at this
     rw [this, IsGaloisGroup.card_eq_finrank (stabilizer Gal(L/K) P) D L,

Mathlib/RingTheory/RamificationInertia/Inertia.lean

@@ -76,22 +76,36 @@ theorem inertiaDeg'_eq [q.LiesOver p] [q.IsPrime] [p.IsPrime]
   subst this
   exact inertiaDeg'_def q R
 
-theorem inertiaDeg_eq_inertiaDeg' [q.LiesOver p] [p.IsMaximal] [q.IsMaximal] :
-    p.inertiaDeg q = q.inertiaDeg' R := by
+theorem inertiaDeg'_eq_of_isFractionRing [q.LiesOver p] [p.IsPrime] [q.IsPrime]
+    (K L : Type*) [Field K] [Field L]
+    [Algebra (R ⧸ p) K] [IsFractionRing (R ⧸ p) K]
+    [Algebra (S ⧸ q) L] [IsFractionRing (S ⧸ q) L]
+    [Algebra R K] [IsScalarTower R (R ⧸ p) K]
+    [Algebra S L] [IsScalarTower S (S ⧸ q) L]
+    [Algebra R L] [IsScalarTower R S L]
+    [Algebra K L] [IsScalarTower R K L] :
+    q.inertiaDeg' R = Module.finrank K L := by
+  let := Localization.AtPrime.algebraOfLiesOver p q
+  rw [inertiaDeg'_eq p q]
+  apply Algebra.finrank_eq_of_equiv_equiv
+    (IsFractionRing.algEquivOfAlgEquiv (R := R) (A := R ⧸ p) (K := p.ResidueField) (L := K) .refl)
+    (IsFractionRing.algEquivOfAlgEquiv (R := S) (A := S ⧸ q) (K := q.ResidueField) (L := L) .refl)
+  apply IsFractionRing.ringHom_ext (A := R ⧸ p)
+  intro x
+  obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
+  simp [← IsScalarTower.algebraMap_apply R p.ResidueField q.ResidueField,
+    IsScalarTower.algebraMap_apply R S q.ResidueField,
+    ← IsScalarTower.algebraMap_apply R K L, ← IsScalarTower.algebraMap_apply R S L]
+
+theorem inertiaDeg'_eq_of_isMaximal [q.LiesOver p] [p.IsMaximal] [q.IsMaximal] :
+    q.inertiaDeg' R = Module.finrank (R ⧸ p) (S ⧸ q) := by
   let : Field (R ⧸ p) := Quotient.field p
   let : Field (S ⧸ q) := Quotient.field q
-  let := Localization.AtPrime.algebraOfLiesOver p q
-  rw [inertiaDeg'_eq p q, inertiaDeg_algebraMap]
-  let f := (algebraMap (S ⧸ q) q.ResidueField).comp (algebraMap (R ⧸ p) (S ⧸ q))
-  let g := (algebraMap p.ResidueField q.ResidueField).comp (algebraMap (R ⧸ p) p.ResidueField)
-  have h : f = g := by ext; simp [f, g, ← IsScalarTower.algebraMap_apply]
-  let : Algebra (R ⧸ p) q.ResidueField := f.toAlgebra
-  have : IsScalarTower (R ⧸ p) (S ⧸ q) q.ResidueField := IsScalarTower.of_algebraMap_eq' rfl
-  have : IsScalarTower (R ⧸ p) p.ResidueField q.ResidueField := IsScalarTower.of_algebraMap_eq' h
-  rw [← mul_one (Module.finrank (R ⧸ p) (S ⧸ q)),
-    ← Module.finrank_of_bijective_algebraMap (bijective_algebraMap_quotient_residueField q),
-    Module.finrank_mul_finrank, ← Module.finrank_mul_finrank (R ⧸ p) p.ResidueField q.ResidueField,
-    Module.finrank_of_bijective_algebraMap (bijective_algebraMap_quotient_residueField p), one_mul]
+  exact inertiaDeg'_eq_of_isFractionRing p q (R ⧸ p) (S ⧸ q)
+
+theorem inertiaDeg_eq_inertiaDeg' [q.LiesOver p] [p.IsMaximal] [q.IsMaximal] :
+    p.inertiaDeg q = q.inertiaDeg' R := by
+  rw [inertiaDeg_algebraMap, inertiaDeg'_eq_of_isMaximal p q]
 
 theorem inertiaDeg'_tower [r.LiesOver q] :
     r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S := by
@@ -105,6 +119,24 @@ theorem inertiaDeg'_tower [r.LiesOver q] :
     apply Module.finrank_mul_finrank
   · rw [inertiaDeg'_of_not_isPrime r R hr, inertiaDeg'_of_not_isPrime r S hr, mul_zero]
 
+theorem inertiaDeg'_below_dvd [r.LiesOver q] :
+    q.inertiaDeg' R ∣ r.inertiaDeg' R := by
+  use r.inertiaDeg' S
+  rw [← inertiaDeg'_tower]
+
+theorem inertiaDeg'_above_dvd [r.LiesOver q] :
+    r.inertiaDeg' S ∣ r.inertiaDeg' R := by
+  use q.inertiaDeg' R
+  rw [mul_comm, ← inertiaDeg'_tower]
+
+theorem inertiaDeg'_below_le [r.IsPrime] [r.LiesOver q] [Module.Finite R T] :
+    q.inertiaDeg' R ≤ r.inertiaDeg' R :=
+  Nat.le_of_dvd (r.inertiaDeg'_pos R) (q.inertiaDeg'_below_dvd r)
+
+theorem inertiaDeg'_above_le [r.IsPrime] [r.LiesOver q] [Module.Finite R T] :
+    r.inertiaDeg' S ≤ r.inertiaDeg' R :=
+  Nat.le_of_dvd (r.inertiaDeg'_pos R) (q.inertiaDeg'_above_dvd r)
+
 variable (R) in
 open Pointwise in
 @[simp]