English
For a,b in a Bézout ring, and any z, gcd(a,b) divides z iff there exist x,y with z = a x + b y.
Русский
Для a,b в кольце Безоу, и любого z, gcd(a,b) делит z тогда, когда существуют x,y такие, что z = a x + b y.
LaTeX
$$$\forall a,b \in R {z} : gcd(a,b) \mid z \iff \exists x,y, z = a x + b y$$$
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.)
If you want the existence of a maximal non-principal ideal see
`Ideal.exists_maximal_not_isPrincipal`. -/
theorem nonPrincipals_zorn (hR : ¬IsPrincipalIdealRing R) (c : Set (Ideal R)) (hs : c ⊆ nonPrincipals R)
(hchain : IsChain (· ≤ ·) c) : ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I :=
by
by_cases H : c.Nonempty
· obtain ⟨K, hKmem⟩ := Set.nonempty_def.1 H
refine ⟨sSup c, fun ⟨x, hx⟩ ↦ ?_, fun _ ↦ le_sSup⟩
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)
exact hs hJc ⟨hsSupJ ▸ ⟨x, hx⟩⟩
· simpa [Set.not_nonempty_iff_eq_empty.1 H, isPrincipalIdealRing_iff] using hR
