[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \tableofcontents types with decidable equality $$a:A, b:A \vdash p(a, b):(a =_A b) + \neg (a =_A b)$$ \section{Commutative rings} A commutative ring is a set $R$ with * a dependent term $x:R, y:R \vdash x + y:R$ * a term $0:R$ * a dependent term $x:R \vdash -x:R$ * a dependent term $x:R, y:R \vdash x \cdot y:R$ * a term $1:R$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{assoc}_+(x, y, z):x + (y + z) =_R (x + y) + z$ * a dependent term $x:R \vdash \mathrm{lunit}_+(x):0 + x =_R x$ * a dependent term $x:R \vdash \mathrm{runit}_+(x):x + 0 =_R x$ * a dependent term $x:R \vdash \mathrm{linv}_+(x):(-x) + x =_R 0$ * a dependent term $x:R \vdash \mathrm{rinv}_+(x):x + (-x) =_R 0$ * a dependent term $x:R, y:R \vdash \mathrm{comm}_+(x, y):x + y =_R y + x$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{assoc}_\cdot(x, y, z):x \cdot (y \cdot z) =_R (x \cdot y) \cdot z$ * a dependent term $x:R \vdash \mathrm{lunit}_\cdot(x):1 \cdot x =_R x$ * a dependent term $x:R \vdash \mathrm{runit}_\cdot(x):x \cdot 1 =_R x$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{ldist}_\cdot(x, y, z):x \cdot (y + z) =_R x \cdot y + x \cdot z$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{rdist}_\cdot(x, y, z):(y + z) \cdot x =_R y \cdot x + z \cdot x$ * a dependent term $x:R, y:R \vdash \mathrm{comm}_\cdot(x, y):x \cdot y =_R y \cdot x$ \section{Local rings} Let $P$ be a predicate on a commutative ring $R$. A commutative ring $R$ is a weak $P$-local ring if the type of all elements $a:R$ for which $P(a)$ is false is an ideal of $R$. A commutative ring $R$ is a $P$-local ring if the type of all elements $a:R$ for which $P(a)$ is true is an anti-ideal of $R$. \section{Field rings} Given a commutative ring $R$, an element $a:R$ is regular if for all $b:R$, and $c:R$ the canonical functions $$\mathrm{idtoleftmul}(a, b, c):(b =_R c) \to (a \cdot b =_R a \cdot c)$$ $$\mathrm{idtorightmul}(a, b, c):(b =_R c) \to (b \cdot a =_R c \cdot a)$$ are equivalences: $$\mathrm{isRegular}(a) \coloneqq \prod_{b:A} \prod_{c:A} \mathrm{isEquiv}(\mathrm{idtoleftmul}(a, b, c)) \times \mathrm{isEquiv}(\mathrm{idtorightmul}(a, b, c))$$ We define the type of regular elements as $$\mathrm{Reg}(R) \coloneqq \sum_{a:A} \mathrm{isRegular}(a)$$ Given a commutative ring $R$, an element $a:R$ is invertible if the type of all $b:B$ such that $a \cdot b =_R 1$ is contractible $$\mathrm{isInvertible}(a) \coloneqq \mathrm{isContr}\left(\sum_{b:B} a \cdot b =_R 1\right)$$ A field ring is a commutative ring $R$ such that every regular element is invertible: $$\prod_{a:A} \mathrm{isRegular}(a) \simeq \mathrm{isInvertible}(a)$$ \section{Integral rings and fields} A zero divisor is an element such that the element being regular implies that the commutative ring is trivial: $$\mathrm{isZeroDivisor}(a) \coloneqq \mathrm{isRegular}(a) \to (0 =_R 1)$$ An integral ring is a commutative ring $R$ such that every zero divisor is equal to zero: $$\prod_{a:A} \mathrm{isZeroDivisor}(a) \simeq (a =_R 0)$$ A field is an integral domain $R$ which is also a field ring. \section{Local rings and Heyting fields} A local ring is a field ring such that for all elements $a:R$ and $b:R$, if $a + b$ is regular, then either $a$ is regular or $b$ is regular. A Heyting field is a local ring which is also a field. \section{Localizations and field rings of fractions} Let $R$ be a commutative ring. The localization of $R$ away from an element $a:R$ is the initial commutative ring $R[a^{-1}]$ with a commutative ring homomorphism $h:R \to R[a^{-1}]$, an element $a^{-1}:R[a^{-1}]$, and an identity $\lambda_a:h(a) \cdot a^{-1} =_R 1$. Let $R$ be a commutative ring. The localization of $R$ away from a multiplicative submonoid $S$ with commutative monoid homomorphism $m:S \to R$ is the initial commutative ring $R[S^{-1}]$ with a commutative ring homomorphism $h:R \to R[S^{-1}]$, a function $(-)^{-1}:S \to R[S^{-1}]$, and identities $a:S \vdash \lambda_S(a):h(m(a)) \cdot a^{-1} =_R 1$. Let $R$ be a commutative ring. The field ring of fractions $R[\mathrm{Reg}(R)^{-1}]$ is the localization of $R$ away from the monoid of regular elements $\mathrm{Reg}(R)$. The rational numbers is the field ring of fractions for the integers $$\mathbb{Q} \coloneqq \mathbb{Z}[\mathrm{Reg}(\mathbb{Z})^{-1}]$$ ## References * Frank Quinn, *Proof Projects for Teachers* ([pdf](https://personal.math.vt.edu/fquinn/education/pfs4teachers0.pdf)) * Henri Lombardi, Claude Quitté (2010): *Commutative algebra: Constructive methods (Finite projective modules)* Translated by Tania K. Roblo, Springer (2015) ([doi:10.1007/978-94-017-9944-7](https://link.springer.com/book/10.1007/978-94-017-9944-7), [pdf](http://hlombardi.free.fr/CACM.pdf)) category: redirected to nlab