Homotopy Type Theory integers > history (changes)

Showing changes from revision #20 to #21: Added | ~~Removed~~ | ~~Chan~~ged

~~Definition~~
~~Commutative ring structure~~
~~The integers $\mathbb{Z}$ are the initial commutative ring structure on the natural numbers $\mathbb{N}$ .~~
A commutative ring structure on $\mathbb{N}$ consists of an element $1:\mathbb{N}$ , functions $(-)+(-):\mathbb{N} \times \mathbb{N} \to \mathbb{N}$ and $(-)\cdot(-):\mathbb{N} \times \mathbb{N} \to \mathbb{N}$ , and dependent products
~~$\mathrm{assoc}_+:\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} \prod_{z:\mathbb{N}} x + (y + z) =_\mathbb{N} (x + y) + z$~~
~~$\mathrm{linv}_+:\prod_{x:\mathbb{N}} \mathrm{isEquiv}(\lambda y:\mathbb{N}.x + y)$~~
~~$\mathrm{rinv}_+:\prod_{x:\mathbb{N}} \mathrm{isEquiv}(\lambda y:\mathbb{N}.y + x)$~~
~~$\mathrm{ldist}_{\cdot, +}:\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} \prod_{z:\mathbb{N}} x \cdot (y + z) =_\mathbb{N} x \cdot y + x \cdot z$~~
~~$\mathrm{rdist}_{\cdot, +}:\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} \prod_{z:\mathbb{N}} (y + z) \cdot x =_\mathbb{N} y \cdot x + z \cdot x$~~
~~$\mathrm{lunit}_{\cdot, 1}:\prod_{x:\mathbb{N}} 1 \cdot x =_\mathbb{N} x$~~
~~$\mathrm{runit}_{\cdot, 1}:\prod_{x:\mathbb{N}} x \cdot 1 =_\mathbb{N} x$~~
~~$\mathrm{comm}_{\cdot}:\prod_{x:\mathbb{N}} x \cdot y =_\mathbb{N} y \cdot x$~~
~~The type of all commutative ring structures on $\mathbb{N}$ is given by~~
$\mathrm{CRingStr}(\mathbb{N}) \coloneqq \begin{array}{c} \sum_{1:\mathbb{N}} \sum_{+:\mathbb{N} \times \mathbb{N} \to \mathbb{N}} \sum_{\cdot:\mathbb{N} \times \mathbb{N} \to \mathbb{N}} \left(\prod_{x:\mathbb{N}} \prod_{y:v} \prod_{z:\mathbb{N}} x + (y + z) =_\mathbb{N} (x + y) + z\right) \\ \times \left(\prod_{x:\mathbb{N}} \mathrm{isEquiv}(\lambda y:\mathbb{N}.x + y)\right) \times \left(\prod_{x:\mathbb{N}} \mathrm{isEquiv}(\lambda y:\mathbb{N}.y + x)\right) \\ \times \left(\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} \prod_{z:\mathbb{N}} x \cdot (y + z) =_\mathbb{N} x \cdot y + x \cdot z\right) \times \left(\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} \prod_{z:\mathbb{N}} (y + z) \cdot x =_\mathbb{N} y \cdot x + z \cdot x\right) \\ \times \left(\prod_{x:\mathbb{N}} 1 \cdot x =_\mathbb{N} x\right) \times \left(\prod_{x:R} x \cdot 1 =_\mathbb{N} x\right) \times \left(\prod_{x:R} x \cdot y =_\mathbb{N} y \cdot x\right) \end{array}$
A commutative ring homomorphism between two commutative ring structures $A:\mathrm{CRingStr}(\mathbb{N})$ and $B:\mathrm{CRingStr}(\mathbb{N})$ consists of a function $f:\mathbb{N} \to \mathbb{N}$ and dependent products
~~$\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} f(x +_A y) =_\mathbb{N} f(x) +_B f(y)$~~
~~$\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} f(x \cdot_A y) =_\mathbb{N} f(x) \cdot_B f(y)$~~
~~$f(1_A) =_\mathbb{N} 1_B$~~
~~The type of commutative ring homomorphisms between commutative ring structures $A:\mathrm{CRingStr}(\mathbb{N})$ and $B:\mathrm{CRingStr}(\mathbb{N})$ is given by~~
$\mathrm{CRingHom}(\mathbb{N})(A, B) \coloneqq \begin{array}{c} \sum_{f:\mathbb{N} \to \mathbb{N}} \left(\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} f(x +_A y) =_\mathbb{N} f(x) +_B f(y)\right) \\ \times \left(\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} f(x \cdot_A y) =_\mathbb{N} f(x) \cdot_B f(y)\right) \times \left(f(1_A) =_\mathbb{N} 1_B\right) \end{array}$
The initial commutative ring structure on $\mathbb{N}$ is a commutative ring structure $\mathbb{Z}:\mathrm{CRingStr}(\mathbb{N})$ such that for all commutative ring structures $R:\mathrm{CRingStr}(\mathbb{N})$ the type of commutative ring homomorphisms $\mathrm{CRingHom}(\mathbb{N})(\mathbb{Z}, R)$ is contractible:
~~$\sum_{\mathbb{Z}:\mathrm{CRingStr}(\mathbb{N})} \prod_{R:\mathrm{CRingStr}(\mathbb{N})} \mathrm{isContr}(\mathrm{CRingHom}(\mathbb{N})(\mathbb{Z}, R))$~~
~~Euclidean domain structure~~
~~In fact, the integers are the initial ordered integral domain structure on $\mathbb{N}$~~

~~category: redirected to nlab~~

Last revised on March 15, 2024 at 17:04:27. See the history of this page for a list of all contributions to it.