/
multiplication-circle.lagda.md
111 lines (90 loc) · 3.24 KB
/
multiplication-circle.lagda.md
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
# The multiplication operation on the circle
```agda
module synthetic-homotopy-theory.multiplication-circle where
```
<details><summary>Imports</summary>
```agda
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.transport
open import foundation.universe-levels
open import structured-types.pointed-homotopies
open import structured-types.pointed-maps
open import synthetic-homotopy-theory.circle
```
</details>
## Idea
Classically, the circle can be viewed as the subset of the complex numbers of
absolute value 1. The absolute value of a product of complex numbers is the
product of their absolute values. This implies that when we multiply two complex
numbers on the unit circle, the result is a complex number on the unit circle.
This multiplicative structure carries over to the homotopy type of the circle.
## Definition
### Homotopy `id ~ id` of degree one
```agda
htpy-id-id-Π-𝕊¹ :
Π-𝕊¹
( eq-value id id)
( loop-𝕊¹)
( map-compute-dependent-identification-eq-value-id-id
( loop-𝕊¹)
( loop-𝕊¹)
( loop-𝕊¹)
( refl))
htpy-id-id-Π-𝕊¹ =
apply-dependent-universal-property-𝕊¹
( eq-value id id)
( loop-𝕊¹)
( map-compute-dependent-identification-eq-value-id-id
( loop-𝕊¹)
( loop-𝕊¹)
( loop-𝕊¹)
( refl))
htpy-id-id-𝕊¹ : (x : 𝕊¹) → Id x x
htpy-id-id-𝕊¹ = pr1 htpy-id-id-Π-𝕊¹
htpy-id-id-base-𝕊¹ : Id (htpy-id-id-𝕊¹ base-𝕊¹) loop-𝕊¹
htpy-id-id-base-𝕊¹ = pr1 (pr2 htpy-id-id-Π-𝕊¹)
```
### Multiplication on the circle
```agda
Mul-Π-𝕊¹ : 𝕊¹ → UU lzero
Mul-Π-𝕊¹ x = 𝕊¹-Pointed-Type →∗ (pair 𝕊¹ x)
dependent-identification-Mul-Π-𝕊¹ :
{x : 𝕊¹} (p : Id base-𝕊¹ x) (q : Mul-Π-𝕊¹ base-𝕊¹) (r : Mul-Π-𝕊¹ x) →
(H : pr1 q ~ pr1 r) → Id (pr2 q ∙ p) (H base-𝕊¹ ∙ pr2 r) →
Id (tr Mul-Π-𝕊¹ p q) r
dependent-identification-Mul-Π-𝕊¹ {x} refl q r H u =
eq-htpy-pointed-map
( q)
( r)
( ( H) ,
(right-transpose-eq-concat
( H base-𝕊¹)
( pr2 r)
( pr2 q)
( inv (inv right-unit ∙ u))))
eq-id-id-𝕊¹-Pointed-Type :
Id (tr Mul-Π-𝕊¹ loop-𝕊¹ id-pointed-map) id-pointed-map
eq-id-id-𝕊¹-Pointed-Type =
dependent-identification-Mul-Π-𝕊¹ loop-𝕊¹
( id-pointed-map)
( id-pointed-map)
( htpy-id-id-𝕊¹)
( inv htpy-id-id-base-𝕊¹ ∙ inv right-unit)
mul-Π-𝕊¹ : Π-𝕊¹ (Mul-Π-𝕊¹) (id-pointed-map) (eq-id-id-𝕊¹-Pointed-Type)
mul-Π-𝕊¹ =
apply-dependent-universal-property-𝕊¹
( Mul-Π-𝕊¹)
( id-pointed-map)
( eq-id-id-𝕊¹-Pointed-Type)
mul-𝕊¹ : 𝕊¹ → 𝕊¹ → 𝕊¹
mul-𝕊¹ x = pr1 (pr1 mul-Π-𝕊¹ x)
left-unit-law-mul-𝕊¹ : (x : 𝕊¹) → Id (mul-𝕊¹ base-𝕊¹ x) x
left-unit-law-mul-𝕊¹ = htpy-eq (ap pr1 (pr1 (pr2 mul-Π-𝕊¹)))
right-unit-law-mul-𝕊¹ : (x : 𝕊¹) → Id (mul-𝕊¹ x base-𝕊¹) x
right-unit-law-mul-𝕊¹ x = pr2 (pr1 mul-Π-𝕊¹ x)
```