dvd_differentIdeal_iff — Mathlib

English

If P is a prime of B lying over a maximal p in A, and the extension is not separable at the corresponding quotients, then P divides the different ideal.

Русский

Для простого P в B над максимальным p в A, если расслоение неразделимо на соответствующих аугментациях, то P делит разный идеал.

LaTeX

$$$[P.IsPrime][P.LiesOver p]\; (H : ¬ Algebra.IsSeparable (A / p) (B / P)) \Rightarrow P \mid \mathrm{differentIdeal } A B$$$

Lean4

/-- A prime divides the different ideal iff it is ramified. -/
theorem dvd_differentIdeal_iff [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {P : Ideal B} [P.IsPrime] :
    P ∣ differentIdeal A B ↔ ¬Algebra.IsUnramifiedAt A P :=
  iff_not_comm.mp not_dvd_differentIdeal_iff.symm

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