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 ramificationIdxIn(p,B) to be the ramification index of p with respect to the map A → B, computed from such a P; otherwise ramificationIdxIn(p,B) = 0. In the Galois situation, the ramification indices over p are all equal, so this common value is well-defined.
Русский
Пусть A — коммутативное кольцо, p — идеал A, B — коммутативное кольцо с A-алгеброй. Если существует простый идеал P в B, лежащий над p, то задаётся рамификационный индекс p через отображение A → B (при выборе P); иначе задаётся 0. В случае Галуа-расширения все такие индексы одинаковы, следовательно, можно определить общий рамификационный индекс над p.
LaTeX
$$$\\displaystyle \\operatorname{ramificationIdxIn}(A,p,B)=\\begin{cases} \\operatorname{ramificationIdx}(\\mathrm{algebraMap}\\ A\\ B)\\ 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.ramificationIdx_eq_of_IsGalois` that all `Ideal.ramificationIdx` over a fixed
maximal ideal `p` of `A` are the same, which we define as `Ideal.ramificationIdxIn`. -/
noncomputable def ramificationIdxIn {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.ramificationIdx (algebraMap A B) h.choose else 0
