English
In a tower of rings R → S → T with maximal primes P and Q, the ramification index e over p via g∘f equals the product of e over p→P and e over P→Q, under suitable hypotheses.
Русский
В башне колец \(R \to S \to T\) с максимальными простыми P и Q, рамфикационный индекс над p через \(g\circ f\) равен произведению индексов над p→P и 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
instance finiteDimensional_quotient_pow [Module.Finite R S] [p.IsMaximal]
(P : (factors (map (algebraMap R S) p)).toFinset) :
FiniteDimensional (R ⧸ p) (S ⧸ (P : Ideal S) ^ ramificationIdx (algebraMap R S) p P) :=
by
refine .of_finrank_pos ?_
rw [pos_iff_ne_zero, Factors.finrank_pow_ramificationIdx]
exact mul_ne_zero (Factors.ramificationIdx_ne_zero p P) (inertiaDeg_pos p P.1).ne'
