# Homotopy Type Theory Sandbox > history (changes)

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.

# 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$.

$\prod_{x:R} \prod_{y:R} (x = y) + (x = y) \to (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$.

$\mathrm{isLeftRegular}(e) \coloneqq \prod_{a:R} \prod_{b:R} (e \cdot a = e \cdot b) \to (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$.

$\mathrm{isRightRegular}(e) \coloneqq \prod_{a:R} \prod_{b:R} (a \cdot e = b \cdot e) \to (a = b)$

An term $e:R$ is regular if it is both left regular and right regular.

$\mathrm{isRegular}(e) \coloneqq \mathrm{isLeftRegular}(e) \times \mathrm{isRightRegular}(e)$

The multiplicative monoid of regular elements in $R$ is the submonoid of all regular elements in $R$

$\mathrm{Reg}(R) \coloneqq \sum_{e:R} \mathrm{isRegular}(e)$

### Non-regular elements and integral rings

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

$\mathrm{isNonRegular}(x) \coloneqq \mathrm{isRegular}(x) \to (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:

$\mathrm{isContr}\left(\sum_{x:R} \mathrm{isNonRegular}(x)\right)$

### 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.

$\mathrm{isLeftInvertible}(e) \coloneqq \left[\sum_{a:R} a \cdot e = 1\right]$

A term $e:R$ is right invertible if the fiber of left multiplication by $e$ at $1$ is inhabited.

$\mathrm{isRightInvertible}(e) \coloneqq \left[\sum_{a:R} e \cdot a = 1\right]$

An term $e:R$ is invertible if it is both left invertible and right invertible.

$\mathrm{isInvertible}(e) \coloneqq \mathrm{isLeftInvertible}(e) \times \mathrm{isRightInvertible}(e)$

The multiplicative group of invertible elements in $R$ is the subgroup of all invertible elements in $R$

$R^\times \coloneqq \sum_{e:R} \mathrm{isInvertible}(e)$

### Non-invertible elements and fields

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

$\mathrm{isNonInvertible}(x) \coloneqq \mathrm{isInvertible}(x) \to (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:

$\mathrm{isContr}\left(\sum_{x:R} \mathrm{isNonInvertible}(x)\right)$

### References

• 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.