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]
[add_comm_group M]
[module R M]
(S : submodule R M) :
Prop
- principal : ∃ (a : M), S = submodule.span R {a}
An R-submodule of M is principal if it is generated by one element.
@[class]
- principal : ∀ (S : ideal R), submodule.is_principal S
A commutative ring is a principal ideal ring if all ideals are principal.
def
submodule.is_principal.generator
{R : Type u}
{M : Type v}
[comm_ring R]
[add_comm_group M]
[module R M]
(S : submodule R 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]
[add_comm_group M]
[module R M]
(S : submodule R M)
[S.is_principal] :
@[simp]
theorem
submodule.is_principal.generator_mem
{R : Type u}
{M : Type v}
[comm_ring R]
[add_comm_group M]
[module R M]
(S : submodule R M)
[S.is_principal] :
theorem
submodule.is_principal.mem_iff_eq_smul_generator
{R : Type u}
{M : Type v}
[comm_ring R]
[add_comm_group M]
[module R M]
(S : submodule R M)
[S.is_principal]
{x : M} :
x ∈ S ↔ ∃ (s : R), x = s • submodule.is_principal.generator S
theorem
submodule.is_principal.mem_iff_generator_dvd
{R : Type u}
[comm_ring R]
(S : ideal R)
[submodule.is_principal S]
{x : R} :
x ∈ S ↔ submodule.is_principal.generator S ∣ x
theorem
submodule.is_principal.eq_bot_iff_generator_eq_zero
{R : Type u}
{M : Type v}
[comm_ring R]
[add_comm_group M]
[module R M]
(S : submodule R M)
[S.is_principal] :
S = ⊥ ↔ submodule.is_principal.generator S = 0
theorem
is_prime.to_maximal_ideal
{R : Type u}
[integral_domain R]
[is_principal_ideal_ring R]
{S : ideal R}
[hpi : S.is_prime]
(hS : S ≠ ⊥) :
@[instance]
@[instance]
def
principal_ideal_ring.is_noetherian_ring
{R : Type u}
[integral_domain R]
[is_principal_ideal_ring R] :
theorem
principal_ideal_ring.is_maximal_of_irreducible
{R : Type u}
[integral_domain R]
[is_principal_ideal_ring R]
{p : R}
(hp : irreducible p) :
ideal.is_maximal (submodule.span R {p})
theorem
principal_ideal_ring.irreducible_iff_prime
{R : Type u}
[integral_domain R]
[is_principal_ideal_ring R]
{p : R} :
irreducible p ↔ prime p
theorem
principal_ideal_ring.associates_irreducible_iff_prime
{R : Type u}
[integral_domain R]
[is_principal_ideal_ring R]
{p : associates R} :
irreducible p ↔ prime p
def
principal_ideal_ring.factors
{R : Type u}
[integral_domain R]
[is_principal_ideal_ring R]
(a : R) :
multiset R
factors a is a multiset of irreducible elements whose product is a, up to units
Equations
- principal_ideal_ring.factors a = dite (a = 0) (λ (h : a = 0), ∅) (λ (h : ¬a = 0), classical.some _)
theorem
principal_ideal_ring.factors_spec
{R : Type u}
[integral_domain R]
[is_principal_ideal_ring R]
(a : R)
(h : a ≠ 0) :
(∀ (b : R), b ∈ principal_ideal_ring.factors a → irreducible b) ∧ associated (principal_ideal_ring.factors a).prod a
theorem
principal_ideal_ring.ne_zero_of_mem_factors
{R : Type v}
[integral_domain R]
[is_principal_ideal_ring R]
{a b : R}
(ha : a ≠ 0)
(hb : b ∈ principal_ideal_ring.factors a) :
b ≠ 0
theorem
principal_ideal_ring.mem_submonoid_of_factors_subset_of_units_subset
{R : Type u}
[integral_domain R]
[is_principal_ideal_ring R]
(s : submonoid R)
{a : R}
(ha : a ≠ 0)
(hfac : ∀ (b : R), b ∈ principal_ideal_ring.factors a → b ∈ s)
(hunit : ∀ (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}
[integral_domain R]
[is_principal_ideal_ring R]
[semiring S]
(f : R →+* S)
(s : submonoid S)
(a : R)
(ha : a ≠ 0)
(h : ∀ (b : R), b ∈ principal_ideal_ring.factors a → ⇑f b ∈ s)
(hf : ∀ (c : units R), ⇑f ↑c ∈ 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]
def
principal_ideal_ring.to_unique_factorization_monoid
{R : Type u}
[integral_domain R]
[is_principal_ideal_ring R] :
A principal ideal domain has unique factorization