English
In a tower R → S → T with maximal p and P lying over p and I lying over P, the inertia degree multiplies along the tower: inertiaDeg p I = inertiaDeg p P · inertiaDeg P I.
Русский
В башне \(R \to S \to T\) с p и P над p, I над P, инерциальная степень удовлетворяет \( inertiaDeg(p,I) = inertiaDeg(p,P) \cdot inertiaDeg(P,I) \).
LaTeX
$$$\\\\operatorname{inertiaDeg} p I = \\\\operatorname{inertiaDeg} p P \\\\cdot \\\\operatorname{inertiaDeg} P I$$$
Lean4
/-- Let `T / S / R` be a tower of algebras, `p, P, Q` be ideals in `R, S, T` respectively,
and `P` and `Q` are prime. If `P = Q ∩ S`, then `e (Q | p) = e (P | p) * e (Q | P)`. -/
theorem ramificationIdx_algebra_tower [IsDedekindDomain S] [IsDedekindDomain T] {p : Ideal R} {P : Ideal S}
{Q : Ideal T} [hpm : P.IsPrime] [hqm : Q.IsPrime] (hg0 : map (algebraMap S T) P ≠ ⊥)
(hfg : map (algebraMap R T) p ≠ ⊥) (hg : map (algebraMap S T) P ≤ Q) :
ramificationIdx (algebraMap R T) p Q =
ramificationIdx (algebraMap R S) p P * ramificationIdx (algebraMap S T) P Q :=
by
rw [IsScalarTower.algebraMap_eq R S T] at hfg ⊢
exact ramificationIdx_tower hg0 hfg hg
