Documentation

Mathlib.RingTheory.RamificationInertia.Ramification

Ramification index #

Let S/R be an extension of rings, and let q be a prime ideal of S lying over a prime ideal p of R. Let Sq be the localization of S and q, and let pSq be the image of p in Sq. Then the ramification index of q over R is defined to be the length of the quotient Sq/pSq as an Sq-module.

Main definitions #

Main statements #

source
noncomputable def Ideal.ramificationIdx {S : Type u_1} [CommRing S] (q : Ideal S) (R : Type u_2) [CommRing R] [Algebra R S] :
ℕ

Let S/R be an extension of rings, and let q be a prime ideal of S lying over a prime ideal p of R. Let Sq be the localization of S and q, and let pSq be the image of p in Sq. Then the ramification index of q over R is defined to be the length of the quotient Sq/pSq as an Sq-module.

When q is not prime, we use a junk value of 0.

This will eventually replace the existing definition of Ideal.ramificationIdx'.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Ideal.ramificationIdx_def {S : Type u_1} [CommRing S] (q : Ideal S) (R : Type u_2) [CommRing R] [Algebra R S] [q.IsPrime] :
    q.ramificationIdx R = (Module.length (Localization.AtPrime q) (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q))).toNat
    source
    @[deprecated Ideal.ramificationIdx_def (since := "2026-07-01")]
    theorem Ideal.ramificationIdx'_def {S : Type u_1} [CommRing S] (q : Ideal S) (R : Type u_2) [CommRing R] [Algebra R S] [q.IsPrime] :
    q.ramificationIdx R = (Module.length (Localization.AtPrime q) (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q))).toNat

    Alias of Ideal.ramificationIdx_def.

    source
    theorem Ideal.ramificationIdx_of_not_isPrime {S : Type u_1} [CommRing S] (q : Ideal S) (R : Type u_2) [CommRing R] [Algebra R S] (hq : ¬q.IsPrime) :
    q.ramificationIdx R = 0
    source
    @[deprecated Ideal.ramificationIdx_of_not_isPrime (since := "2026-07-01")]
    theorem Ideal.ramificationIdx'_of_not_isPrime {S : Type u_1} [CommRing S] (q : Ideal S) (R : Type u_2) [CommRing R] [Algebra R S] (hq : ¬q.IsPrime) :
    q.ramificationIdx R = 0

    Alias of Ideal.ramificationIdx_of_not_isPrime.

    source
    theorem Ideal.ramificationIdx_pos {S : Type u_1} [CommRing S] (q : Ideal S) (R : Type u_2) [CommRing R] [Algebra R S] [q.IsPrime] [Module.Finite R S] :
    0 < q.ramificationIdx R
    source
    @[deprecated Ideal.ramificationIdx_pos (since := "2026-07-01")]
    theorem Ideal.ramificationIdx'_pos {S : Type u_1} [CommRing S] (q : Ideal S) (R : Type u_2) [CommRing R] [Algebra R S] [q.IsPrime] [Module.Finite R S] :
    0 < q.ramificationIdx R

    Alias of Ideal.ramificationIdx_pos.

    source
    theorem Ideal.ramificationIdx_eq_one {S : Type u_1} [CommRing S] (q : Ideal S) (R : Type u_2) [CommRing R] [Algebra R S] [q.IsPrime] [Algebra.EssFiniteType R S] [Algebra.IsUnramifiedAt R q] :
    q.ramificationIdx R = 1
    source
    @[deprecated Ideal.ramificationIdx_eq_one (since := "2026-07-01")]
    theorem Ideal.ramificationIdx'_eq_one {S : Type u_1} [CommRing S] (q : Ideal S) (R : Type u_2) [CommRing R] [Algebra R S] [q.IsPrime] [Algebra.EssFiniteType R S] [Algebra.IsUnramifiedAt R q] :
    q.ramificationIdx R = 1

    Alias of Ideal.ramificationIdx_eq_one.

    source
    theorem Ideal.ramificationIdx_eq_one_iff {S : Type u_1} [CommRing S] {q : Ideal S} {R : Type u_2} [CommRing R] [Algebra R S] [q.IsPrime] [Algebra.EssFiniteType R S] [Algebra.IsIntegral R S] [PerfectField (under R q).ResidueField] :
    q.ramificationIdx R = 1 ↔ Algebra.IsUnramifiedAt R q
    source
    @[deprecated Ideal.ramificationIdx_eq_one_iff (since := "2026-07-01")]
    theorem Ideal.ramificationIdx'_eq_one_iff {S : Type u_1} [CommRing S] {q : Ideal S} {R : Type u_2} [CommRing R] [Algebra R S] [q.IsPrime] [Algebra.EssFiniteType R S] [Algebra.IsIntegral R S] [PerfectField (under R q).ResidueField] :
    q.ramificationIdx R = 1 ↔ Algebra.IsUnramifiedAt R q

    Alias of Ideal.ramificationIdx_eq_one_iff.

    source
    theorem Ideal.ramificationIdx_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [q.LiesOver p] [q.IsPrime] :
    q.ramificationIdx R = (Module.length (Localization.AtPrime q) (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) p)).toNat
    source
    @[deprecated Ideal.ramificationIdx_eq (since := "2026-07-01")]
    theorem Ideal.ramificationIdx'_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [q.LiesOver p] [q.IsPrime] :
    q.ramificationIdx R = (Module.length (Localization.AtPrime q) (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) p)).toNat

    Alias of Ideal.ramificationIdx_eq.

    source
    theorem Ideal.ramificationIdx'_eq_ramificationIdx' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [IsDedekindDomain S] [q.LiesOver p] [hq : q.IsPrime] (hpS : map (algebraMap R S) p ≠ ⊥) :
    p.ramificationIdx' q = q.ramificationIdx R
    source
    @[deprecated Ideal.ramificationIdx'_eq_ramificationIdx' (since := "2026-07-01")]
    theorem Ideal.ramificationIdx_eq_ramificationIdx'' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [IsDedekindDomain S] [q.LiesOver p] [hq : q.IsPrime] (hpS : map (algebraMap R S) p ≠ ⊥) :
    p.ramificationIdx' q = q.ramificationIdx R

    Alias of Ideal.ramificationIdx'_eq_ramificationIdx'.

    source
    theorem Ideal.ramificationIdx'_eq_ramificationIdx {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [IsDomain R] [IsDedekindDomain S] [Module.IsTorsionFree R S] [q.LiesOver p] [hq : q.IsPrime] (hp : p ≠ ⊥) :
    p.ramificationIdx' q = q.ramificationIdx R
    source
    @[deprecated Ideal.ramificationIdx'_eq_ramificationIdx (since := "2026-07-01")]
    theorem Ideal.ramificationIdx_eq_ramificationIdx' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [IsDomain R] [IsDedekindDomain S] [Module.IsTorsionFree R S] [q.LiesOver p] [hq : q.IsPrime] (hp : p ≠ ⊥) :
    p.ramificationIdx' q = q.ramificationIdx R

    Alias of Ideal.ramificationIdx'_eq_ramificationIdx.

    source
    theorem Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [IsDedekindDomain S] [q.LiesOver p] (hp0 : map (algebraMap R S) p ≠ ⊥) :
    q.ramificationIdx R = Multiset.count q (UniqueFactorizationMonoid.factors (map (algebraMap R S) p))
    source
    theorem Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [IsDedekindDomain S] [q.LiesOver p] (hp0 : map (algebraMap R S) p ≠ ⊥) :
    q.ramificationIdx R = Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (algebraMap R S) p))
    source
    theorem Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [IsDedekindDomain S] [q.IsPrime] [q.LiesOver p] (hp : map (algebraMap R S) p ≠ ⊥) :
    q.ramificationIdx R = multiplicity q (map (algebraMap R S) p)
    source
    theorem Ideal.ramificationIdx_tower' {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T) [q.IsPrime] [r.IsPrime] [r.LiesOver q] [Algebra (Localization.AtPrime q) (Localization.AtPrime r)] [Localization.AtPrime.IsLiesOverAlgebra q r] [Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)] :
    r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S

    See ramificationIdx_tower for a version that does not assume primality.

    source
    @[deprecated Ideal.ramificationIdx_tower' (since := "2026-07-01")]
    theorem Ideal.ramificationIdx'_tower' {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T) [q.IsPrime] [r.IsPrime] [r.LiesOver q] [Algebra (Localization.AtPrime q) (Localization.AtPrime r)] [Localization.AtPrime.IsLiesOverAlgebra q r] [Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)] :
    r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S

    Alias of Ideal.ramificationIdx_tower'.

    See ramificationIdx_tower for a version that does not assume primality.

    source
    theorem Ideal.ramificationIdx_tower {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T) [r.LiesOver q] [Module.Flat S T] :
    r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S

    See ramificationIdx_tower' for a version that only assumes local flatness.

    source
    @[deprecated Ideal.ramificationIdx_tower (since := "2026-07-01")]
    theorem Ideal.ramificationIdx'_tower {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T) [r.LiesOver q] [Module.Flat S T] :
    r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S

    Alias of Ideal.ramificationIdx_tower.

    See ramificationIdx_tower' for a version that only assumes local flatness.

    source
    theorem Ideal.ramificationIdx_below_dvd {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T) [r.LiesOver q] [Module.Flat S T] :
    q.ramificationIdx R ∣ r.ramificationIdx R
    source
    @[deprecated Ideal.ramificationIdx_below_dvd (since := "2026-07-01")]
    theorem Ideal.ramificationIdx'_below_dvd {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T) [r.LiesOver q] [Module.Flat S T] :
    q.ramificationIdx R ∣ r.ramificationIdx R

    Alias of Ideal.ramificationIdx_below_dvd.

    source
    theorem Ideal.ramificationIdx_above_dvd {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T) [r.LiesOver q] [Module.Flat S T] :
    r.ramificationIdx S ∣ r.ramificationIdx R
    source
    @[deprecated Ideal.ramificationIdx_above_dvd (since := "2026-07-01")]
    theorem Ideal.ramificationIdx'_above_dvd {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T) [r.LiesOver q] [Module.Flat S T] :
    r.ramificationIdx S ∣ r.ramificationIdx R

    Alias of Ideal.ramificationIdx_above_dvd.

    source
    theorem Ideal.ramificationIdx_below_le {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T) [r.IsPrime] [r.LiesOver q] [Module.Finite R T] [Module.Flat S T] :
    q.ramificationIdx R ≤ r.ramificationIdx R
    source
    @[deprecated Ideal.ramificationIdx_below_le (since := "2026-07-01")]
    theorem Ideal.ramificationIdx'_below_le {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T) [r.IsPrime] [r.LiesOver q] [Module.Finite R T] [Module.Flat S T] :
    q.ramificationIdx R ≤ r.ramificationIdx R

    Alias of Ideal.ramificationIdx_below_le.

    source
    theorem Ideal.ramificationIdx_above_le {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T) [r.IsPrime] [r.LiesOver q] [Module.Finite R T] [Module.Flat S T] :
    r.ramificationIdx S ≤ r.ramificationIdx R
    source
    @[deprecated Ideal.ramificationIdx_above_le (since := "2026-07-01")]
    theorem Ideal.ramificationIdx'_above_le {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T) [r.IsPrime] [r.LiesOver q] [Module.Finite R T] [Module.Flat S T] :
    r.ramificationIdx S ≤ r.ramificationIdx R

    Alias of Ideal.ramificationIdx_above_le.

    source
    @[simp]
    theorem Ideal.ramificationIdx_smul (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (q : Ideal S) {G : Type u_4} [Group G] [MulSemiringAction G S] [SMulCommClass G R S] (g : G) :
    (g • q).ramificationIdx R = q.ramificationIdx R
    source
    @[deprecated Ideal.ramificationIdx_smul (since := "2026-07-01")]
    theorem Ideal.ramificationIdx'_smul (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (q : Ideal S) {G : Type u_4} [Group G] [MulSemiringAction G S] [SMulCommClass G R S] (g : G) :
    (g • q).ramificationIdx R = q.ramificationIdx R

    Alias of Ideal.ramificationIdx_smul.