# mathlib3documentation

ring_theory.principal_ideal_domain

# Principal ideal rings and principal ideal domains #

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

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 [is_domain R] [is_principal_ideal_ring R]. There is no explicit definition of a PID. Theorems about PID's are in the principal_ideal_ring namespace.

• is_principal_ideal_ring: a predicate on rings, saying that every 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.
• euclidean_domain.to_principal_ideal_domain : a Euclidean domain is a PID.
@[class]
structure submodule.is_principal {R : Type u} {M : Type v} [ring R] [ M] (S : M) :
Prop
• principal : (a : M), S = {a}

An R-submodule of M is principal if it is generated by one element.

Instances of this typeclass
theorem submodule.is_principal_iff {R : Type u} {M : Type v} [ring R] [ M] (S : M) :
S.is_principal (a : M), S = {a}
@[protected, instance]
def bot_is_principal {R : Type u} {M : Type v} [ring R] [ M] :
@[protected, instance]
def top_is_principal {R : Type u} [ring R] :
@[class]
structure is_principal_ideal_ring (R : Type u) [ring R] :
Prop

A ring is a principal ideal ring if all (left) ideals are principal.

Instances of this typeclass
theorem is_principal_ideal_ring_iff (R : Type u) [ring R] :
(S : ideal R),
@[protected, instance]
noncomputable def submodule.is_principal.generator {R : Type u} {M : Type v} [ring R] [ M] (S : M) [S.is_principal] :
M

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

Equations
theorem submodule.is_principal.span_singleton_generator {R : Type u} {M : Type v} [ring R] [ M] (S : M) [S.is_principal] :
theorem ideal.span_singleton_generator {R : Type u} [ring R] (I : ideal R)  :
@[simp]
theorem submodule.is_principal.generator_mem {R : Type u} {M : Type v} [ring R] [ M] (S : M) [S.is_principal] :
theorem submodule.is_principal.mem_iff_eq_smul_generator {R : Type u} {M : Type v} [ring R] [ M] (S : M) [S.is_principal] {x : M} :
x S (s : R),
theorem submodule.is_principal.eq_bot_iff_generator_eq_zero {R : Type u} {M : Type v} [ring R] [ M] (S : M) [S.is_principal] :
theorem submodule.is_principal.mem_iff_generator_dvd {R : Type u} [comm_ring R] (S : ideal R) {x : R} :
x S
theorem submodule.is_principal.prime_generator_of_is_prime {R : Type u} [comm_ring R] (S : ideal R) [is_prime : S.is_prime] (ne_bot : S ) :
theorem submodule.is_principal.generator_map_dvd_of_mem {R : Type u} {M : Type v} [comm_ring R] [ M] {N : M} (ϕ : M →ₗ[R] R) [ N).is_principal] {x : M} (hx : x N) :
theorem submodule.is_principal.generator_submodule_image_dvd_of_mem {R : Type u} {M : Type v} [comm_ring R] [ M] {N O : M} (hNO : N O) (ϕ : O →ₗ[R] R) [(ϕ.submodule_image N).is_principal] {x : M} (hx : x N) :
ϕ x, _⟩
theorem is_prime.to_maximal_ideal {R : Type u} [comm_ring R] [is_domain R] {S : ideal R} [hpi : S.is_prime] (hS : S ) :
theorem mod_mem_iff {R : Type u} {S : ideal R} {x y : R} (hy : y S) :
x % y S x S
@[protected, instance]
@[protected, instance]
noncomputable def principal_ideal_ring.factors {R : Type u} [comm_ring R] [is_domain R] (a : R) :

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

Equations
theorem principal_ideal_ring.factors_spec {R : Type u} [comm_ring R] [is_domain R] (a : R) (h : a 0) :
( (b : R),
theorem principal_ideal_ring.ne_zero_of_mem_factors {R : Type v} [comm_ring R] [is_domain R] {a b : R} (ha : a 0) (hb : b ) :
b 0
theorem principal_ideal_ring.mem_submonoid_of_factors_subset_of_units_subset {R : Type u} [comm_ring R] [is_domain R] (s : submonoid R) {a : R} (ha : a 0) (hfac : (b : R), b s) (hunit : (c : Rˣ), c s) :
a s
theorem principal_ideal_ring.ring_hom_mem_submonoid_of_factors_subset_of_units_subset {R : Type u_1} {S : Type u_2} [comm_ring R] [is_domain R] [semiring S] (f : R →+* S) (s : submonoid S) (a : R) (ha : a 0) (h : (b : R), f b s) (hf : (c : Rˣ), f c s) :
f a s

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

@[protected, instance]

A principal ideal domain has unique factorization

theorem submodule.is_principal.of_comap {R : Type u} {M : Type v} {N : Type u_2} [ring R] [ M] [ N] (f : M →ₗ[R] N) (hf : function.surjective f) (S : N) [hI : S).is_principal] :
theorem ideal.is_principal.of_comap {R : Type u} {S : Type u_1} [ring R] [ring S] (f : R →+* S) (hf : function.surjective f) (I : ideal S) [hI : submodule.is_principal I)] :
theorem is_principal_ideal_ring.of_surjective {R : Type u} {S : Type u_1} [ring R] [ring S] (f : R →+* S) (hf : function.surjective f) :

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

theorem span_gcd {R : Type u} [comm_ring R] [is_domain R] [gcd_monoid R] (x y : R) :
theorem gcd_dvd_iff_exists {R : Type u} [comm_ring R] [is_domain R] [gcd_monoid R] (a b : R) {z : R} :
z (x y : R), z = a * x + b * y
theorem exists_gcd_eq_mul_add_mul {R : Type u} [comm_ring R] [is_domain R] [gcd_monoid R] (a b : R) :
(x y : R), = a * x + b * y

Bézout's lemma

theorem gcd_is_unit_iff {R : Type u} [comm_ring R] [is_domain R] [gcd_monoid R] (x y : R) :
theorem is_coprime_of_dvd {R : Type u} [comm_ring R] [is_domain R] [gcd_monoid R] (x y : R) (nonzero : ¬(x = 0 y = 0)) (H : (z : R), z z 0 z x ¬z y) :
y
theorem dvd_or_coprime {R : Type u} [comm_ring R] [is_domain R] [gcd_monoid R] (x y : R) (h : irreducible x) :
x y y
theorem is_coprime_of_irreducible_dvd {R : Type u} [comm_ring R] [is_domain R] [gcd_monoid R] {x y : R} (nonzero : ¬(x = 0 y = 0)) (H : (z : R), z x ¬z y) :
y
theorem is_coprime_of_prime_dvd {R : Type u} [comm_ring R] [is_domain R] [gcd_monoid R] {x y : R} (nonzero : ¬(x = 0 y = 0)) (H : (z : R), z x ¬z y) :
y
theorem irreducible.coprime_iff_not_dvd {R : Type u} [comm_ring R] [is_domain R] [gcd_monoid R] {p n : R} (pp : irreducible p) :
n ¬p n
theorem prime.coprime_iff_not_dvd {R : Type u} [comm_ring R] [is_domain R] [gcd_monoid R] {p n : R} (pp : prime p) :
n ¬p n
theorem irreducible.dvd_iff_not_coprime {R : Type u} [comm_ring R] [is_domain R] [gcd_monoid R] {p n : R} (hp : irreducible p) :
p n ¬ n
theorem irreducible.coprime_pow_of_not_dvd {R : Type u} [comm_ring R] [is_domain R] [gcd_monoid R] {p a : R} (m : ) (hp : irreducible p) (h : ¬p a) :
(p ^ m)
theorem irreducible.coprime_or_dvd {R : Type u} [comm_ring R] [is_domain R] [gcd_monoid R] {p : R} (hp : irreducible p) (i : R) :
i p i
theorem exists_associated_pow_of_mul_eq_pow' {R : Type u} [comm_ring R] [is_domain R] [gcd_monoid R] {a b c : R} (hab : b) {k : } (h : a * b = c ^ k) :
(d : R), associated (d ^ k) a
def non_principals (R : Type u) [comm_ring R] :

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

Equations
• = {I : |
theorem non_principals_def (R : Type u) [comm_ring R] {I : ideal R} :
theorem non_principals_zorn {R : Type u} [comm_ring R] (c : set (ideal R)) (hs : c ) (hchain : c) {K : ideal R} (hKmem : K c) :
(I : ideal R) (H : I , (J : ideal 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.)

theorem is_principal_ideal_ring.of_prime {R : Type u} [comm_ring R] (H : (P : ideal R), ) :

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