Documentation

Mathlib.RingTheory.RamificationInertia.Inertia

Inertia degree #

Given a prime ideal q of an R-algebra S, the inertia degree of q over R is defined to be the degree of the residue field of q over the residue field of its preimage p in R.

Main definitions #

Main statements #

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

Given a prime ideal q of an R-algebra S, the inertia degree of q over R is defined to be the degree of the residue field of q over the residue field of its preimage p in R.

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

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

Equations
Instances For
    source
    theorem Ideal.inertiaDeg_def {S : Type u_1} [CommRing S] (q : Ideal S) (R : Type u_2) [CommRing R] [Algebra R S] [hq : q.IsPrime] [Algebra (Localization.AtPrime (under R q)) (Localization.AtPrime q)] [Localization.AtPrime.IsLiesOverAlgebra (under R q) q] :
    q.inertiaDeg R = Module.finrank (under R q).ResidueField q.ResidueField
    source
    @[deprecated Ideal.inertiaDeg_def (since := "2026-07-03")]
    theorem Ideal.inertiaDeg'_def {S : Type u_1} [CommRing S] (q : Ideal S) (R : Type u_2) [CommRing R] [Algebra R S] [hq : q.IsPrime] [Algebra (Localization.AtPrime (under R q)) (Localization.AtPrime q)] [Localization.AtPrime.IsLiesOverAlgebra (under R q) q] :
    q.inertiaDeg R = Module.finrank (under R q).ResidueField q.ResidueField

    Alias of Ideal.inertiaDeg_def.

    source
    theorem Ideal.inertiaDeg_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.inertiaDeg R = 0
    source
    @[deprecated Ideal.inertiaDeg_of_not_isPrime (since := "2026-07-03")]
    theorem Ideal.inertiaDeg'_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.inertiaDeg R = 0

    Alias of Ideal.inertiaDeg_of_not_isPrime.

    source
    theorem Ideal.inertiaDeg_pos {S : Type u_1} [CommRing S] (q : Ideal S) (R : Type u_2) [CommRing R] [Algebra R S] [hq : q.IsPrime] [Module.Finite R S] :
    0 < q.inertiaDeg R
    source
    theorem Ideal.inertiaDeg_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] [p.IsPrime] [Algebra (Localization.AtPrime p) (Localization.AtPrime q)] [Localization.AtPrime.IsLiesOverAlgebra p q] :
    q.inertiaDeg R = Module.finrank p.ResidueField q.ResidueField
    source
    @[deprecated Ideal.inertiaDeg_eq (since := "2026-07-03")]
    theorem Ideal.inertiaDeg'_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] [p.IsPrime] [Algebra (Localization.AtPrime p) (Localization.AtPrime q)] [Localization.AtPrime.IsLiesOverAlgebra p q] :
    q.inertiaDeg R = Module.finrank p.ResidueField q.ResidueField

    Alias of Ideal.inertiaDeg_eq.

    source
    theorem Ideal.inertiaDeg_eq_of_isFractionRing {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [q.LiesOver p] [p.IsPrime] [q.IsPrime] (K : Type u_4) (L : Type u_5) [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
    source
    @[deprecated Ideal.inertiaDeg_eq_of_isFractionRing (since := "2026-07-03")]
    theorem Ideal.inertiaDeg'_eq_of_isFractionRing {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [q.LiesOver p] [p.IsPrime] [q.IsPrime] (K : Type u_4) (L : Type u_5) [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

    Alias of Ideal.inertiaDeg_eq_of_isFractionRing.

    source
    theorem Ideal.inertiaDeg_eq_of_isMaximal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [q.LiesOver p] [p.IsMaximal] [q.IsMaximal] :
    q.inertiaDeg R = Module.finrank (R ⧸ p) (S ⧸ q)
    source
    @[deprecated Ideal.inertiaDeg_eq_of_isMaximal (since := "2026-07-03")]
    theorem Ideal.inertiaDeg'_eq_of_isMaximal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [q.LiesOver p] [p.IsMaximal] [q.IsMaximal] :
    q.inertiaDeg R = Module.finrank (R ⧸ p) (S ⧸ q)

    Alias of Ideal.inertiaDeg_eq_of_isMaximal.

    source
    theorem Ideal.inertiaDeg'_eq_inertiaDeg {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [q.LiesOver p] [p.IsMaximal] [q.IsMaximal] :
    p.inertiaDeg' q = q.inertiaDeg R
    source
    @[deprecated Ideal.inertiaDeg'_eq_inertiaDeg (since := "2026-07-03")]
    theorem Ideal.inertiaDeg_eq_inertiaDeg' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [q.LiesOver p] [p.IsMaximal] [q.IsMaximal] :
    p.inertiaDeg' q = q.inertiaDeg R

    Alias of Ideal.inertiaDeg'_eq_inertiaDeg.

    source
    theorem Ideal.inertiaDeg_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] :
    r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S
    source
    @[deprecated Ideal.inertiaDeg_tower (since := "2026-07-03")]
    theorem Ideal.inertiaDeg'_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] :
    r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S

    Alias of Ideal.inertiaDeg_tower.

    source
    theorem Ideal.inertiaDeg_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] :
    q.inertiaDeg R ∣ r.inertiaDeg R
    source
    @[deprecated Ideal.inertiaDeg_below_dvd (since := "2026-07-03")]
    theorem Ideal.inertiaDeg'_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] :
    q.inertiaDeg R ∣ r.inertiaDeg R

    Alias of Ideal.inertiaDeg_below_dvd.

    source
    theorem Ideal.inertiaDeg_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] :
    r.inertiaDeg S ∣ r.inertiaDeg R
    source
    @[deprecated Ideal.inertiaDeg_above_dvd (since := "2026-07-03")]
    theorem Ideal.inertiaDeg'_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] :
    r.inertiaDeg S ∣ r.inertiaDeg R

    Alias of Ideal.inertiaDeg_above_dvd.

    source
    theorem Ideal.inertiaDeg_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] :
    q.inertiaDeg R ≤ r.inertiaDeg R
    source
    @[deprecated Ideal.inertiaDeg_below_le (since := "2026-07-03")]
    theorem Ideal.inertiaDeg'_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] :
    q.inertiaDeg R ≤ r.inertiaDeg R

    Alias of Ideal.inertiaDeg_below_le.

    source
    theorem Ideal.inertiaDeg_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] :
    r.inertiaDeg S ≤ r.inertiaDeg R
    source
    @[deprecated Ideal.inertiaDeg_above_le (since := "2026-07-03")]
    theorem Ideal.inertiaDeg'_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] :
    r.inertiaDeg S ≤ r.inertiaDeg R

    Alias of Ideal.inertiaDeg_above_le.

    source
    @[simp]
    theorem Ideal.inertiaDeg_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).inertiaDeg R = q.inertiaDeg R
    source
    @[deprecated Ideal.inertiaDeg_smul (since := "2026-07-03")]
    theorem Ideal.inertiaDeg'_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).inertiaDeg R = q.inertiaDeg R

    Alias of Ideal.inertiaDeg_smul.

    source
    theorem Ideal.cardQuot_pow_inertiaDeg {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [Module.Finite R S] [p.IsMaximal] [q.IsMaximal] [q.LiesOver p] :
    Submodule.cardQuot p ^ q.inertiaDeg R = Submodule.cardQuot q
    source
    @[deprecated Ideal.cardQuot_pow_inertiaDeg (since := "2026-07-03")]
    theorem Ideal.cardQuot_pow_inertiaDeg' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [Module.Finite R S] [p.IsMaximal] [q.IsMaximal] [q.LiesOver p] :
    Submodule.cardQuot p ^ q.inertiaDeg R = Submodule.cardQuot q

    Alias of Ideal.cardQuot_pow_inertiaDeg.

    source
    theorem Ideal.absNorm_pow_inertiaDeg {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [Module.Finite R S] [q.IsPrime] [q.LiesOver p] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Free ℤ R] [Module.Free ℤ S] :
    absNorm p ^ q.inertiaDeg R = absNorm q
    source
    @[deprecated Ideal.absNorm_pow_inertiaDeg (since := "2026-07-03")]
    theorem Ideal.absNorm_pow_inertiaDeg' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [Module.Finite R S] [q.IsPrime] [q.LiesOver p] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Free ℤ R] [Module.Free ℤ S] :
    absNorm p ^ q.inertiaDeg R = absNorm q

    Alias of Ideal.absNorm_pow_inertiaDeg.

    source
    theorem Ideal.natAbs_pow_inertiaDeg {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] (p : ℤ) (P : Ideal R) [P.IsPrime] [P.LiesOver (span {p})] :
    p.natAbs ^ P.inertiaDeg ℤ = absNorm P
    source
    @[deprecated Ideal.natAbs_pow_inertiaDeg (since := "2026-07-03")]
    theorem Ideal.natAbs_pow_inertiaDeg' {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] (p : ℤ) (P : Ideal R) [P.IsPrime] [P.LiesOver (span {p})] :
    p.natAbs ^ P.inertiaDeg ℤ = absNorm P

    Alias of Ideal.natAbs_pow_inertiaDeg.

    source
    theorem Ideal.pow_inertiaDeg {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] (p : ℕ) (P : Ideal R) [P.IsPrime] [P.LiesOver (span {↑p})] :
    p ^ P.inertiaDeg ℤ = absNorm P