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

# 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 principal_ideal_ring namespace.

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

# Main results #

• 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} [Ring R] [] [Module R M] :
.IsPrincipal
Equations
• =
instance top_isPrincipal {R : Type u} [Ring R] :
.IsPrincipal
Equations
• =
class IsBezout (R : Type u) [Ring R] :

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

• isPrincipal_of_FG : ∀ (I : ), I.FG

Any finitely generated ideal is principal.

Instances
theorem IsBezout.isPrincipal_of_FG {R : Type u} [Ring R] [self : ] (I : ) :
I.FG

Any finitely generated ideal is principal.

@[instance 100]
Equations
• =
@[instance 100]
Equations
• =
noncomputable def Submodule.IsPrincipal.generator {R : Type u} {M : Type v} [] [Ring R] [Module R M] (S : ) [S.IsPrincipal] :
M

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

Equations
Instances For
theorem Submodule.IsPrincipal.span_singleton_generator {R : Type u} {M : Type v} [] [Ring R] [Module R M] (S : ) [S.IsPrincipal] :
@[simp]
theorem Ideal.span_singleton_generator {R : Type u} [Ring R] (I : ) :
@[simp]
theorem Submodule.IsPrincipal.generator_mem {R : Type u} {M : Type v} [] [Ring R] [Module R M] (S : ) [S.IsPrincipal] :
theorem Submodule.IsPrincipal.mem_iff_eq_smul_generator {R : Type u} {M : Type v} [] [Ring R] [Module R M] (S : ) [S.IsPrincipal] {x : M} :
x S ∃ (s : R),
theorem Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero {R : Type u} {M : Type v} [] [Ring R] [Module R M] (S : ) [S.IsPrincipal] :
theorem Submodule.IsPrincipal.mem_iff_generator_dvd {R : Type u} [] (S : ) {x : R} :
x S
theorem Submodule.IsPrincipal.prime_generator_of_isPrime {R : Type u} [] (S : ) [is_prime : S.IsPrime] (ne_bot : S ) :
theorem Submodule.IsPrincipal.generator_map_dvd_of_mem {R : Type u} {M : Type v} [] [] [Module R M] {N : } (ϕ : M →ₗ[R] R) [().IsPrincipal] {x : M} (hx : x N) :
theorem Submodule.IsPrincipal.generator_submoduleImage_dvd_of_mem {R : Type u} {M : Type v} [] [] [Module R M] {N : } {O : } (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] [] (x : R) (y : R) :
Equations
• =
noncomputable def IsBezout.gcd {R : Type u} [Ring R] (x : R) (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
Instances For
theorem IsBezout.span_gcd {R : Type u} [Ring R] (x : R) (y : R) [Submodule.IsPrincipal (Ideal.span {x, y})] :
theorem IsBezout.gcd_dvd_left {R : Type u} [] (x : R) (y : R) [Submodule.IsPrincipal (Ideal.span {x, y})] :
x
theorem IsBezout.gcd_dvd_right {R : Type u} [] (x : R) (y : R) [Submodule.IsPrincipal (Ideal.span {x, y})] :
y
theorem IsBezout.dvd_gcd {R : Type u} [] {x : R} {y : R} {z : R} [Submodule.IsPrincipal (Ideal.span {x, y})] (hx : z x) (hy : z y) :
z
theorem IsBezout.gcd_eq_sum {R : Type u} [] (x : R) (y : R) [Submodule.IsPrincipal (Ideal.span {x, y})] :
∃ (a : R) (b : R), a * x + b * y =
theorem IsRelPrime.isCoprime {R : Type u} [] {x : R} {y : R} [Submodule.IsPrincipal (Ideal.span {x, y})] (h : ) :
theorem isRelPrime_iff_isCoprime {R : Type u} [] {x : R} {y : R} [Submodule.IsPrincipal (Ideal.span {x, y})] :
noncomputable def IsBezout.toGCDDomain (R : Type u) [] [] [] [] :

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
Instances For
instance IsBezout.nonemptyGCDMonoid (R : Type u) [] [] [] :
Equations
• =
theorem IsBezout.associated_gcd_gcd (R : Type u) [] {x : R} {y : R} [Submodule.IsPrincipal (Ideal.span {x, y})] [] [] :
Associated () (gcd x y)
theorem IsPrime.to_maximal_ideal {R : Type u} [] [] {S : } [hpi : S.IsPrime] (hS : S ) :
S.IsMaximal
theorem mod_mem_iff {R : Type u} [] {S : } {x : R} {y : R} (hy : y S) :
x % y S x S
@[instance 100]
Equations
• =
theorem IsField.isPrincipalIdealRing {R : Type u_1} [] (h : ) :
@[instance 100]
Equations
• =
@[deprecated irreducible_iff_prime]
theorem PrincipalIdealRing.irreducible_iff_prime {α : Type u_1} {a : α} :

Alias of irreducible_iff_prime.

@[deprecated associates_irreducible_iff_prime]

Alias of associates_irreducible_iff_prime.

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

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

Equations
• = if h : a = 0 then else
Instances For
theorem PrincipalIdealRing.factors_spec {R : Type u} [] [] (a : R) (h : a 0) :
() Associated .prod a
theorem PrincipalIdealRing.ne_zero_of_mem_factors {R : Type v} [] [] {a : R} {b : R} (ha : a 0) (hb : ) :
b 0
theorem PrincipalIdealRing.mem_submonoid_of_factors_subset_of_units_subset {R : Type u} [] [] (s : ) {a : R} (ha : a 0) (hfac : b, 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} [] [] [] (f : R →+* S) (s : ) (a : R) (ha : a 0) (h : b, 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]

A principal ideal domain has unique factorization

Equations
• =
theorem Submodule.IsPrincipal.of_comap {R : Type u} {M : Type v} {N : Type u_2} [Ring R] [] [] [Module R M] [Module R N] (f : M →ₗ[R] N) (hf : ) (S : ) [hI : ().IsPrincipal] :
S.IsPrincipal
theorem Ideal.IsPrincipal.of_comap {R : Type u} {S : Type u_1} [Ring R] [Ring S] (f : R →+* S) (hf : ) (I : ) [hI : ] :
theorem IsPrincipalIdealRing.of_surjective {R : Type u} {S : Type u_1} [Ring R] [Ring S] (f : R →+* S) (hf : ) :

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

theorem IsBezout.span_gcd_eq_span_gcd {R : Type u} [] [] [] [] (x : R) (y : R) :
theorem span_gcd {R : Type u} [] [] [] [] (x : R) (y : R) :
Ideal.span {gcd x y} = Ideal.span {x, y}
theorem gcd_dvd_iff_exists {R : Type u} [] [] [] [] (a : R) (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} [] [] [] [] (a : R) (b : R) :
∃ (x : R) (y : R), gcd a b = a * x + b * y

Bézout's lemma

theorem gcd_isUnit_iff {R : Type u} [] [] [] [] (x : R) (y : R) :
IsUnit (gcd x y)
theorem isCoprime_of_dvd {R : Type u} [] [] (x : R) (y : R) (nonzero : ¬(x = 0 y = 0)) (H : z, z 0z x¬z y) :
theorem dvd_or_coprime {R : Type u} [] [] (x : R) (y : R) (h : ) :
x y
theorem Irreducible.coprime_iff_not_dvd {R : Type u} [] [] {p : R} {n : R} (hp : ) :
¬p n

See also Irreducible.isRelPrime_iff_not_dvd.

theorem Prime.coprime_iff_not_dvd {R : Type u} [] [] [] {p : R} {n : R} (hp : ) :
¬p n
theorem Irreducible.dvd_iff_not_coprime {R : Type u} [] [] {p : R} {n : R} (hp : ) :
p n ¬

See also Irreducible.coprime_iff_not_dvd'.

theorem Irreducible.coprime_pow_of_not_dvd {R : Type u} [] [] {p : R} {a : R} (m : ) (hp : ) (h : ¬p a) :
IsCoprime a (p ^ m)
theorem Irreducible.coprime_or_dvd {R : Type u} [] [] {p : R} (hp : ) (i : R) :
p i
theorem exists_associated_pow_of_mul_eq_pow' {R : Type u} [] [] [] {a : R} {b : R} {c : R} (hab : ) {k : } (h : a * b = c ^ k) :
∃ (d : R), Associated (d ^ k) a
theorem isCoprime_of_irreducible_dvd {R : Type u} [] [] {x : R} {y : R} (nonzero : ¬(x = 0 y = 0)) (H : ∀ (z : R), z x¬z y) :
theorem isCoprime_of_prime_dvd {R : Type u} [] [] {x : R} {y : R} (nonzero : ¬(x = 0 y = 0)) (H : ∀ (z : R), z x¬z y) :
def nonPrincipals (R : Type u) [] :
Set ()

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

Equations
• = {I : | }
Instances For
theorem nonPrincipals_def (R : Type u) [] {I : } :
theorem nonPrincipals_zorn {R : Type u} [] (c : Set ()) (hs : ) (hchain : IsChain (fun (x x_1 : ) => x x_1) c) {K : } (hKmem : K c) :
I, Jc, 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 IsPrincipalIdealRing.of_prime {R : Type u} [] (H : ∀ (P : ), P.IsPrime) :

If all prime ideals in a commutative ring are principal, so are all other ideals.