Homotopy Type Theory Sandbox (Rev #70)

Commutative algebra

Cancellative elements

Given a commutative ring $R$, a term $e:R$ is left cancellative if for all $a:R$ and $b:R$, $e \cdot a = e \cdot b$ implies $a = b$.

A term $e:R$ is right cancellative if for all $a:R$ and $b:R$, $a \cdot e = b \cdot e$ implies $a = b$.

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

The monoid of cancellative elements in $R$ is the subset of all cancellative 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 or a unit if it is both left invertible and right invertible.

The group of units in $R$ is the subset of all units in $R$

Non-cancellative and non-invertible elements

Given a commutative ring $R$, the monoid of cancellative elements in $R$ is denoted as $\mathrm{Can}(R)$ with injection $i:\mathrm{Can}(R) \to R$ and the group of units is denoted as $R^\times$ with injection $j:R^\times \to R$. An element $x \in R$ is non-cancellative if for all elements $y \in \mathrm{Can}(R)$, if $i(y) = x$, then $0 = 1$. An element $x \in R$ is non-invertible if for all elements $y \in R^\times$, if $j(y) = x$, then $0 = 1$.

A commutative ring is an integral domain if every non-cancellative 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)