feat(RingTheory/RamificationInertia/Ramification): positivity of ramification index (leanprover-community#39977)

This PR proves positivity of the new definition of ramification index.

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

Author: tb65536

Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean

@@ -232,3 +232,8 @@ noncomputable def PrimeSpectrum.preimageHomeomorphFiber (R S : Type*) [CommRing
       simp only [Equiv.toFun_as_coe, RelIso.coe_fn_toEquiv, Homeomorph.symm_apply_apply]
       simp
     continuous_invFun := H.continuous }
+
+@[simp]
+theorem PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply (q : PrimeSpectrum (p.Fiber S)) :
+    (primesOverOrderIsoFiber R S p).symm q = q.1.comap Algebra.TensorProduct.includeRight :=
+  rfl

Mathlib/RingTheory/RamificationInertia/Ramification.lean

@@ -6,9 +6,9 @@ Authors: Thomas Browning
 module
 
 public import Mathlib.NumberTheory.RamificationInertia.Ramification
-public import Mathlib.RingTheory.Flat.Localization
 public import Mathlib.RingTheory.LocalRing.Length
 public import Mathlib.RingTheory.LocalRing.ResidueField.Instances
+public import Mathlib.RingTheory.QuasiFinite.Basic
 public import Mathlib.RingTheory.Unramified.LocalRing
 
 /-!
@@ -62,6 +62,24 @@ theorem ramificationIdx'_def [q.IsPrime] :
 theorem ramificationIdx'_of_not_isPrime (hq : ¬ q.IsPrime) : q.ramificationIdx' R = 0 :=
   dif_neg hq
 
+theorem ramificationIdx'_pos [q.IsPrime] [Module.Finite R S] : 0 < q.ramificationIdx' R := by
+  let p := q.under R
+  let Sq := Localization.AtPrime q
+  rw [ramificationIdx'_def]
+  apply ENat.toNat_pos
+  · rw [← pos_iff_ne_zero, Module.length_pos_iff, Submodule.Quotient.nontrivial_iff,
+      IsScalarTower.algebraMap_eq R S, ← map_map, ← lt_top_iff_ne_top]
+    grw [map_mono map_comap_le, Localization.AtPrime.map_eq_maximalIdeal]
+    exact (IsLocalRing.maximalIdeal.isMaximal _).lt_top
+  · let r := PrimeSpectrum.primesOverOrderIsoFiber R S p (primesOver.mk p q)
+    have : q = r.1.comap Algebra.TensorProduct.includeRight := by
+      rw [← PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply, OrderIso.symm_apply_apply]
+    let := Localization.AtPrime.algebraOfLiesOver p (r.1.comap Algebra.TensorProduct.includeRight)
+    have : IsArtinianRing (Sq ⧸ map (algebraMap R Sq) p) := by
+      convert (Fiber.localizationAlgEquivQuotient p r.1).toRingEquiv.isArtinianRing
+    rwa [Module.length_eq_of_surjective (R := Sq ⧸ p.map (algebraMap R Sq)) Quotient.mk_surjective,
+      Module.length_ne_top_iff, ← isArtinianRing_iff_isFiniteLength]
+
 theorem ramificationIdx'_eq_one [q.IsPrime] [Algebra.EssFiniteType R S]
     [Algebra.IsUnramifiedAt R q] : q.ramificationIdx' R = 1 := by
   let p := q.under R