English
In a ring with KrullDimLE 0, several equivalent statements hold, including the existence and uniqueness of a prime and a nilpotent condition.
Русский
Для кольца с Ring.KrullDimLE 0 выполняются эквивалентности: существование и единственность простого идеала и условия nilpotent.
LaTeX
$$TFAE statement for Ring.KrullDimLE 0$$
Lean4
theorem krullDimLE_zero_and_isLocalRing_tfae :
List.TFAE
[Ring.KrullDimLE 0 R ∧ IsLocalRing R, ∃! I : Ideal R, I.IsPrime, ∀ x : R, IsNilpotent x ↔ ¬IsUnit x,
(nilradical R).IsMaximal] :=
by
tfae_have 1 → 3 := by
intro ⟨h₁, h₂⟩ x
change x ∈ nilradical R ↔ x ∈ IsLocalRing.maximalIdeal R
rw [nilradical, Ideal.radical_eq_sInf]
simp [← Ideal.isMaximal_iff_isPrime, IsLocalRing.isMaximal_iff]
tfae_have 3 → 4 := by
refine fun H ↦ ⟨fun e ↦ ?_, fun I hI ↦ ?_⟩
· obtain ⟨n, hn⟩ := (Ideal.eq_top_iff_one _).mp e
exact (H 0).mp .zero ((show (1 : R) = 0 by simpa using hn) ▸ isUnit_one)
· obtain ⟨x, hx, hx'⟩ := (SetLike.lt_iff_le_and_exists.mp hI).2
exact Ideal.eq_top_of_isUnit_mem _ hx (not_not.mp ((H x).not.mp hx'))
tfae_have 4 → 2 := fun H ↦
⟨_, H.isPrime, fun p (hp : p.IsPrime) ↦ (H.eq_of_le hp.ne_top (nilradical_le_prime p)).symm⟩
tfae_have 2 → 1 := by
rintro ⟨P, hP₁, hP₂⟩
obtain ⟨P, hP₃, -⟩ := P.exists_le_maximal hP₁.ne_top
obtain rfl := hP₂ P hP₃.isPrime
exact ⟨.mk₀ fun Q h ↦ hP₂ Q h ▸ hP₃, .of_unique_max_ideal ⟨P, hP₃, fun Q h ↦ hP₂ Q h.isPrime⟩⟩
tfae_finish
