nonPrincipals_zorn — Mathlib

English

If R is not principal, every chain of nonprincipal ideals has an upper bound which is nonprincipal.

Русский

Если R не является главной, каждая цепь неглавных идеалов имеет верхнюю грань, которая тоже не главная.

LaTeX

$$$\forall c \subseteq \mathrm{Ideal}(R),\; c \text{ is a chain in } \le \; \Rightarrow \exists I \in \{I \mid \neg I.IsPrincipal\}, \forall J \in c, J \le I$$$

Lean4

/-- Any chain in the set of non-principal ideals has an upper bound which is non-principal.
(Namely, the union of the chain is such an upper bound.)
-/
@[deprecated Ideal.nonPrincipals_zorn (since := "2025-09-30")]
theorem nonPrincipals_zorn (c : Set (Ideal R)) (hs : c ⊆ {I : Ideal R | ¬I.IsPrincipal}) (hchain : IsChain (· ≤ ·) c)
    {K : Ideal R} (hKmem : K ∈ c) : ∃ I ∈ {I : Ideal R | ¬I.IsPrincipal}, ∀ J ∈ c, J ≤ I :=
  by
  refine ⟨sSup c, ?_, fun J hJ => le_sSup hJ⟩
  rintro ⟨x, hx⟩
  have hxmem : x ∈ sSup c := hx.symm ▸ Submodule.mem_span_singleton_self x
  obtain ⟨J, hJc, hxJ⟩ := (Submodule.mem_sSup_of_directed ⟨K, hKmem⟩ hchain.directedOn).1 hxmem
  have hsSupJ : sSup c = J := le_antisymm (by simp [hx, Ideal.span_le, hxJ]) (le_sSup hJc)
  specialize hs hJc
  rw [← hsSupJ, hx] at hs
  exact hs ⟨⟨x, rfl⟩⟩

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