Homotopy Type Theory
integers > history (Rev #20)
< integer
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 : ℕ 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
assoc + : ∏ x : ℕ ∏ y : ℕ ∏ z : ℕ x + ( y + z ) = ℕ ( x + y ) + z \mathrm{assoc}_+:\prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} \prod_{z:\mathbb{N}} x + (y + z) =_\mathbb{N} (x + y) + z linv + : ∏ x : ℕ isEquiv ( λ y : ℕ . x + y ) \mathrm{linv}_+:\prod_{x:\mathbb{N}} \mathrm{isEquiv}(\lambda y:\mathbb{N}.x + y) rinv + : ∏ x : ℕ isEquiv ( λ y : ℕ . y + x ) \mathrm{rinv}_+:\prod_{x:\mathbb{N}} \mathrm{isEquiv}(\lambda y:\mathbb{N}.y + x) ldist ⋅ , + : ∏ x : ℕ ∏ y : ℕ ∏ z : ℕ x ⋅ ( y + z ) = ℕ x ⋅ y + x ⋅ z \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 rdist ⋅ , + : ∏ x : ℕ ∏ y : ℕ ∏ z : ℕ ( y + z ) ⋅ x = ℕ y ⋅ x + z ⋅ x \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 lunit ⋅ , 1 : ∏ x : ℕ 1 ⋅ x = ℕ x \mathrm{lunit}_{\cdot, 1}:\prod_{x:\mathbb{N}} 1 \cdot x =_\mathbb{N} x runit ⋅ , 1 : ∏ x : ℕ x ⋅ 1 = ℕ x \mathrm{runit}_{\cdot, 1}:\prod_{x:\mathbb{N}} x \cdot 1 =_\mathbb{N} x comm ⋅ : ∏ x : ℕ x ⋅ y = ℕ y ⋅ 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
CRingStr ( ℕ ) ≔ ∑ 1 : ℕ ∑ + : ℕ × ℕ → ℕ ∑ ⋅ : ℕ × ℕ → ℕ ( ∏ x : ℕ ∏ y : v ∏ z : ℕ x + ( y + z ) = ℕ ( x + y ) + z ) × ( ∏ x : ℕ isEquiv ( λ y : ℕ . x + y ) ) × ( ∏ x : ℕ isEquiv ( λ y : ℕ . y + x ) ) × ( ∏ x : ℕ ∏ y : ℕ ∏ z : ℕ x ⋅ ( y + z ) = ℕ x ⋅ y + x ⋅ z ) × ( ∏ x : ℕ ∏ y : ℕ ∏ z : ℕ ( y + z ) ⋅ x = ℕ y ⋅ x + z ⋅ x ) × ( ∏ x : ℕ 1 ⋅ x = ℕ x ) × ( ∏ x : R x ⋅ 1 = ℕ x ) × ( ∏ x : R x ⋅ y = ℕ y ⋅ 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}
A commutative ring homomorphism between two commutative ring structures A : CRingStr ( ℕ ) A:\mathrm{CRingStr}(\mathbb{N}) and B : CRingStr ( ℕ ) B:\mathrm{CRingStr}(\mathbb{N}) consists of a function f : ℕ → ℕ f:\mathbb{N} \to \mathbb{N} and dependent products
∏ x : ℕ ∏ y : ℕ f ( x + A y ) = ℕ f ( x ) + B f ( y ) \prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} f(x +_A y) =_\mathbb{N} f(x) +_B f(y) ∏ x : ℕ ∏ y : ℕ f ( x ⋅ A y ) = ℕ 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 ) = ℕ 1 B f(1_A) =_\mathbb{N} 1_B
The type of commutative ring homomorphisms between commutative ring structures A : CRingStr ( ℕ ) A:\mathrm{CRingStr}(\mathbb{N}) and B : CRingStr ( ℕ ) B:\mathrm{CRingStr}(\mathbb{N}) is given by
CRingHom ( ℕ ) ( A , B ) ≔ ∑ f : ℕ → ℕ ( ∏ x : ℕ ∏ y : ℕ f ( x + A y ) = ℕ f ( x ) + B f ( y ) ) × ( ∏ x : ℕ ∏ y : ℕ f ( x ⋅ A y ) = ℕ f ( x ) ⋅ B f ( y ) ) × ( f ( 1 A ) = ℕ 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) =_\mathbb{N} 1_B\right)
\end{array}
The initial commutative ring structure on ℕ \mathbb{N} is a commutative ring structure ℤ : CRingStr ( ℕ ) \mathbb{Z}:\mathrm{CRingStr}(\mathbb{N}) such that for all commutative ring structures R : CRingStr ( ℕ ) R:\mathrm{CRingStr}(\mathbb{N}) the type of commutative ring homomorphisms CRingHom ( ℕ ) ( ℤ , R ) \mathrm{CRingHom}(\mathbb{N})(\mathbb{Z}, R) is contractible:
∑ ℤ : CRingStr ( ℕ ) ∏ R : CRingStr ( ℕ ) isContr ( CRingHom ( ℕ ) ( ℤ , 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}
Revision on November 22, 2023 at 14:48:41 by
.? .
See the history of this page for a list of all contributions to it.