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.

Contents

Commutative algebra

Trivial ring

A commutative ring $R$ is trivial if $0 = 1$.

Discrete rings

A commutative ring $R$ is discrete if for all elements $x:R$ and $y:R$, either $x = y$, or $x = y$ implies $0 = 1$.

Regular elements

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$

Non-regular elements and integral rings

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:

Invertible elements

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$

Non-invertible elements and fields

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:

References

• Frank Quinn, Proof Projects for Teachers (pdf)

• Henri Lombardi, Claude Quitté, Commutative algebra: Constructive methods (Finite projective modules) (arXiv:1605.04832)