English
Let A be a commutative ring, p an ideal of A, and B a commutative ring with an A-algebra structure. If there exists a prime P of B lying over p, define inertiaDegIn(p,B) to be the inertia degree p.inertiaDeg h.choose; otherwise inertiaDegIn(p,B) = 0. In a Galois extension, all inertia degrees over p are equal, so this common value is well-defined.
Русский
Пусть A — коммутативное кольцо, p — идеал A, B — коммутативное кольцо с A-алгеброй. Если существует простая над p в B, то задаётся инерная степень p через отображение A → B (при выборе P); иначе задаётся 0. В Галуа-расширении все степени инерции над p совпадают, следовательно, существует общий инерный показатель.
LaTeX
$$$\\displaystyle \\operatorname{inertiaDegIn}(A,p,B)=\\begin{cases} p.\\text{inertiaDeg}\\ h.\\text{choose} \\\\ &\\text{if }\\ \\exists P : \\text{Ideal } B,\\ P.\\IsPrime \\wedge P.LiesOver\\ p \\\\ 0 & \\text{otherwise} \\end{cases}$$$
Lean4
/-- If `L / K` is a Galois extension, it can be seen from
the theorem `Ideal.inertiaDeg_eq_of_IsGalois` that all `Ideal.inertiaDeg` over a fixed
maximal ideal `p` of `A` are the same, which we define as `Ideal.inertiaDegIn`. -/
noncomputable def inertiaDegIn {A : Type*} [CommRing A] (p : Ideal A) (B : Type*) [CommRing B] [Algebra A B] : ℕ :=
if h : ∃ P : Ideal B, P.IsPrime ∧ P.LiesOver p then p.inertiaDeg h.choose else 0
