Showing changes from revision #73 to #74:
Added | Removed | Changed
As of 6 June 2022, the HoTT web is regarded as deprecated. The vast majority of the articles have since been ported to the main nLab web. All further HoTT-related editing should happen on the main nLab web.
A commutative ring is trivial if .
A commutative ring is discrete if for all elements and , either , or implies .
Given a commutative ring , a term is left regular if for all and , implies .
A term is right regular if for all and , implies .
An term is regular if it is both left regular and right regular.
The multiplicative monoid of regular elements in is the submonoid of all regular elements in
An element is non-regular if being regular implies that
Zero is always a non-regular element of . By definition of non-regular, if is regular, then the ring is trivial.
A commutative ring is integral if the type of all non-regular elements in is contractible:
Given a commutative ring , a term is left invertible if the fiber of right multiplication by at is inhabited.
A term is right invertible if the fiber of left multiplication by at is inhabited.
An term is invertible if it is both left invertible and right invertible.
The multiplicative group of invertible elements in is the subgroup of all invertible elements in
An element is non-invertible if being invertible implies that
Zero is always a non-invertible element of . By definition of non-invertible, if is invertible, then the ring is trivial.
A commutative ring is a field if the type of all non-invertible elements in is contractible:
Frank Quinn, Proof Projects for Teachers (pdf)
Henri Lombardi, Claude Quitté, Commutative algebra: Constructive methods (Finite projective modules) (arXiv:1605.04832)
Last revised on June 19, 2022 at 23:05:26. See the history of this page for a list of all contributions to it.