English
The inertia degree measures the degree of the residue-field extension when passing from R/p to S/P. More precisely, if P lies over p, then the inertia degree equals the finiteness degree of the extension (R/p) → (S/P).
Русский
Инерционная степень измеряет степень расширения полей остатков при переходе от R/p к S/P; если P лежит над p, то inertiaDeg(p,P) = finrank_{R/p}(S/P).
LaTeX
$$$\\\\operatorname{inertiaDeg} \\, p \\, P = \\operatorname{finrank} \\, (\\\\,R \\/ p) \\, (\\\\, S \\/ P)$$$
Lean4
/-- The inertia degree of `P : Ideal S` lying over `p : Ideal R` is the degree of the
extension `(S / P) : (R / p)`.
We do not assume `P` lies over `p` in the definition; we return `0` instead.
See `inertiaDeg_algebraMap` for the common case where `f = algebraMap R S`
and there is an algebra structure `R / p → S / P`.
-/
noncomputable def inertiaDeg : ℕ :=
if hPp : comap f P = p then
letI : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap hPp.ge
finrank (R ⧸ p) (S ⧸ P)
else
0
-- Useful for the `nontriviality` tactic using `comap_eq_of_scalar_tower_quotient`.
