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 #
Ideal.inertiaDeg' q R: The inertia degree ofqoverR.
Main statements #
inertiaDeg_eq_inertiaDeg': The inertia degree agrees with the usual definition in the case of maximal ideals.inertiaDeg'_tower: Inertia degree is multiplicative in towers.
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
- q.inertiaDeg' R = if x : q.IsPrime then Module.finrank (Ideal.under R q).ResidueField q.ResidueField else 0
Instances For
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]
:
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]
: