ramificationIdx_eq_one_of_isUnramifiedAt

English

If p is prime and unramified over R, then the ramification index e(p|R) = 1.

Русский

Если p – простой и нераспухший над R, то коэффициент рaмификации e(p|R) = 1.

LaTeX

$$$e(p|R) = 1$$$

Lean4

theorem ramificationIdx_eq_one_of_isUnramifiedAt {p : Ideal S} [p.IsPrime] [IsNoetherianRing S] [IsUnramifiedAt R p]
    (hp : p ≠ ⊥) [IsDomain S] [EssFiniteType R S] : e(p|R) = 1 :=
  (Ideal.ramificationIdx_eq_one_of_map_localization Ideal.map_comap_le hp p.primeCompl_le_nonZeroDivisors
    ((isUnramifiedAt_iff_map_eq R (p.under R) p).mp ‹_›).2)

Похожие утверждения