Local rings #
Define local rings as commutative rings having a unique maximal ideal.
Main definitions #
LocalRing: A predicate on commutative semirings, stating that for any pair of elements that adds up to
1, one of them is a unit. This is shown to be equivalent to the condition that there exists a unique maximal ideal.
LocalRing.maximalIdeal: The unique maximal ideal for a local rings. Its carrier set is the set of non units.
IsLocalRingHom: 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.
LocalRing.ResidueField: The quotient of a local ring by its maximal ideal.
- of_is_unit_or_is_unit_of_add_one :: (
- exists_pair_ne : ∃ x y, x ≠ y
in a local ring
a + b = 1, then either
ais a unit or
bis a unit. In another word, for every
a : R, either
ais a unit or
1 - ais a unit.
A semiring is local if it is nontrivial and
b is a unit whenever
a + b = 1.
LocalRing is a predicate.
A local ring homomorphism
f : R ⟶ Swill send nonunits of
Rto nonunits of
A local ring homomorphism is a homomorphism
f between local rings such that
a in the domain
is a unit if
f a is a unit for any
LocalRing.local_hom_TFAE for other equivalent
The image of the maximal ideal of the source is contained within the maximal ideal of the target.
A ring homomorphism between local rings is a local ring hom iff it reflects units, i.e. any preimage of a unit is still a unit. https://stacks.math.columbia.edu/tag/07BJ