#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)$$ ### 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-regular and non-invertible elements ### 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)$$ 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-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](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)) ## Real numbers ### Pointed abelian groups ### A **pointed abelian group** is a set $A$ with an element $1:A$ called **one** and a binary operation $(-)-(-):A \times A \to A$ called **subtraction** such that * for all elements $a:A$, $a - a = 1 - 1$ * for all elements $a:A$, $(1 - 1) - ((1 - 1) - a) = a$ * for all elements $a:A$ and $b:A$, $a - ((1 - 1) - b) = b - ((1 - 1) - a)$ * for all elements $a:A$, $b:A$, and $c:A$, $a - (b - c) = (a - ((1 - 1) - c)) - b$ ### Pointed halving groups ### A **pointed halving group** is a pointed abelian group *G* with a function $(-)/2:G \to G$ called **halving** or **dividing by two** such that for all elements $g:G$, $g/2 = g - g/2$. ### Totally ordered pointed halving groups ### A pointed halving group $R$ is a totally ordered pointed halving group if it comes with a function $\max:R \times R \to R$ such that * for all elements $a:R$, $\max(a, a) = a$ * for all elements $a:R$ and $b:R$, $\max(a, b) = \max(b, a)$ * for all elements $a:R$, $b:R$, and $c:R$, $\max(a, \max(b, c)) = \max(\max(a, b), c)$ * for all elements $a:R$ and $b:R$, $\max(a, b) = a$ or $\max(a, b) = b$ * for all elements $a:R$ and $b:R$, $\max(a, b) = b$ implies that for all elements $c:R$, $\max(a - c, b - c) = b - c$ ### Strictly ordered pointed halving groups ### A totally ordered pointed halving group $R$ is a strictly ordered pointed abelian group if it comes with a type family $\lt$ such that * for all elements $a:R$ and $b:R$, $a \lt b$ is a proposition * for all elements $a:R$, $a \lt a$ is false * for all elements $a:R$, $b:R$, and $c:R$, if $a \lt c$, then $a \lt b$ or $b \lt c$ * for all elements $a:R$ and $b:R$, if $a \lt b$ is false and $b \lt a$ is false, then $a = b$ * for all elements $a:R$ and $b:R$, if $a \lt b$, then $b \lt a$ is false. * $1 - 1 \lt 1$ * for all elements $a:R$ and $b:R$, if $1 - 1 \lt a$ and $1 - 1 \lt b$, then $(1 - 1) \lt a - ((1 - 1) - b)$ The homotopy initial strictly ordered pointed halving group is the dyadic rational numbers $\mathbb{D}$. ### Archimedean ordered pointed halving groups ### A strictly ordered pointed halving group $A$ is an Archimedean ordered pointed halving group if for all elements $a:A$ and $b:A$, if $a \lt b$, then there merely exists a dyadic rational number $d:\mathbb{D}$ such that $a \lt h(d)$ and $h(d) \lt b$. ### Sequentially Cauchy complete Archimedean ordered pointed halving groups ### Let $A$ be an Archimedean ordered pointed halving group and let $$A_{+} \coloneqq \sum_{a:A} 1 - 1 \lt a$$ be the positive elements in $A$. A **sequence** in $A$ is a function $x:\mathbb{N} \to A$. A sequence $x:\mathbb{N} \to A$ is a **Cauchy sequence** if for all positive elements $\epsilon:A_{+}$, there merely exists a natural number $N:\mathbb{N}$ such that for all natural numbers $i:\mathbb{N}$ and $j:\mathbb{N}$ such that $N \leq i$ and $N \leq j$, $\max(x_i - x_j, x_j - x_i) \lt \epsilon$. An element $l:A$ is said to be a **limit** of the sequence $x:\mathbb{N} \to A$ if for all positive elements $\epsilon:A_{+}$, there merely exists a natural number $N:\mathbb{N}$ such that for all natural numbers $i:\mathbb{N}$ such that $N \leq i$, $\max(x_i - l, l - x_i) \lt \epsilon$ $A$ is **sequentially Cauchy complete** if every Cauchy sequence in $A$ merely has a limit. category: not redirected to nlab yet