English
For a Bezout domain R that is a domain, the four properties Noetherian, Principal Ideal Ring, Unique Factorization Monoid, and WfDvdMonoid are equivalent.
Русский
Для Безут домена R, являющегося доменом, четыре свойства: Noetherian, PIR, UFD, WfDvdMonoid эквивалентны.
LaTeX
$$$IsBezout\ R \land IsDomain\ R \Rightarrow \text{List.TFAE}([IsNoetherianRing\ R, IsPrincipalIdealRing\ R, UniqueFactorizationMonoid\ R, WfDvdMonoid\ R])$$$
Lean4
theorem _root_.Function.Surjective.isBezout {S : Type v} [CommRing S] (f : R →+* S) (hf : Function.Surjective f)
[IsBezout R] : IsBezout S := by
rw [iff_span_pair_isPrincipal]
intro x y
obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := hf x, hf y
use f (gcd x y)
trans Ideal.map f (Ideal.span {gcd x y})
· rw [span_gcd, Ideal.map_span, Set.image_insert_eq, Set.image_singleton]
· rw [Ideal.map_span, Set.image_singleton]; rfl
