[Merged by Bors] - chore(RingTheory/Ideal/Norm/RelNorm): switch over to new definitions of ramificationIdx and inertiaDeg

Mathlib/RingTheory/DedekindDomain/Factorization.lean

@@ -5,7 +5,7 @@ Authors: María Inés de Frutos-Fernández
 -/
 module
 
-public import Mathlib.NumberTheory.RamificationInertia.Basic
+public import Mathlib.RingTheory.RamificationInertia.Basic
 public import Mathlib.Order.Filter.Cofinite
 public import Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
 
@@ -819,7 +819,7 @@ If `p` is a maximal ideal, then the lift of `p` in an extension is the product o
 over `p` to the power the ramification index.
 -/
 theorem Ideal.map_algebraMap_eq_finsetProd_pow {p : Ideal S} [p.IsMaximal] (hp : p ≠ 0) :
-    map (algebraMap S R) p = ∏ P ∈ p.primesOver R, P ^ p.ramificationIdx P := by
+    map (algebraMap S R) p = ∏ P ∈ p.primesOver R, P ^ P.ramificationIdx' S := by
   classical
   have h : map (algebraMap S R) p ≠ 0 := map_ne_bot_of_ne_bot hp
   rw [← finprod_heightOneSpectrum_factorization (I := p.map (algebraMap S R)) h]
@@ -830,8 +830,8 @@ theorem Ideal.map_algebraMap_eq_finsetProd_pow {p : Ideal S} [p.IsMaximal] (hp :
     ← Finset.prod_set_coe]
   · let _ : Fintype {v : HeightOneSpectrum R // v.asIdeal ∣ map (algebraMap S R) p} := hF
     refine Fintype.prod_equiv (equivPrimesOver _ hp) _ _ fun ⟨v, _⟩ ↦ ?_
-    simp [maxPowDividing_eq_pow_multiset_count _ h,
-      ramificationIdx_eq_factors_count h v.isPrime v.ne_bot]
+    have : v.asIdeal.LiesOver p := by rwa [Ideal.liesOver_iff_dvd_map v.2.ne_top]
+    simp [maxPowDividing_eq_pow_multiset_count _ h, ramificationIdx'_eq_factors_count p v h]
   · intro v hv
     simpa [maxPowDividing, Function.mem_mulSupport, IsPrime.ne_top _,
       Associates.count_ne_zero_iff_dvd h (irreducible v)] using hv

Mathlib/RingTheory/Ideal/Norm/RelNorm.lean

@@ -398,27 +398,26 @@ See `Ideal.relNorm_eq_pow_of_isMaximal` for a statement that does not require th
 be Galois.
 -/
 theorem relNorm_eq_pow_of_isPrime_isGalois [p.IsMaximal] [P.IsPrime]
-    [IsGalois (FractionRing R) (FractionRing S)] : relNorm R P = p ^ p.inertiaDeg P := by
+    [IsGalois (FractionRing R) (FractionRing S)] : relNorm R P = p ^ P.inertiaDeg' R := by
   have : P.IsMaximal := IsMaximal.of_liesOver_isMaximal P p
   let G := Gal(FractionRing S/FractionRing R)
   let := IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
   have := IsGaloisGroup.of_isFractionRing G R S (FractionRing R) (FractionRing S)
   by_cases hp : p = ⊥
-  · have h : p.inertiaDeg P ≠ 0 := Nat.ne_zero_iff_zero_lt.mpr <| inertiaDeg_pos p P
+  · have h : P.inertiaDeg' R ≠ 0 := (inertiaDeg'_pos P R).ne'
     have hP : P = ⊥ := by
       rw [hp] at hPp
       exact eq_bot_of_liesOver_bot R P
     rw [hp, hP, relNorm_bot, bot_pow]
-    rwa [hp, hP] at h
+    rwa [hP] at h
   obtain ⟨s, hs⟩ := exists_relNorm_eq_pow_of_isPrime P p
-  suffices s = p.inertiaDeg P by rwa [this] at hs
+  suffices s = P.inertiaDeg' R by rwa [this] at hs
   have h₀ : ∀ Q ∈ (p.primesOver S).toFinset,
-      relNorm R Q ^ ramificationIdx p Q = p ^ ((p.ramificationIdxIn S) * s) := by
+      relNorm R Q ^ Q.ramificationIdx' R = p ^ ((p.ramificationIdxIn S) * s) := by
     intro Q hQ
     rw [Set.mem_toFinset] at hQ
     have : Q.IsPrime := hQ.1
     have : Q.LiesOver p := hQ.2
-    rw [ramificationIdx_eq_ramificationIdx' p Q hp]
     rw [← ramificationIdxIn_eq_ramificationIdx p Q G]
     obtain ⟨σ, rfl⟩ := Ideal.exists_smul_eq_of_isGaloisGroup p P Q G
     rw [relNorm_smul, hs, ← pow_mul, mul_comm]
@@ -430,13 +429,12 @@ theorem relNorm_eq_pow_of_isPrime_isGalois [p.IsMaximal] [P.IsPrime]
     ← Set.ncard_eq_toFinset_card',
     ((IsLeftCancelMulZero.mul_left_cancel_of_ne_zero hp).pow_injective _).eq_iff,
     mul_right_inj' (IsDedekindDomain.primesOver_ncard_ne_zero p S),
-    mul_right_inj' (ramificationIdxIn_ne_zero G),
-    inertiaDegIn_eq_inertiaDeg p P G, ← inertiaDeg_eq_inertiaDeg' p P] at h
+    mul_right_inj' (ramificationIdxIn_ne_zero G), inertiaDegIn_eq_inertiaDeg p P G] at h
   rw [one_eq_top]
   exact IsMaximal.ne_top inferInstance
 
 theorem relNorm_eq_pow_of_isMaximal [PerfectField (FractionRing R)] [P.IsMaximal] [p.IsMaximal] :
-    relNorm R P = p ^ p.inertiaDeg P := by
+    relNorm R P = p ^ P.inertiaDeg' R := by
   let T := Ring.NormalClosure R S
   obtain ⟨Q, hQ₁, hQ₂⟩ : ∃ Q : Ideal T, Q.IsMaximal ∧ Q.LiesOver P :=
     exists_maximal_ideal_liesOver_of_isIntegral P
@@ -445,8 +443,7 @@ theorem relNorm_eq_pow_of_isMaximal [PerfectField (FractionRing R)] [P.IsMaximal
   have : IsGalois (FractionRing S) (FractionRing T) :=
     IsGalois.tower_top_of_isGalois (FractionRing R) (FractionRing S) (FractionRing T)
   rwa [← relNorm_relNorm R S, relNorm_eq_pow_of_isPrime_isGalois Q P, map_pow,
-    inertiaDeg_algebra_tower p P Q, pow_mul, pow_left_inj] at h
-  exact Nat.ne_zero_iff_zero_lt.mpr <| inertiaDeg_pos P Q
+    inertiaDeg'_tower (R := R) P Q, pow_mul, pow_left_inj (inertiaDeg'_pos Q S).ne'] at h
 
 end relNorm_prime
 
@@ -477,7 +474,8 @@ theorem absNorm_relNorm [PerfectField (FractionRing R)] (I : Ideal S) :
     have : Fact (p.Prime) := ⟨Nat.absNorm_under_prime _⟩
     have hp : Prime (p : ℤ) := Nat.prime_iff_prime_int.mp <| Nat.absNorm_under_prime _
     rw [relNorm_eq_pow_of_isMaximal Q P, map_pow, absNorm_eq_pow_inertiaDeg Q hp,
-      absNorm_eq_pow_inertiaDeg P hp, inertiaDeg_algebra_tower (span {(p : ℤ)}) P Q, pow_mul]
+      absNorm_eq_pow_inertiaDeg P hp, inertiaDeg_algebra_tower (span {(p : ℤ)}) P Q, pow_mul,
+      ← inertiaDeg_eq_inertiaDeg' P]
 
 theorem relNorm_int (I : Ideal S) :
     relNorm ℤ I = Ideal.span {(absNorm I : ℤ)} := by

Mathlib/RingTheory/RamificationInertia/Ramification.lean

@@ -122,14 +122,11 @@ theorem ramificationIdx'_eq [q.LiesOver p] [q.IsPrime] :
   rw [ramificationIdx'_def, over_def q p]
 
 open Localization IsLocalization.AtPrime in
-theorem ramificationIdx_eq_ramificationIdx'
-    [IsDomain R] [IsDedekindDomain S] [Module.IsTorsionFree R S]
-    [q.LiesOver p] [hq : q.IsPrime] (hp : p ≠ ⊥) :
+theorem ramificationIdx_eq_ramificationIdx'' [IsDedekindDomain S]
+    [q.LiesOver p] [hq : q.IsPrime] (hpS : p.map (algebraMap R S) ≠ ⊥) :
     p.ramificationIdx q = q.ramificationIdx' R := by
-  have : p.IsPrime := isPrime_of_liesOver q p
-  have hq' : q ≠ ⊥ := ne_bot_of_liesOver_of_ne_bot hp q
+  have hq' : q ≠ ⊥ := ne_bot_of_le_ne_bot hpS (map_le_of_le_comap (q.over_def p).le)
   have : q.IsMaximal := hq.isMaximal hq'
-  have hpS : p.map (algebraMap R S) ≠ ⊥ := map_ne_bot_of_ne_bot hp
   obtain ⟨I, hqI, h⟩ := Ideal.eq_prime_pow_mul_coprime hpS q
   replace hqI : ¬ I ≤ q := by
     contrapose! hqI
@@ -142,6 +139,23 @@ theorem ramificationIdx_eq_ramificationIdx'
   have hSq := isDiscreteValuationRing_of_dedekind_domain S hq' (Localization.AtPrime q)
   rw [ramificationIdx'_eq p q, h, hSq.length_quotient_pow_maximalIdeal, ENat.toNat_coe]
 
+theorem ramificationIdx_eq_ramificationIdx' [IsDomain R] [IsDedekindDomain S]
+    [Module.IsTorsionFree R S] [q.LiesOver p] [hq : q.IsPrime] (hp : p ≠ ⊥) :
+    p.ramificationIdx q = q.ramificationIdx' R := by
+  have hpS : p.map (algebraMap R S) ≠ ⊥ := map_ne_bot_of_ne_bot hp
+  exact ramificationIdx_eq_ramificationIdx'' p q hpS
+
+open UniqueFactorizationMonoid in
+theorem IsDedekindDomain.ramificationIdx'_eq_factors_count [IsDedekindDomain S]
+    [q.LiesOver p] (hp0 : p.map (algebraMap R S) ≠ ⊥) :
+    q.ramificationIdx' R = (factors (p.map (algebraMap R S))).count q := by
+  by_cases hq : q.IsPrime; swap
+  · rw [ramificationIdx'_of_not_isPrime q R hq, eq_comm, Multiset.count_eq_zero]
+    contrapose! hq
+    exact isPrime_of_prime (prime_of_factor q hq)
+  have hq0 : q ≠ ⊥ := ne_bot_of_le_ne_bot hp0 (map_le_of_le_comap (q.over_def p).le)
+  rw [← ramificationIdx_eq_ramificationIdx'' p q hp0, ramificationIdx_eq_factors_count hp0 ‹_› hq0]
+
 /-- See `ramificationIdx'_tower` for a version that does not assume primality. -/
 theorem ramificationIdx'_tower' [q.IsPrime] [r.IsPrime] [r.LiesOver q]
     [Algebra (Localization.AtPrime q) (Localization.AtPrime r)]