Principal ideal rings and principal ideal domains #
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
IsPrincipalIdealRing: 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 #
RingHom maps all units and all factors of an element
a into a submonoid
s, then it
a into that submonoid.
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.)