English
In a tower of rings with maximal primes, the ramification index of the composed map equals the product of the two stepwise ramification indices.
Русский
В башне колец с максимальными простыми, рамфикационный индекс составного отображения равен произведению двух последовательных индексов.
LaTeX
$$$\\\\operatorname{ramificationIdx} (algebraMap R T) p Q = \\\\operatorname{ramificationIdx} (algebraMap R S) p P \\\\cdot \\\\operatorname{ramificationIdx} (algebraMap S T) P Q$$$
Lean4
/-- **Chinese remainder theorem** for a ring of integers: if the prime ideal `p : Ideal R`
factors in `S` as `∏ i, P i ^ e i`, then `S ⧸ I` factors as `Π i, R ⧸ (P i ^ e i)`. -/
noncomputable def piQuotientEquiv (p : Ideal R) (hp : map (algebraMap R S) p ≠ ⊥) :
S ⧸ map (algebraMap R S) p ≃+*
∀ P : (factors (map (algebraMap R S) p)).toFinset, S ⧸ (P : Ideal S) ^ ramificationIdx (algebraMap R S) p P :=
(IsDedekindDomain.quotientEquivPiFactors hp).trans <|
@RingEquiv.piCongrRight (factors (map (algebraMap R S) p)).toFinset
(fun P => S ⧸ (P : Ideal S) ^ (factors (map (algebraMap R S) p)).count (P : Ideal S))
(fun P => S ⧸ (P : Ideal S) ^ ramificationIdx (algebraMap R S) p P) _ _
fun P : (factors (map (algebraMap R S) p)).toFinset =>
Ideal.quotEquivOfEq <| by
rw [IsDedekindDomain.ramificationIdx_eq_factors_count hp (Factors.isPrime p P) (Factors.ne_bot p P)]
