English
A Nullstellensatz-like statement: if P divides the product mapping to p and certain coprimality holds, then P does not divide the different ideal.
Русский
Пусть произведение делит образ p, и существуют условия взаимной простоты; тогда P не делит различный идеал.
LaTeX
$$¬(P ∣ differentIdeal(A,B))$$
Lean4
theorem pow_sub_one_dvd_differentIdeal [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A}
[p.IsMaximal] (P : Ideal B) (e : ℕ) (hp : p ≠ ⊥) (hP : P ^ e ∣ p.map (algebraMap A B)) :
P ^ (e - 1) ∣ differentIdeal A B :=
by
have : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
IsIntegralClosure.isLocalization _ (FractionRing A) _ _
have : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
by_cases he : e = 0
· rw [he, pow_zero]; exact one_dvd _
exact pow_sub_one_dvd_differentIdeal_aux A (FractionRing A) (FractionRing B) _ he hp hP
