English
In a tower of algebras R → S → T with maximal p, P, Q prime, the ramification in the tower satisfies the multiplicativity e(p→Q) = e(p→P) e(P→Q).
Русский
В башне алгебр \(R \to S \to T\) с максимальными p, P, Q простыми, рамфикационная кратность удовлетворяет \(e(p→Q) = e(p→P) e(P→Q)\).
LaTeX
$$$\\\\operatorname{ramificationIdx} (algebraMap R T) p Q = \\\\operatorname{ramificationIdx} (algebraMap R S) p P \\\\cdot \\\\operatorname{ramificationIdx} (algebraMap S T) P Q$$$
Lean4
/-- `Ideal.sum_ramification_inertia`, in the local (DVR) case. -/
theorem ramificationIdx_mul_inertiaDeg_of_isLocalRing (K L : Type*) [Field K] [Field L] [IsLocalRing S]
[IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L]
[Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] {p : Ideal R} [p.IsMaximal]
(hp0 : p ≠ ⊥) :
ramificationIdx (algebraMap R S) p (IsLocalRing.maximalIdeal S) * p.inertiaDeg (IsLocalRing.maximalIdeal S) =
Module.finrank K L :=
by
have := FaithfulSMul.of_field_isFractionRing R S K L
simp_rw [← sum_ramification_inertia S K L hp0, IsLocalRing.primesOverFinset_eq S hp0, Finset.sum_singleton]
