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

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

  Any finitely generated ideal is principal.

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

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

Equations

• @IsBezout.span_pair_isPrincipal = @IsBezout.span_pair_isPrincipal.proof_1

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 b, 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

• @IsBezout.instIsIntegrallyClosed = @IsBezout.instIsIntegrallyClosed.proof_1

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.of_isPrincipalIdealRing = @IsBezout.of_isPrincipalIdealRing.proof_1

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