--- > 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:HomePage|nLab web]]. All further HoTT-related editing should happen on the main [[nLab:HomePage|nLab web]]. --- #Contents# * table of contents {:toc} ## 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](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