Homotopy Type Theory integers > history (Rev #20, changes)

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

Definition

~~The integers $\mathbb{Z}$ are the initial commutative ring structure on the natural numbers $\mathbb{N}$ .~~

Commutative ring structure

A The ~~commutative~~ integers ~~ring~~ ~~structure~~ on $ℕ ℤ$ ~~\mathbb{N}~~ \mathbb{Z} ~~consists~~ are of the an initial ~~element~~ commutative ring structure on the natural numbers $1 : ℕ$ ~~1:\mathbb{N}~~ \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$~~

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{linv}_+:\prod_{x:\mathbb{N}} \mathrm{isEquiv}(\lambda y:\mathbb{N}.x + y)$~~

{rinv assoc}_{+} : \prod_{x : ℕ} isEquiv \prod_{y : ℕ} \prod_{z : ℕ} x + (λ y : ℕ . y + z) =_{ℕ} (x + y) + z

~~\mathrm{rinv}_+:\prod_{x:\mathbb{N}}~~ \mathrm{assoc}_+:\prod_{x:\mathbb{N}} ~~\mathrm{isEquiv}(\lambda~~ \prod_{y:\mathbb{N}} ~~y:\mathbb{N}.y~~ \prod_{z:\mathbb{N}} x + x) (y + z) =_\mathbb{N} (x + y) + z

{ldist linv}_{\cdot, + +} : \prod_{x : ℕ} \prod_{y : ℕ} isEquiv \prod_{z : ℕ} x \cdot (λ y + : z ℕ) . =_{ℕ} x \cdot y + x y \cdot) z

~~\mathrm{ldist}_{\cdot,~~ \mathrm{linv}_+:\prod_{x:\mathbb{N}} ~~+}:\prod_{x:\mathbb{N}}~~ \mathrm{isEquiv}(\lambda ~~\prod_{y:\mathbb{N}}~~ y:\mathbb{N}.x ~~\prod_{z:\mathbb{N}}~~ x ~~\cdot~~ (y + z) y) ~~=_\mathbb{N}~~ x ~~\cdot~~ y + x ~~\cdot~~ z

{rdist rinv}_{\cdot, + +} : \prod_{x : ℕ} \prod_{y : ℕ} isEquiv \prod_{z : ℕ} (λ y + : z ℕ) . \cdot x =_{ℕ} y \cdot x + z \cdot x)

~~\mathrm{rdist}_{\cdot,~~ \mathrm{rinv}_+:\prod_{x:\mathbb{N}} ~~+}:\prod_{x:\mathbb{N}}~~ \mathrm{isEquiv}(\lambda ~~\prod_{y:\mathbb{N}}~~ y:\mathbb{N}.y ~~\prod_{z:\mathbb{N}}~~ (y + z) x) ~~\cdot~~ x ~~=_\mathbb{N}~~ y ~~\cdot~~ x + z ~~\cdot~~ x

{lunit ldist}_{\cdot, 1 +} : \prod_{x : ℕ} 1 \prod_{y : ℕ} \cdot \prod_{z : ℕ} x \cdot (y + z) =_{ℕ} x \cdot y + x \cdot z

~~\mathrm{lunit}_{\cdot,~~ \mathrm{ldist}_{\cdot, ~~1}:\prod_{x:\mathbb{N}}~~ +}:\prod_{x:\mathbb{N}} 1 \prod_{y:\mathbb{N}} ~~\cdot~~ \prod_{z:\mathbb{N}} x \cdot (y + z) =_\mathbb{N} x \cdot y + x \cdot z

{runit rdist}_{\cdot, 1 +} : \prod_{x : ℕ} x \prod_{y : ℕ} \prod_{z : ℕ} (y + z) \cdot 1 x =_{ℕ} y \cdot x + z \cdot x

~~\mathrm{runit}_{\cdot,~~ \mathrm{rdist}_{\cdot, ~~1}:\prod_{x:\mathbb{N}}~~ +}:\prod_{x:\mathbb{N}} x \prod_{y:\mathbb{N}} \prod_{z:\mathbb{N}} (y + z) \cdot 1 x =_\mathbb{N} y \cdot x + z \cdot x

{comm lunit}_{\cdot \cdot, 1} : \prod_{x : ℕ} x 1 \cdot y x =_{ℕ} y \cdot x

~~\mathrm{comm}_{\cdot}:\prod_{x:\mathbb{N}}~~ \mathrm{lunit}_{\cdot, x 1}:\prod_{x:\mathbb{N}} 1 \cdot y x =_\mathbb{N} y ~~\cdot~~ x

\mathrm{runit}_{\cdot, 1}:\prod_{x:\mathbb{N}} x \cdot 1 =_\mathbb{N} x

~~The type of all commutative ring structures on $\mathbb{N}$ is given by~~

\mathrm{comm}_{\cdot}:\prod_{x:\mathbb{N}} x \cdot y =_\mathbb{N} y \cdot x

$\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}$

The type of all commutative ring structures on $\mathbb{N}$ is given by

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

\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}

~~$\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)$~~

\prod_{x : ℕ} \prod_{y : ℕ} f (1_{A} x +_{A} y) =_{ℕ} 1_{B} f (x) +_{B} f (y)

~~f(1_A)~~ \prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} f(x +_A y) =_\mathbb{N} ~~1_B~~ 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)

~~The type of commutative ring homomorphisms between commutative ring structures $A:\mathrm{CRingStr}(\mathbb{N})$ and $B:\mathrm{CRingStr}(\mathbb{N})$ is given by~~

f(1_A) =_\mathbb{N} 1_B

$\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) =_S 1_B\right) \end{array}$

The type of commutative ring homomorphisms between commutative ring structures $A:\mathrm{CRingStr}(\mathbb{N})$ and $B:\mathrm{CRingStr}(\mathbb{N})$ is given by

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:

\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}

~~$\sum_{\mathbb{Z}:\mathrm{CRingStr}(\mathbb{N})} \prod_{R:\mathrm{CRingStr}(\mathbb{N})} \mathrm{isContr}(\mathrm{CRingHom}(\mathbb{N})(\mathbb{Z}, R))$~~

\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.