English
If p is unramified at R, then ramificationIdx p B = 1.
Русский
Если p не содержит рaмификации над R, то ramificationIdx p B = 1.
LaTeX
$$$\\mathrm{ramificationIdx}(p|R) = 1$$$
Lean4
theorem of_liesOver_of_ne_bot (p : Ideal S) (P : Ideal T) [P.LiesOver p] [p.IsPrime] [P.IsPrime] [IsUnramifiedAt R P]
[EssFiniteType R S] [EssFiniteType R T] [IsDedekindDomain S] (hP₁ : P.primeCompl ≤ nonZeroDivisors T)
(hP₂ : p ≠ ⊥ → P ≠ ⊥) : IsUnramifiedAt R p :=
by
let p₀ : Ideal R := p.under R
have : P.LiesOver p₀ := .trans P p p₀
have hp₀ : p₀ = P.under R := Ideal.LiesOver.over
have : EssFiniteType S T := .of_comp R S T
have := Algebra.EssFiniteType.isNoetherianRing S T
rw [isUnramifiedAt_iff_map_eq R p₀ p]
have ⟨h₁, h₂⟩ := (isUnramifiedAt_iff_map_eq R p₀ P).mp ‹_›
refine ⟨Algebra.isSeparable_tower_bot_of_isSeparable _ _ P.ResidueField, ?_⟩
by_cases hp : p = ⊥
· have : p₀.map (algebraMap R S) = p := by
subst hp
exact le_bot_iff.mp (Ideal.map_comap_le)
rw [IsScalarTower.algebraMap_eq _ S, ← Ideal.map_map, this, Localization.AtPrime.map_eq_maximalIdeal]
rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hp Ideal.map_comap_le, ← not_ne_iff,
Ideal.ramificationIdx_ne_one_iff Ideal.map_comap_le]
intro H
have := Ideal.ramificationIdx_eq_one_of_map_localization (hp₀ ▸ Ideal.map_comap_le) (hP₂ hp) hP₁ h₂
rw [← not_ne_iff, Ideal.ramificationIdx_ne_one_iff (hp₀ ▸ Ideal.map_comap_le)] at this
replace H := Ideal.map_mono (f := algebraMap S T) H
rw [Ideal.map_map, ← IsScalarTower.algebraMap_eq, Ideal.map_pow] at H
refine this (H.trans (Ideal.pow_right_mono ?_ _))
exact Ideal.map_le_iff_le_comap.mpr Ideal.LiesOver.over.le
