Local rings #
Define local rings as commutative rings having a unique maximal ideal.
Main definitions #
local_ring: A predicate on commutative rings, stating that every element
ais either a unit or
1 - ais a unit. This is shown to be equivalent to the condition that there exists a unique maximal ideal.
local_ring.maximal_ideal: The unique maximal ideal for a local rings. Its carrier set is the set of non units.
is_local_ring_hom: A predicate on semiring homomorphisms, requiring that it maps nonunits to nonunits. For local rings, this means that the image of the unique maximal ideal is again contained in the unique maximal ideal.
local_ring.residue_field: The quotient of a local ring by its maximal ideal.
A commutative ring is local if it has a unique maximal ideal. Note that
local_ring is a predicate.
A local ring homomorphism is a homomorphism between local rings such that the image of the maximal ideal of the source is contained within the maximal ideal of the target.
The map on residue fields induced by a local homomorphism between local rings