Bézout rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

is_bezout.iff_span_pair_is_principal: It suffices to verify every span {x, y} is principal.
is_bezout.to_gcd_monoid: Every Bézout domain is a GCD domain. This is not an instance.
is_bezout.tfae: For a Bézout domain, noetherian ↔ PID ↔ UFD ↔ ACCP

source

@[class]

structure is_bezout (R : Type u) [comm_ring R] :

Prop

is_principal_of_fg : ∀ (I : ideal R), I.fg → submodule.is_principal I

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

Instances of this typeclass

source

@[protected, instance]

def is_bezout.span_pair_is_principal {R : Type u} [comm_ring R] [is_bezout R] (x y : R) :

submodule.is_principal (ideal.span {x, y})

source

theorem is_bezout.iff_span_pair_is_principal {R : Type u} [comm_ring R] :

is_bezout R ↔ ∀ (x y : R), submodule.is_principal (ideal.span {x, y})

source

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

The gcd of two elements in a bezout domain.

Equations

is_bezout.gcd x y = submodule.is_principal.generator (ideal.span {x, y})

source

theorem is_bezout.span_gcd {R : Type u} [comm_ring R] [is_bezout R] (x y : R) :

ideal.span {is_bezout.gcd x y} = ideal.span {x, y}

source

theorem is_bezout.gcd_dvd_left {R : Type u} [comm_ring R] [is_bezout R] (x y : R) :

is_bezout.gcd x y ∣ x

source

theorem is_bezout.gcd_dvd_right {R : Type u} [comm_ring R] [is_bezout R] (x y : R) :

is_bezout.gcd x y ∣ y

source

theorem is_bezout.dvd_gcd {R : Type u} [comm_ring R] [is_bezout R] {x y z : R} (hx : z ∣ x) (hy : z ∣ y) :

z ∣ is_bezout.gcd x y

source

theorem is_bezout.gcd_eq_sum {R : Type u} [comm_ring R] [is_bezout R] (x y : R) :

∃ (a b : R), a * x + b * y = is_bezout.gcd x y

source

noncomputable def is_bezout.to_gcd_domain (R : Type u) [comm_ring R] [is_bezout R] [is_domain R] [decidable_eq R] :

gcd_monoid R

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

Equations

is_bezout.to_gcd_domain R = gcd_monoid_of_gcd is_bezout.gcd is_bezout.gcd_dvd_left is_bezout.gcd_dvd_right _

source

@[protected, instance]

def is_bezout.is_integrally_closed {R : Type u} [comm_ring R] [is_domain R] [is_bezout R] :

is_integrally_closed R

source

theorem function.surjective.is_bezout {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (hf : function.surjective ⇑f) [is_bezout R] :

is_bezout S

source

@[protected, instance]

def is_bezout.of_is_principal_ideal_ring {R : Type u} [comm_ring R] [is_principal_ideal_ring R] :

is_bezout R

source

theorem is_bezout.tfae {R : Type u} [comm_ring R] [is_bezout R] [is_domain R] :

[is_noetherian_ring R, is_principal_ideal_ring R, unique_factorization_monoid R, wf_dvd_monoid R].tfae