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.

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] [AddCommGroup M] [Module R M] : ⊥.IsPrincipal

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

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

generator I, if I is a principal submodule, is an x ∈ M such that span R {x} = I

Equations

• Submodule.IsPrincipal.generator S = Classical.choose ⋯

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

@[simp]

theorem Ideal.span_singleton_generator {R : Type u} [Semiring R] (I : Ideal R) [Submodule.IsPrincipal I] : Ideal.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] : Submodule.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 • Submodule.IsPrincipal.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 = ⊥ ↔ Submodule.IsPrincipal.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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

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

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

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

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

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

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

Equations

• ⋯ = ⋯

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.

Equations

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

theorem IsBezout.span_gcd {R : Type u} [Ring R] (x y : R) [Submodule.IsPrincipal (Ideal.span {x, y})] : Ideal.span {IsBezout.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})] : IsBezout.gcd x y ∣ x

theorem IsBezout.gcd_dvd_right {R : Type u} [CommRing R] (x y : R) [Submodule.IsPrincipal (Ideal.span {x, y})] : IsBezout.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 ∣ IsBezout.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 = IsBezout.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.

Equations

• IsBezout.toGCDDomain R = gcdMonoidOfGCD (fun (x1 x2 : R) => IsBezout.gcd x1 x2) ⋯ ⋯ ⋯

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

Equations

• ⋯ = ⋯

theorem IsBezout.associated_gcd_gcd (R : Type u) [CommRing R] {x y : R} [Submodule.IsPrincipal (Ideal.span {x, y})] [IsDomain R] [GCDMonoid R] : Associated (IsBezout.gcd x y) (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

Equations

• ⋯ = ⋯

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

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

@[deprecated irreducible_iff_prime]

theorem PrincipalIdealRing.irreducible_iff_prime {M : Type u_1} [CancelCommMonoidWithZero M] [DecompositionMonoid M] {a : M} : Irreducible a ↔ Prime a

Alias of irreducible_iff_prime.

@[deprecated associates_irreducible_iff_prime]

theorem PrincipalIdealRing.associates_irreducible_iff_prime {M : Type u_1} [CancelCommMonoidWithZero M] [DecompositionMonoid M] {p : Associates M} : Irreducible p ↔ Prime p

Alias of associates_irreducible_iff_prime.

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

Equations

• PrincipalIdealRing.factors a = if h : a = 0 then ∅ else Classical.choose ⋯

theorem PrincipalIdealRing.factors_spec {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (a : R) (h : a ≠ 0) : (∀ b ∈ PrincipalIdealRing.factors a, Irreducible b) ∧ Associated (PrincipalIdealRing.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 ∈ PrincipalIdealRing.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 ∈ PrincipalIdealRing.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] [Semiring S] (f : R →+* S) (s : Submonoid S) (a : R) (ha : a ≠ 0) (h : ∀ b ∈ PrincipalIdealRing.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

Equations

• ⋯ = ⋯

theorem Submodule.IsPrincipal.map {R : Type u} {M : Type v} {N : Type u_2} [Ring R] [AddCommGroup M] [AddCommGroup 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} [Ring R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) (S : Submodule R N) [hI : (Submodule.comap f S).IsPrincipal] : S.IsPrincipal

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

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

theorem IsPrincipalIdealRing.of_surjective {R : Type u} {S : Type u_1} {F : Type u_3} [Ring R] [Ring 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 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_coprime {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_coprime {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.coprime_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 {gcd x y} = Ideal.span {IsBezout.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

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.

Equations

• nonPrincipals R = {I : Ideal R | ¬Submodule.IsPrincipal I}

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

theorem nonPrincipals_eq_empty_iff {R : Type u} [CommRing R] : nonPrincipals R = ∅ ↔ IsPrincipalIdealRing R

theorem nonPrincipals_zorn {R : Type u} [CommRing R] (c : Set (Ideal R)) (hs : c ⊆ nonPrincipals R) (hchain : IsChain (fun (x1 x2 : Ideal R) => x1 ≤ x2) c) {K : Ideal R} (hKmem : K ∈ 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.)