The fundamental identity in the quotient-based formulation

Mathlib's Ideal.sum_ramification_inertia_eq_finrank states the fundamental identity ∑ e · f = [L : K] for the localization-based Ideal.ramificationIdx and Ideal.inertiaDeg, summed over the subtype p.primesOver S. The rest of this development works with the quotient-based Ideal.ramificationIdx' and Ideal.inertiaDeg' over the finite set IsDedekindDomain.primesOverFinset, so this file transports the identity to that form and records the resulting bound e ≤ [L : K] for a single prime.

theorem Ideal.sum_ramificationIdx'_mul_inertiaDeg' {R : Type u_1} {S : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing S] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [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] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : ∑ P ∈ IsDedekindDomain.primesOverFinset p S, p.ramificationIdx' P * p.inertiaDeg' P = Module.finrank K L

The fundamental identity ∑ e · f = [L : K] for the quotient-based ramification index and inertia degree, summed over the finite set of primes above a nonzero maximal ideal p.

theorem Ideal.ramificationIdx'_le_finrank {R : Type u_1} {S : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing S] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [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] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) (P : Ideal S) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver p] : p.ramificationIdx' P ≤ Module.finrank K L

The quotient-based ramification index of a prime above a nonzero maximal ideal is bounded by the degree of the extension of fraction fields.