Bézout rings

A Bézout ring (Bezout ring) is a ring whose finitely generated ideals are principal. Notable examples include principal ideal rings, valuation rings, and the ring of algebraic integers.

Main results

• IsBezout.iff_span_pair_isPrincipal: It suffices to verify every span {x, y} is principal.
• IsBezout.toGCDDomain: Every Bézout domain is a GCD domain. This is not an instance.
• IsBezout.TFAE: For a Bézout domain, noetherian ↔ PID ↔ UFD ↔ ACCP

class IsBezout (R : Type u) [CommRing R] : Prop

A Bézout ring is a ring whose finitely generated ideals are principal.

• isPrincipal_of_FG : ∀ (I : Ideal R), Ideal.FG I → Submodule.IsPrincipal I

  Any finitely generated ideal is principal.

instance IsBezout.span_pair_isPrincipal {R : Type u} [CommRing R] [IsBezout R] (x : R) (y : R) : Submodule.IsPrincipal (Ideal.span {x, y})

Equations

• (_ : Submodule.IsPrincipal (Ideal.span {x, y})) = (_ : Submodule.IsPrincipal (Ideal.span {x, y}))

theorem IsBezout.iff_span_pair_isPrincipal {R : Type u} [CommRing R] : IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})

noncomputable def IsBezout.gcd {R : Type u} [CommRing R] [IsBezout R] (x : R) (y : R) : R

The gcd of two elements in a bezout domain.

Equations

• IsBezout.gcd x y = Submodule.IsPrincipal.generator (Ideal.span {x, y})

theorem IsBezout.span_gcd {R : Type u} [CommRing R] [IsBezout R] (x : R) (y : R) : Ideal.span {IsBezout.gcd x y} = Ideal.span {x, y}

theorem IsBezout.gcd_dvd_left {R : Type u} [CommRing R] [IsBezout R] (x : R) (y : R) : IsBezout.gcd x y ∣ x

theorem IsBezout.gcd_dvd_right {R : Type u} [CommRing R] [IsBezout R] (x : R) (y : R) : IsBezout.gcd x y ∣ y

theorem IsBezout.dvd_gcd {R : Type u} [CommRing R] [IsBezout R] {x : R} {y : R} {z : R} (hx : z ∣ x) (hy : z ∣ y) : z ∣ IsBezout.gcd x y

theorem IsBezout.gcd_eq_sum {R : Type u} [CommRing R] [IsBezout R] (x : R) (y : R) : ∃ (a : R) (b : R), a * x + b * y = IsBezout.gcd x y

noncomputable def IsBezout.toGCDDomain (R : Type u) [CommRing R] [IsBezout R] [IsDomain R] [DecidableEq R] : GCDMonoid R

Any bezout domain is a GCD domain. This is not an instance since GCDMonoid contains data, and this might not be how we would like to construct it.

Equations

• IsBezout.toGCDDomain R = gcdMonoidOfGCD IsBezout.gcd (_ : ∀ (x y : R), IsBezout.gcd x y ∣ x) (_ : ∀ (x y : R), IsBezout.gcd x y ∣ y) (_ : ∀ {a b c : R}, a ∣ c → a ∣ b → a ∣ IsBezout.gcd c b)

instance IsBezout.instIsIntegrallyClosed {R : Type u} [CommRing R] [IsDomain R] [IsBezout R] : IsIntegrallyClosed R

Equations

• (_ : IsIntegrallyClosed R) = (_ : IsIntegrallyClosed R)

theorem Function.Surjective.isBezout {R : Type u} [CommRing R] {S : Type v} [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) [IsBezout R] : IsBezout S

instance IsBezout.of_isPrincipalIdealRing {R : Type u} [CommRing R] [IsPrincipalIdealRing R] : IsBezout R

Equations

• (_ : IsBezout R) = (_ : IsBezout R)

theorem IsBezout.TFAE {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] : List.TFAE [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R]