# mathlibdocumentation

ring_theory.principal_ideal_domain

# Principal ideal rings and principal ideal domains

A principal ideal ring (PIR) is a commutative ring in which all 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 [integral 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 commutative rings, saying that every 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] :
M → Prop
• principal : ∃ (a : M), S = {a}

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

Instances
@[class]
structure is_principal_ideal_ring (R : Type u) [comm_ring R] :
Prop
• principal : ∀ (S : ideal R),

A commutative ring is a principal ideal ring if all ideals are principal.

Instances
def submodule.is_principal.generator {R : Type u} {M : Type v} [comm_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} [comm_ring R] [ M] (S : M) [S.is_principal] :

@[simp]
theorem submodule.is_principal.generator_mem {R : Type u} {M : Type v} [comm_ring R] [ M] (S : M) [S.is_principal] :

theorem submodule.is_principal.mem_iff_eq_smul_generator {R : Type u} {M : Type v} [comm_ring R] [ M] (S : M) [S.is_principal] {x : M} :
x S ∃ (s : R),

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.eq_bot_iff_generator_eq_zero {R : Type u} {M : Type v} [comm_ring R] [ M] (S : M) [S.is_principal] :

theorem is_prime.to_maximal_ideal {R : Type u} {S : ideal R} [hpi : S.is_prime] :

theorem mod_mem_iff {R : Type u} {S : ideal R} {x y : R} :
y S(x % y S x S)

@[instance]

@[instance]

theorem principal_ideal_ring.irreducible_iff_prime {R : Type u} {p : R} :

def principal_ideal_ring.factors {R : Type u}  :
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} (a : R) :
a 0(∀ (b : R),

theorem principal_ideal_ring.ne_zero_of_mem_factors {R : Type v} {a b : R} :
a 0b 0

theorem principal_ideal_ring.mem_submonoid_of_factors_subset_of_units_subset {R : Type u} (s : submonoid R) {a : R} :
a 0(∀ (b : R), b s)(∀ (c : units 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} [semiring S] (f : R →+* S) (s : submonoid S) (a : R) :
a 0(∀ (b : R), f b s)(∀ (c : units 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.

@[instance]

A principal ideal domain has unique factorization