[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \tableofcontents \section{Apartness types} An apartness type is a type $T$ with a proposition-valued type family $\#$ and * a dependent term $a:T \vdash \mathrm{irr}(a):(a \# a) \to \mathbb{0}$ * a dependent term $a:T, b:T \vdash \mathrm{sym}(a, b):(a \# b) \to (b \# a)$ * a dependent term $a:T, b:T, c:T \vdash \mathrm{com}(a, b, c):(a \# c) \to ((a \# b) \vee (b \# c))$ * a dependent term $a:T, b:T \vdash \mathrm{tight}(a, b):\mathrm{isEquiv}(\mathrm{idtonotapart}(a, b))$ where $a:T, b:T \vdash \mathrm{idtonotapart}(a, b):(a =_T b) \to ((a \# b) \to \mathbb{0})$ is inductively defined by $$\beta(a):\mathrm{idtonotapart}(a, a) =_{(a \# a) \to \mathbb{0}} \mathrm{irr}(a)$$ \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{Prefield 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 prefield ring is a commutative ring $R$ such that every regular element is invertible: $$\prod_{a:A} \mathrm{isRegular}(a) \simeq \mathrm{isInvertible}(a)$$ \section{Localizations and 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 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 ring of fractions for the integers $$\mathbb{Q} \coloneqq \mathbb{Z}[\mathrm{Reg}(\mathbb{Z})^{-1}]$$ \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. ## 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