The multiplication operation on the circle
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Victor Blanchi.
Created on 2022-06-02.
Last modified on 2023-09-11.
module synthetic-homotopy-theory.multiplication-circle where
Imports
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-along-identifications open import foundation.universe-levels open import structured-types.pointed-homotopies open import structured-types.pointed-maps open import synthetic-homotopy-theory.circle
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
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
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)
Recent changes
- 2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).
- 2023-09-10. Fredrik Bakke. Rename
inv-con
andcon-inv
toleft/right-transpose-eq-concat
(#730). - 2023-07-19. Egbert Rijke. refactoring pointed maps (#682).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).