English
In a tower of rings with prime ideals P over p and Q over p in the composed map, ramification indices multiply compatibly along the tower.
Русский
В башне колец с простыми P над p и Q над p в составе, рамификационные индексы умножаются согласованно вдоль башни.
LaTeX
$$$\\\\operatorname{ramificationIdx} (algebraMap R T) p Q = \\\\operatorname{ramificationIdx} (algebraMap R S) p P \\\\cdot \\\\operatorname{ramificationIdx} (algebraMap S T) P Q$$$
Lean4
theorem ramificationIdx_tower [IsDedekindDomain S] [IsDedekindDomain T] {f : R →+* S} {g : S →+* T} {p : Ideal R}
{P : Ideal S} {Q : Ideal T} [hpm : P.IsPrime] [hqm : Q.IsPrime] (hg0 : map g P ≠ ⊥) (hfg : map (g.comp f) p ≠ ⊥)
(hg : map g P ≤ Q) : ramificationIdx (g.comp f) p Q = ramificationIdx f p P * ramificationIdx g P Q := by
classical
have hf0 : map f p ≠ ⊥ := ne_bot_of_map_ne_bot (Eq.mp (congrArg (fun I ↦ I ≠ ⊥) (map_map f g).symm) hfg)
have hp0 : P ≠ ⊥ := ne_bot_of_map_ne_bot hg0
have hq0 : Q ≠ ⊥ := ne_bot_of_le_ne_bot hg0 hg
letI : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hf0 hpm hp0,
IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hg0 hqm hq0,
IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hfg hqm hq0, ← map_map]
rcases eq_prime_pow_mul_coprime hf0 P with ⟨I, hcp, heq⟩
have hcp : ⊤ = map g P ⊔ map g I := by rw [← map_sup, hcp, map_top g]
have hntq : ¬⊤ ≤ Q := fun ht ↦ IsPrime.ne_top hqm (Iff.mpr (eq_top_iff_one Q) (ht trivial))
nth_rw 1 [heq, Ideal.map_mul, Ideal.map_pow,
normalizedFactors_mul (pow_ne_zero _ hg0) <| by
by_contra h
simp only [h, Submodule.zero_eq_bot, bot_le, sup_of_le_left] at hcp
exact hntq (hcp.trans_le hg),
Multiset.count_add, normalizedFactors_pow, Multiset.count_nsmul]
exact
add_eq_left.mpr <|
Decidable.byContradiction fun h ↦
hntq <| hcp.trans_le <| sup_le hg <| le_of_dvd <| dvd_of_mem_normalizedFactors <| Multiset.count_ne_zero.mp h
