English
Under an algebra isomorphism e between two rings, the ramification index computed with respect to p and P is preserved under comap/ map with the appropriate transports.
Русский
При изоморфизме колец e сохраняется величина ramificationIdx при переходе между парами p,P через соответствующие отображения comap и map.
LaTeX
$$$ramificationIdx(\\text{algebraMap } R S, p, P) = ramificationIdx(\\text{algebraMap } R S_1, p, P)$$$
Lean4
/-- The ramification index of `P` over `p` is the largest exponent `n` such that
`p` is contained in `P^n`.
In particular, if `p` is not contained in `P^n`, then the ramification index is 0.
If there is no largest such `n` (e.g. because `p = ⊥`), then `ramificationIdx` is
defined to be 0.
-/
noncomputable def ramificationIdx : ℕ :=
sSup {n | map f p ≤ P ^ n}
