## 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$. $$\mathrm{isLeftCancellative}(e) \coloneqq \prod_{a:R} \prod_{b :R}(e \cdot a = e \cdot b) \to (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$. $$\mathrm{isRightCancellative}(e) \coloneqq \prod_{a:R} \prod_{b :R}(a \cdot e = b \cdot e) \to (a = b)$$ An term $e:R$ is *cancellative* if it is both left cancellative and right cancellative. $$\mathrm{isCancellative}(e) \coloneqq \mathrm{isLeftCancellative}(e) \times \mathrm{isRightCancellative}(e)$$ The **monoid of cancellative elements in $R$** is the subset of all cancellative elements in $R$ $$\mathrm{Can}(R) \coloneqq \sum_{e:R} \mathrm{isCancellative}(e)$$ ### 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 \sum_{a:R} a \cdot e = 1$$ A term $e:R$ is *right invertible* if the fiber of left multiplication by $e$ at $1$ is inhabited. $$\mathrm{isRightInvertible}(e) \coloneqq \sum_{a:R} e \cdot a = 1$$ An term $e:R$ is *invertible* or a *unit* if it is both left invertible and right invertible. $$\mathrm{isInvertible}(e) \coloneqq \mathrm{isLeftInvertible}(e) \times \mathrm{isRightInvertible}(e)$$ The **group of units in $R$** is the subset of all units in $R$ $$R^\times \coloneqq \sum_{e:R} \mathrm{isInvertible}(e)$$ ### 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](https://personal.math.vt.edu/fquinn/education/pfs4teachers0.pdf)) * Henri Lombardi, Claude Quitté, *Commutative algebra: Constructive methods (Finite projective modules)* ([arXiv:1605.04832](https://arxiv.org/abs/1605.04832)) category: not redirected to nlab yet