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 $R$ is trivial if $0 = 1$.
A commutative ring $R$ is discrete if for all elements $x:R$ and $y:R$, either $x = y$, or $x = y$ implies $0 = 1$.
Given a commutative ring $R$, a term $e:R$ is left regular if for all $a:R$ and $b:R$, $e \cdot a = e \cdot b$ implies $a = b$.
A term $e:R$ is right regular if for all $a:R$ and $b:R$, $a \cdot e = b \cdot e$ implies $a = b$.
An term $e:R$ is regular if it is both left regular and right regular.
The multiplicative monoid of regular elements in $R$ is the submonoid of all regular elements in $R$
An element $x:R$ is non-regular if $x$ being regular implies that $0 = 1$
Zero is always a non-regular element of $R$. By definition of non-regular, if $0$ is regular, then the ring $R$ is trivial.
A commutative ring is integral if the type of all non-regular elements in $R$ is contractible:
Given a commutative ring $R$, a term $e:R$ is left invertible if the fiber of right multiplication by $e$ at $1$ is inhabited.
A term $e:R$ is right invertible if the fiber of left multiplication by $e$ at $1$ is inhabited.
An term $e:R$ is invertible if it is both left invertible and right invertible.
The multiplicative group of invertible elements in $R$ is the subgroup of all invertible elements in $R$
An element $x:R$ is non-invertible if $x$ being invertible implies that $0 = 1$
Zero is always a non-invertible element of $R$. By definition of non-invertible, if $0$ is invertible, then the ring $R$ is trivial.
A commutative ring is a field if the type of all non-invertible elements in $R$ 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.