English
Let R ⊂ S be a setting with S a Dedekind domain and P a prime ideal of S lying over a prime ideal p of R. Then the ramification index e(P|p) equals 1 if and only if the image of p in the localization of S at P is the maximal ideal of that local ring. In particular, unramified primes have ramification index 1.
Русский
Пусть R⊆S и S — кольцо Дедекинда; P — простый идеал в S над p — простым идеалом в R. Тогда ramificationIdx(algebraMap R S) p P = 1 тогда и только тогда, когда образ p в локализации AtPrime P равен максимальному идеалу этой локализации.
LaTeX
$$$\\\\operatorname{ramificationIdx}(\\\\operatorname{algebraMap} R S) \\, p \\, P = 1 \\,\\\\Longrightarrow\\\\, p.map (\\\\operatorname{algebraMap} R (\\\\ Localization.AtPrime P)) = \\,\\\\operatorname{maximalIdeal} (\\\\ Localization.AtPrime P)$ and conversely.$$
Lean4
theorem ramificationIdx_eq_one_iff [Algebra R S] {p : Ideal R} {P : Ideal S} [P.IsPrime] (hp : P ≠ ⊥)
(hpP : p.map (algebraMap R S) ≤ P) :
ramificationIdx (algebraMap R S) p P = 1 ↔
p.map (algebraMap R (Localization.AtPrime P)) = maximalIdeal (Localization.AtPrime P) :=
by
refine ⟨?_, ramificationIdx_eq_one_of_map_localization hpP hp (primeCompl_le_nonZeroDivisors _)⟩
let Sₚ := Localization.AtPrime P
rw [← not_ne_iff (b := 1), ramificationIdx_ne_one_iff hpP, pow_two]
intro H₁
obtain ⟨a, ha⟩ : P ∣ p.map (algebraMap R S) := Ideal.dvd_iff_le.mpr hpP
have ha' : ¬a ≤ P := fun h ↦ H₁ (ha.trans_le (Ideal.mul_mono_right h))
rw [IsScalarTower.algebraMap_eq _ S, ← Ideal.map_map, ha, Ideal.map_mul, Localization.AtPrime.map_eq_maximalIdeal]
convert Ideal.mul_top _
rw [← not_ne_iff, IsLocalization.map_algebraMap_ne_top_iff_disjoint P.primeCompl]
simpa [primeCompl, Set.disjoint_compl_left_iff_subset]
