Homotopy Type Theory integers > history (Rev #20)

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

Revision on November 22, 2023 at 14:48:41 by .?. See the history of this page for a list of all contributions to it.