From d00edf833e6d126ba5bcddf05f7b46f8a1ba554b Mon Sep 17 00:00:00 2001 From: Kevin Orr Date: Mon, 18 Dec 2023 20:16:22 -0500 Subject: [PATCH 1/2] defn: two point circle --- src/Homotopy/Space/Circle/TwoPoint.lagda.md | 163 ++++++++++++++++++++ src/index.lagda.md | 1 + 2 files changed, 164 insertions(+) create mode 100644 src/Homotopy/Space/Circle/TwoPoint.lagda.md diff --git a/src/Homotopy/Space/Circle/TwoPoint.lagda.md b/src/Homotopy/Space/Circle/TwoPoint.lagda.md new file mode 100644 index 000000000..923e0c873 --- /dev/null +++ b/src/Homotopy/Space/Circle/TwoPoint.lagda.md @@ -0,0 +1,163 @@ + + +```agda +module Homotopy.Space.Circle.TwoPoint where +``` + +# Spaces: The circle with two point constructors + +We can add additional points onto the [[circle]], and still end up with +a space that is homotopy-equivalent to `S¹`{.Agda}. + +~~~{.quiver} +\begin{tikzpicture} +\node[draw,circle,label=below:{$\rm{south}$},fill,outer sep=0.1cm, inner sep=0pt, minimum size=0.1cm] (south) at (0, -1) {}; +\node[draw,circle,label=above:{$\rm{north}$},fill,outer sep=0.1cm, inner sep=0pt, minimum size=0.1cm] (north) at (0, 1) {}; +\draw[->, bend right=85, distance=1.2cm] (south) to node[right] {$\rm{east}\ i$} (north); +\draw[->, bend right=85, distance=1.2cm] (north) to node[left] {$\rm{west}\ i$} (south); +\end{tikzpicture} +~~~ + +```agda +data S¹₂ : Type where + south : S¹₂ + north : S¹₂ + east : south ≡ north + west : north ≡ south +``` + +The path which corresponds to `loop`{.Agda} is simply the composition of +`east`{.Agda} and `west`{.Agda}. + +```agda +loop₂ : south ≡ south +loop₂ = east ∙ west +``` + +First we define a mapping from `S¹`{.Agda} to `S¹₂`{.Agda}. + +```agda +S¹→S¹₂ : S¹ → S¹₂ +S¹→S¹₂ base = south +S¹→S¹₂ (loop i) = loop₂ i +``` + +The inverse mapping is less obvious. `south`{.Agda} should of course map +to `base`{.Agda}. + + + +```agda +S¹₂→S¹ : S¹₂ → S¹ +S¹₂→S¹ south = base +``` + +But what shall we map `north`{.Agda} (and by extension, `east`{.Agda} +and `west`{.Agda}) to? If the interval type were literally the unit +interval of the real numbers, $[0,1]$, then we could map `north`{.Agda} +to the point halfway along `loop`{.Agda}. However, the only two points +along the interval that we can name are `i0`{.Agda} and `i1`{.Agda}. +Thus, we need to map `north`{.Agda} to either `base`{.Agda}, `loop i0`, +or `loop i1`, since these are the only terms of type `S¹`{.Agda} that we +can name. However, all three of these terms are definitionally +`base`{.Agda}! So let's use that. + +```agda +S¹₂→S¹ north = base +``` + +The question now arrises how we map `east`{.Agda} and `west`{.Agda} onto +`S¹`{.Agda}. Recall that the composition `east ∙ west` should map to +`loop`{.Agda}. If we map `east`{.Agda} to `refl`{.Agda}, and +`west`{.Agda} to `loop`{.Agda}, then there will indeed be a path from +`ap S¹₂→S¹ (east ∙ west)` to `loop`{.Agda}. + +```agda +S¹₂→S¹ (east i) = base +S¹₂→S¹ (west i) = loop i + +loop₂→loop : ap S¹₂→S¹ loop₂ ≡ loop +loop₂→loop = + ap S¹₂→S¹ loop₂ ≡⟨⟩ + ap S¹₂→S¹ (east ∙ west) ≡⟨ ap-∙ S¹₂→S¹ east west ⟩ + ap S¹₂→S¹ east ∙ ap S¹₂→S¹ west ≡⟨⟩ + refl ∙ loop ≡⟨ ∙-idl _ ⟩ + loop ∎ +``` + +As an aside, we can use this proof, along with `refl≠loop`{.Agda}, to +show that `loop₂`{.Agda} is similarly distinct from `refl`{.Agda}. + +```agda +refl≠loop₂ : ¬ (refl ≡ loop₂) +refl≠loop₂ p = refl≠loop (ap (ap S¹₂→S¹) p ∙ loop₂→loop) +``` + +`loop₂→loop`{.Agda} is also enough to show that `S¹→S¹₂`{.Agda} and +`S¹₂→S¹`{.Agda} form an equivalence. + +```agda +S¹₂≃S¹ : S¹₂ ≃ S¹ +S¹₂≃S¹ = Iso→Equiv $ + S¹₂→S¹ , iso S¹→S¹₂ + (λ where + base → refl + (loop i) j → loop₂→loop j i) + (λ where + south → refl + north → east + (east i) j → east (i ∧ j) + (west i) j → ∙-filler' east west (~ j) i) +``` + +Now we can borrow theorems about `S¹`{.Agda} and transport them to +theorems about `S¹₂`{.Agda}. The loop space at `south`{.Agda} is +equivalent to the integers. + +```agda +module S¹₂Path {ℤ} (univ : Integers ℤ) where + open S¹Path univ + ΩS¹₂≃integers : (south ≡ south) ≃ ℤ + ΩS¹₂≃integers = line→equiv (λ i → H i) ∙e ΩS¹≃integers + where + H : (south ≡ south) ≡ (base ≡ base) + H = apd (λ i x → x ≡ x) (path→ua-pathp S¹₂≃S¹ refl) +``` + +The loop space at `north`{.Agda} is similarly equivalent to the +integers. + +```agda + ΩS¹₂≃integers' : (north ≡ north) ≃ ℤ + ΩS¹₂≃integers' = line→equiv (λ i → H i) ∙e ΩS¹≃integers + where + H : (north ≡ north) ≡ (base ≡ base) + H = apd (λ i x → x ≡ x) (path→ua-pathp S¹₂≃S¹ refl) + +open S¹₂Path Int-integers public +``` + + diff --git a/src/index.lagda.md b/src/index.lagda.md index 79192d81c..c8ebc8a34 100644 --- a/src/index.lagda.md +++ b/src/index.lagda.md @@ -1051,6 +1051,7 @@ open import Homotopy.Connectedness -- Connected types open import Homotopy.Space.Suspension -- Suspensions open import Homotopy.Space.Circle -- The circle +open import Homotopy.Space.Circle.TwoPoint -- The circle with two named points open import Homotopy.Space.Sphere -- The n-spheres open import Homotopy.Space.Sinfty -- The ∞-sphere open import Homotopy.Space.Torus -- The torus From 8c5bcbcb09172022b6d5c67d8373cf1d1692a39c Mon Sep 17 00:00:00 2001 From: Kevin Orr Date: Tue, 19 Dec 2023 11:20:42 -0600 Subject: [PATCH 2/2] Update src/Homotopy/Space/Circle/TwoPoint.lagda.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Naïm Favier --- src/Homotopy/Space/Circle/TwoPoint.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Homotopy/Space/Circle/TwoPoint.lagda.md b/src/Homotopy/Space/Circle/TwoPoint.lagda.md index 923e0c873..4ed5d3e0c 100644 --- a/src/Homotopy/Space/Circle/TwoPoint.lagda.md +++ b/src/Homotopy/Space/Circle/TwoPoint.lagda.md @@ -80,7 +80,7 @@ can name. However, all three of these terms are definitionally S¹₂→S¹ north = base ``` -The question now arrises how we map `east`{.Agda} and `west`{.Agda} onto +The question now arises how we map `east`{.Agda} and `west`{.Agda} onto `S¹`{.Agda}. Recall that the composition `east ∙ west` should map to `loop`{.Agda}. If we map `east`{.Agda} to `refl`{.Agda}, and `west`{.Agda} to `loop`{.Agda}, then there will indeed be a path from