English
ramificationIdxIn_eq_ramificationIdx states equality of ramification indices across p and P; i.e., ramificationIdxIn p B = ramificationIdx (algebraMap A B) p P.
Русский
ramificationIdxIn_eq_ramificationIdx утверждает равенство индексов рамификации по отношению к p и P: ramificationIdxIn p B = ramificationIdx (algebraMap A B) p P.
LaTeX
$$$\\mathrm{ramificationIdxIn}\\ p\\ B = \\mathrm{ramificationIdx}(\\mathrm{algebraMap}\\ A B)\\ p\\ P$$$
Lean4
/-- Up to technical conditions, If `T/S/R` is a tower of algebras, `P` is a prime of `T` unramified
in `R`, then `P ∩ S` (as a prime of `S`) is also unramified in `R`.
-/
theorem of_liesOver (p : Ideal S) (P : Ideal T) [P.LiesOver p] [p.IsPrime] [P.IsPrime] [IsUnramifiedAt R P]
[EssFiniteType R S] [EssFiniteType R T] [IsDedekindDomain S] [IsDomain T] [NoZeroSMulDivisors S T] :
IsUnramifiedAt R p :=
IsUnramifiedAt.of_liesOver_of_ne_bot R p P P.primeCompl_le_nonZeroDivisors (Ideal.ne_bot_of_liesOver_of_ne_bot · P)
