Principal ideal rings, principal ideal domains, and Bézout rings

A principal ideal ring (PIR) is a ring in which all left ideals are principal. A principal ideal domain (PID) is an integral domain which is a principal ideal ring.

The definition of IsPrincipalIdealRing can be found in Mathlib/RingTheory/Ideal/Span.lean.

Main definitions

Note that for principal ideal domains, one should use [IsDomain R] [IsPrincipalIdealRing R]. There is no explicit definition of a PID. Theorems about PID's are in the PrincipalIdealRing namespace.

• IsBezout: the predicate saying that every finitely generated left ideal is principal.
• generator: a generator of a principal ideal (or more generally submodule)
• to_uniqueFactorizationMonoid: a PID is a unique factorization domain

Main results

• Ideal.IsPrime.to_maximal_ideal: a non-zero prime ideal in a PID is maximal.
• EuclideanDomain.to_principal_ideal_domain : a Euclidean domain is a PID.
• IsBezout.nonemptyGCDMonoid: Every Bézout domain is a GCD domain.

instance bot_isPrincipal {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : ⊥.IsPrincipal

instance top_isPrincipal {R : Type u} [Semiring R] : ⊤.IsPrincipal

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

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

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

  Any finitely generated ideal is principal.

@[instance 100]

instance IsBezout.of_isPrincipalIdealRing (R : Type u) [Semiring R] [IsPrincipalIdealRing R] : IsBezout R

@[instance 100]

instance DivisionSemiring.isPrincipalIdealRing (K : Type u) [DivisionSemiring K] : IsPrincipalIdealRing K

@[simp]

theorem Ideal.span_singleton_generator {R : Type u} [Semiring R] (I : Ideal R) [Submodule.IsPrincipal I] : span {Submodule.IsPrincipal.generator I} = I

@[simp]

theorem Submodule.IsPrincipal.generator_mem {R : Type u} {M : Type v} [AddCommMonoid M] [Semiring R] [Module R M] (S : Submodule R M) [S.IsPrincipal] : generator S ∈ S

theorem Submodule.IsPrincipal.mem_iff_eq_smul_generator {R : Type u} {M : Type v} [AddCommMonoid M] [Semiring R] [Module R M] (S : Submodule R M) [S.IsPrincipal] {x : M} : x ∈ S ↔ ∃ (s : R), x = s • generator S

theorem Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero {R : Type u} {M : Type v} [AddCommMonoid M] [Semiring R] [Module R M] (S : Submodule R M) [S.IsPrincipal] : S = ⊥ ↔ generator S = 0

theorem Submodule.IsPrincipal.fg {R : Type u} {M : Type v} [AddCommMonoid M] [Semiring R] [Module R M] {S : Submodule R M} (h : S.IsPrincipal) : S.FG

@[instance 100]

instance PrincipalIdealRing.isNoetherianRing {R : Type u} [Semiring R] [IsPrincipalIdealRing R] : IsNoetherianRing R

@[instance 100]

instance IsPrincipalIdealRing.of_isNoetherianRing_of_isBezout {R : Type u} [Semiring R] [IsNoetherianRing R] [IsBezout R] : IsPrincipalIdealRing R

theorem Submodule.IsPrincipal.associated_generator_span_self {R : Type u} [CommSemiring R] [IsDomain R] (r : R) : Associated (generator (Ideal.span {r})) r

theorem Submodule.IsPrincipal.mem_iff_generator_dvd {R : Type u} [CommSemiring R] (S : Ideal R) [IsPrincipal S] {x : R} : x ∈ S ↔ generator S ∣ x

theorem Submodule.IsPrincipal.prime_generator_of_isPrime {R : Type u} [CommSemiring R] (S : Ideal R) [IsPrincipal S] [is_prime : S.IsPrime] (ne_bot : S ≠ ⊥) : Prime (generator S)

theorem Submodule.IsPrincipal.generator_map_dvd_of_mem {R : Type u} {M : Type v} [AddCommMonoid M] [CommSemiring R] [Module R M] {N : Submodule R M} (ϕ : M →ₗ[R] R) [(Submodule.map ϕ N).IsPrincipal] {x : M} (hx : x ∈ N) : generator (Submodule.map ϕ N) ∣ ϕ x

theorem Submodule.IsPrincipal.generator_submoduleImage_dvd_of_mem {R : Type u} {M : Type v} [AddCommMonoid M] [CommSemiring R] [Module R M] {N O : Submodule R M} (hNO : N ≤ O) (ϕ : ↥O →ₗ[R] R) [(ϕ.submoduleImage N).IsPrincipal] {x : M} (hx : x ∈ N) : generator (ϕ.submoduleImage N) ∣ ϕ ⟨x, ⋯⟩

theorem Submodule.IsPrincipal.dvd_generator_span_iff {R : Type u} [CommSemiring R] {r : R} {s : Set R} [IsPrincipal (Ideal.span s)] : r ∣ generator (Ideal.span s) ↔ ∀ x ∈ s, r ∣ x

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

noncomputable def IsBezout.gcd {R : Type u} [Ring R] (x y : R) [Submodule.IsPrincipal (Ideal.span {x, y})] : R

A choice of gcd of two elements in a Bézout domain.

Note that the choice is usually not unique.

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

theorem IsBezout.gcd_dvd_left {R : Type u} [CommRing R] (x y : R) [Submodule.IsPrincipal (Ideal.span {x, y})] : gcd x y ∣ x

theorem IsBezout.gcd_dvd_right {R : Type u} [CommRing R] (x y : R) [Submodule.IsPrincipal (Ideal.span {x, y})] : gcd x y ∣ y

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

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

theorem IsRelPrime.isCoprime {R : Type u} [CommRing R] {x y : R} [Submodule.IsPrincipal (Ideal.span {x, y})] (h : IsRelPrime x y) : IsCoprime x y

theorem isRelPrime_iff_isCoprime {R : Type u} [CommRing R] {x y : R} [Submodule.IsPrincipal (Ideal.span {x, y})] : IsRelPrime x y ↔ IsCoprime x y

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

Any Bézout 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.

instance IsBezout.nonemptyGCDMonoid (R : Type u) [CommRing R] [IsBezout R] [IsDomain R] : Nonempty (GCDMonoid R)

theorem IsBezout.associated_gcd_gcd (R : Type u) [CommRing R] {x y : R} [Submodule.IsPrincipal (Ideal.span {x, y})] [GCDMonoid R] : Associated (gcd x y) (GCDMonoid.gcd x y)

theorem IsPrime.to_maximal_ideal {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Ideal R} [hpi : S.IsPrime] (hS : S ≠ ⊥) : S.IsMaximal

theorem mod_mem_iff {R : Type u} [EuclideanDomain R] {S : Ideal R} {x y : R} (hy : y ∈ S) : x % y ∈ S ↔ x ∈ S

@[instance 100]

instance EuclideanDomain.to_principal_ideal_domain {R : Type u} [EuclideanDomain R] : IsPrincipalIdealRing R

theorem IsField.isPrincipalIdealRing {R : Type u_1} [Ring R] (h : IsField R) : IsPrincipalIdealRing R

theorem PrincipalIdealRing.isMaximal_of_irreducible {R : Type u} [CommSemiring R] [IsPrincipalIdealRing R] {p : R} (hp : Irreducible p) : Ideal.IsMaximal (R ∙ p)

noncomputable def PrincipalIdealRing.factors {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (a : R) : Multiset R

factors a is a multiset of irreducible elements whose product is a, up to units

theorem PrincipalIdealRing.factors_spec {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (a : R) (h : a ≠ 0) : (∀ b ∈ factors a, Irreducible b) ∧ Associated (factors a).prod a

theorem PrincipalIdealRing.ne_zero_of_mem_factors {R : Type v} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a b : R} (ha : a ≠ 0) (hb : b ∈ factors a) : b ≠ 0

theorem PrincipalIdealRing.mem_submonoid_of_factors_subset_of_units_subset {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (s : Submonoid R) {a : R} (ha : a ≠ 0) (hfac : ∀ b ∈ factors a, b ∈ s) (hunit : ∀ (c : Rˣ), ↑c ∈ s) : a ∈ s

theorem PrincipalIdealRing.ringHom_mem_submonoid_of_factors_subset_of_units_subset {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NonAssocSemiring S] (f : R →+* S) (s : Submonoid S) (a : R) (ha : a ≠ 0) (h : ∀ b ∈ factors a, f b ∈ s) (hf : ∀ (c : Rˣ), f ↑c ∈ s) : f a ∈ s

If a RingHom maps all units and all factors of an element a into a submonoid s, then it also maps a into that submonoid.

@[instance 100]

instance PrincipalIdealRing.to_uniqueFactorizationMonoid {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] : UniqueFactorizationMonoid R

A principal ideal domain has unique factorization

theorem Submodule.IsPrincipal.map {R : Type u} {M : Type v} {N : Type u_2} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) {S : Submodule R M} (hI : S.IsPrincipal) : (Submodule.map f S).IsPrincipal

theorem Submodule.IsPrincipal.of_comap {R : Type u} {M : Type v} {N : Type u_2} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) (S : Submodule R N) [hI : (comap f S).IsPrincipal] : S.IsPrincipal

theorem Submodule.IsPrincipal.map_ringHom {R : Type u} {S : Type u_1} {F : Type u_3} [Semiring R] [Semiring S] [FunLike F R S] [RingHomClass F R S] (f : F) {I : Ideal R} (hI : IsPrincipal I) : IsPrincipal (Ideal.map f I)

theorem Ideal.IsPrincipal.of_comap {R : Type u} {S : Type u_1} {F : Type u_3} [Semiring R] [Semiring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) (I : Ideal S) [hI : Submodule.IsPrincipal (comap f I)] : Submodule.IsPrincipal I

theorem IsPrincipalIdealRing.of_surjective {R : Type u} {S : Type u_1} {F : Type u_3} [Semiring R] [Semiring S] [FunLike F R S] [RingHomClass F R S] [IsPrincipalIdealRing R] (f : F) (hf : Function.Surjective ⇑f) : IsPrincipalIdealRing S

The surjective image of a principal ideal ring is again a principal ideal ring.

theorem isPrincipalIdealRing_prod_iff {R : Type u} {S : Type u_1} [Semiring R] [Semiring S] : IsPrincipalIdealRing (R × S) ↔ IsPrincipalIdealRing R ∧ IsPrincipalIdealRing S

theorem isPrincipalIdealRing_pi_iff {ι : Type u_5} [Finite ι] {R : ι → Type u_4} [(i : ι) → Semiring (R i)] : IsPrincipalIdealRing ((i : ι) → R i) ↔ ∀ (i : ι), IsPrincipalIdealRing (R i)

theorem isCoprime_of_dvd {R : Type u} [CommRing R] [IsBezout R] (x y : R) (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ z ∈ nonunits R, z ≠ 0 → z ∣ x → ¬z ∣ y) : IsCoprime x y

theorem dvd_or_isCoprime {R : Type u} [CommRing R] [IsBezout R] (x y : R) (h : Irreducible x) : x ∣ y ∨ IsCoprime x y

theorem Irreducible.coprime_iff_not_dvd {R : Type u} [CommRing R] [IsBezout R] {p n : R} (hp : Irreducible p) : IsCoprime p n ↔ ¬p ∣ n

See also Irreducible.isRelPrime_iff_not_dvd.

theorem Irreducible.dvd_iff_not_isCoprime {R : Type u} [CommRing R] [IsBezout R] {p n : R} (hp : Irreducible p) : p ∣ n ↔ ¬IsCoprime p n

See also Irreducible.coprime_iff_not_dvd'.

theorem Irreducible.coprime_pow_of_not_dvd {R : Type u} [CommRing R] [IsBezout R] {p a : R} (m : ℕ) (hp : Irreducible p) (h : ¬p ∣ a) : IsCoprime a (p ^ m)

theorem Irreducible.isCoprime_or_dvd {R : Type u} [CommRing R] [IsBezout R] {p : R} (hp : Irreducible p) (i : R) : IsCoprime p i ∨ p ∣ i

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

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

theorem gcd_dvd_iff_exists {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] [GCDMonoid R] (a b : R) {z : R} : gcd a b ∣ z ↔ ∃ (x : R) (y : R), z = a * x + b * y

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

Bézout's lemma

theorem gcd_isUnit_iff {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] [GCDMonoid R] (x y : R) : IsUnit (gcd x y) ↔ IsCoprime x y

theorem Prime.coprime_iff_not_dvd {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] {p n : R} (hp : Prime p) : IsCoprime p n ↔ ¬p ∣ n

theorem exists_associated_pow_of_mul_eq_pow' {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] {a b c : R} (hab : IsCoprime a b) {k : ℕ} (h : a * b = c ^ k) : ∃ (d : R), Associated (d ^ k) a

theorem exists_associated_pow_of_associated_pow_mul {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] {a b c : R} (hab : IsCoprime a b) {k : ℕ} (h : Associated (c ^ k) (a * b)) : ∃ (d : R), Associated (d ^ k) a

theorem isCoprime_of_irreducible_dvd {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {x y : R} (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y) : IsCoprime x y

theorem isCoprime_of_prime_dvd {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {x y : R} (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ (z : R), Prime z → z ∣ x → ¬z ∣ y) : IsCoprime x y

@[reducible, inline]

abbrev Ideal.nonPrincipals (R : Type u) [Semiring R] : Set (Ideal R)

nonPrincipals R is the set of all ideals of R that are not principal ideals.

theorem Ideal.nonPrincipals_eq_empty_iff {R : Type u} [Semiring R] : nonPrincipals R = ∅ ↔ IsPrincipalIdealRing R

theorem Ideal.nonPrincipals_zorn {R : Type u} [Semiring R] (hR : ¬IsPrincipalIdealRing R) (c : Set (Ideal R)) (hs : c ⊆ nonPrincipals R) (hchain : IsChain (fun (x1 x2 : Ideal R) => x1 ≤ x2) c) : ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I

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 Ideal.exists_maximal_not_isPrincipal {R : Type u} [Semiring R] (hR : ¬IsPrincipalIdealRing R) : ∃ (I : Ideal R), Maximal (fun (x : Ideal R) => ¬Submodule.IsPrincipal x) I

@[deprecated Ideal.nonPrincipals (since := "2025-09-30")]

def nonPrincipals (R : Type u) [CommRing R] : Set (Ideal R)

nonPrincipals R is the set of all ideals of R that are not principal ideals.

@[deprecated "Not necessary anymore since Ideal.nonPrincipals is an abrev." (since := "2025-09-30")]

theorem nonPrincipals_def (R : Type u) [CommRing R] {I : Ideal R} : I ∈ {I : Ideal R | ¬Submodule.IsPrincipal I} ↔ ¬Submodule.IsPrincipal I

@[deprecated Ideal.nonPrincipals_eq_empty_iff (since := "2025-09-30")]

theorem nonPrincipals_eq_empty_iff {R : Type u} [CommRing R] : {I : Ideal R | ¬Submodule.IsPrincipal I} = ∅ ↔ IsPrincipalIdealRing R

@[deprecated Ideal.nonPrincipals_zorn (since := "2025-09-30")]

theorem nonPrincipals_zorn {R : Type u} [CommRing R] (c : Set (Ideal R)) (hs : c ⊆ {I : Ideal R | ¬Submodule.IsPrincipal I}) (hchain : IsChain (fun (x1 x2 : Ideal R) => x1 ≤ x2) c) {K : Ideal R} (hKmem : K ∈ c) : ∃ I ∈ {I : Ideal R | ¬Submodule.IsPrincipal I}, ∀ J ∈ c, J ≤ I

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.)

theorem span_singleton_inf_span_singleton {R : Type u} [EuclideanDomain R] [GCDMonoid R] (n m : R) : Ideal.span {n} ⊓ Ideal.span {m} = Ideal.span {lcm n m}