Homotopy Type Theory Sandbox (Rev #71)

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$

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-regular and non-invertible elements

An element $x:R$ is non-regular if $x$ being regular implies that $0 = 1$

An element $x:R$ is non-invertible if $x$ being invertible implies that $0 = 1$

Zero is always a non-regular and non-invertible element of $R$. By definition of non-regular and non-invertible, if $0$ is regular or invertible, then the ring $R$ is trivial.

A commutative ring is integral if every non-regular element is equal to zero. A commutative ring is a field if every non-invertible element is equal to zero.

References

• Frank Quinn, Proof Projects for Teachers (pdf)

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