module Homotopy.Space.Circle where
Spaces: The circle🔗
The first example of nontrivial space one typically encounters when studying synthetic homotopy theory is the circle: it is, in a sense, the perfect space to start with, having exactly one nontrivial path space, which is a free group, and the simplest nontrivial free group at that: the integers.
data S¹ : Type where base : S¹ loop : base ≡ base S¹∙ : Type∙ lzero S¹∙ = S¹ , base
Diagrammatically, we can picture the circle as being the generated by the following diagram:
In type theory with K, the circle is exactly the same type as ⊤. However, with univalence, it can be shown
that the circle has at least two different paths:
möbius : S¹ → Type möbius base = Bool möbius (loop i) = ua (not , not-is-equiv) i
When pattern matching on the circle, we are asked to provide a
basepoint b and a path l : b ≡ b, as can be
seen in the definition above. To make it clearer, we can also define a
recursion principle:
S¹-rec : ∀ {ℓ} {A : Type ℓ} (b : A) (l : b ≡ b) → S¹ → A S¹-rec b l base = b S¹-rec b l (loop i) = l i
S¹-elim : ∀ {ℓ} {A : S¹ → Type ℓ} (b : A base) (l : PathP (λ i → A (loop i)) b b) → ∀ s → A s S¹-elim b l base = b S¹-elim b l (loop i) = l i
We call the map möbius a double cover
of the circle, since the fibre at each point is a discrete space with
two elements. It has an action by the fundamental group of the circle,
which has the effect of negating the “parity” of the path. In fact, we
can use möbius to show that loop is not refl:
parity : base ≡ base → Bool parity l = subst möbius l true _ : parity refl ≡ true _ = refl _ : parity loop ≡ false _ = refl refl≠loop : ¬ refl ≡ loop refl≠loop path = true≠false (ap parity path)
The circle is also useful as a source of counterexamples: we can
prove that there is an inhabitant of (x : S¹) → x ≡ x
which is not constantly refl.
always-loop : (x : S¹) → x ≡ x always-loop = S¹-elim loop (double-connection loop loop)
Fundamental group🔗
We now calculate the loop space of the circle, relative to an arbitrary implementation of the integers: any type that satisfies their type-theoretic universal property. We call this a HoTT take: the integers are the homotopy-initial space with a point and an automorphism. What we’d like to do is prove that the loop space of the circle is also an implementation of the integers, but it’s non-trivial to show that it is a set directly.
module S¹Path {ℤ} (univ : Integers ℤ) where open Integers univ
We start by defining a type family that we’ll later find out is the universal cover of the circle. For now, it serves a humbler purpose: A value in gives a concrete representation to a path in the circle. We want to show that so we set the fibre over the basepoint to be the integers:
Cover : S¹ → Type Cover base = ℤ Cover (loop i) = ua rotate i
We can define a function from paths to integers — or, more precisely, a function from to Note that the path induces a path and since is equipped with a choice of point, then is
encode : ∀ x → base ≡ x → Cover x encode x p = subst Cover p point
Let us now define the inverse function: one from integer to paths. By the mapping-out property of the integers, we must give an equivalence from to itself. Since is a group, any element induces such an equivalence, by postcomposition We take to be the generating non-trivial path,
loopⁿ : ℤ → base ≡ base loopⁿ n = map-out refl (∙-post-equiv loop) n loopⁿ⁺¹ : (n : ℤ) → loopⁿ (rotate .fst n) ≡ loopⁿ n ∙ loop loopⁿ⁺¹ n = map-out-rotate _ _ _
To prove that the map is an equivalence, we shall need to extend it to a map defined fibrewise on the cover. We shall do so cubically, i.e., by directly pattern-matching on the argument
When we’re at the base point, we already know what we want to do: we have a function already, so we can use that.
decode : ∀ x → Cover x → base ≡ x decode base = loopⁿ
For the other case, we must provide a path laying over the loop, which we can picture as the boundary of a square. Namely,
While it doesn’t look like this square commutes, note that
is an inhabitant of ua rotate i, so
that its values on the endpoints of i are off by one. If we unglue
we get an integer whose incarnation at i = i0 is
(adjusting for the rotation offset) while at i = i1 it is just
We can provide such a square as sketching out an open cube whose missing face has the boundary above. Here’s such a cube: the missing face has a dotted boundary.
decode (loop i) n j = hcomp (∂ i ∨ ∂ j) λ where k (k = i0) → loopⁿ (unglue (∂ i) n) j k (i = i0) → ∙→square (loopⁿ⁺¹ n) (~ k) j k (i = i1) → loopⁿ n j k (j = i0) → base k (j = i1) → loop (i ∨ ~ k)
We understand this as a particularly annoying commutative diagram. For example, the left face expresses the equation The proof is now straightforward to wrap up:
encode-decode : ∀ x (p : base ≡ x) → decode x (encode x p) ≡ p encode-decode _ = J (λ x p → decode x (encode x p) ≡ p) $ ap loopⁿ (transport-refl point) ∙ map-out-point _ _ encode-loopⁿ : (n : ℤ) → encode base (loopⁿ n) ≡ n encode-loopⁿ n = p ∙ ℤ-η n where p : encode base (loopⁿ n) ≡ map-out point rotate n p = map-out-unique (encode base ∘ loopⁿ) (ap (encode base) (map-out-point _ _) ∙ transport-refl point) (λ x → ap (encode base) {y = loopⁿ x ∙ loop} (map-out-rotate _ _ _) ·· subst-∙ Cover (loopⁿ x) loop point ·· uaβ rotate (subst Cover (loopⁿ x) point)) n ΩS¹≃integers : (base ≡ base) ≃ ℤ ΩS¹≃integers = Iso→Equiv $ encode base , iso loopⁿ encode-loopⁿ (encode-decode base) open S¹Path Int-integers public
It immediately follows from this that the circle is a groupoid, since its loop space is a set.
opaque S¹-is-groupoid : is-groupoid S¹ S¹-is-groupoid = S¹-elim (S¹-elim (Equiv→is-hlevel 2 ΩS¹≃integers (hlevel 2)) prop!) prop!
By induction, we can show that this equivalence respects group composition (that is, so that we have a proper isomorphism of groups.
loopⁿ-+ : (a b : Int) → loopⁿ (a +ℤ b) ≡ loopⁿ a ∙ loopⁿ b loopⁿ-+ a = Integers.induction Int-integers (ap loopⁿ (+ℤ-zeror a) ∙ sym (∙-idr _)) λ b → loopⁿ (a +ℤ b) ≡ loopⁿ a ∙ loopⁿ b ≃⟨ ap (_∙ loop) , equiv→cancellable (∙-post-equiv loop .snd) ⟩≃ loopⁿ (a +ℤ b) ∙ loop ≡ (loopⁿ a ∙ loopⁿ b) ∙ loop ≃⟨ ∙-post-equiv (sym (∙-assoc _ _ _)) ⟩≃ loopⁿ (a +ℤ b) ∙ loop ≡ loopⁿ a ∙ loopⁿ b ∙ loop ≃⟨ ∙-post-equiv (ap (loopⁿ a ∙_) (sym (loopⁿ⁺¹ b))) ⟩≃ loopⁿ (a +ℤ b) ∙ loop ≡ loopⁿ a ∙ loopⁿ (sucℤ b) ≃⟨ ∙-pre-equiv (loopⁿ⁺¹ (a +ℤ b)) ⟩≃ loopⁿ (sucℤ (a +ℤ b)) ≡ loopⁿ a ∙ loopⁿ (sucℤ b) ≃⟨ ∙-pre-equiv (ap loopⁿ (+ℤ-sucr a b)) ⟩≃ loopⁿ (a +ℤ sucℤ b) ≡ loopⁿ a ∙ loopⁿ (sucℤ b) ≃∎ π₁S¹≡ℤ : π₁Groupoid.π₁ S¹∙ S¹-is-groupoid ≡ ℤ π₁S¹≡ℤ = sym $ ∫-Path Groups-equational (total-hom (Equiv.from ΩS¹≃integers ∘ Lift.lower) (record { pres-⋆ = λ (lift a) (lift b) → loopⁿ-+ a b })) (∙-is-equiv (Lift-≃ .snd) ((ΩS¹≃integers e⁻¹) .snd))
Furthermore, since the loop space of the circle is a set, we automatically get that all of its higher homotopy groups are trivial.
Ωⁿ⁺²S¹-is-contr : ∀ n → is-contr ⌞ Ωⁿ (2 + n) S¹∙ ⌟ Ωⁿ⁺²S¹-is-contr zero = is-prop∙→is-contr (hlevel 1) refl Ωⁿ⁺²S¹-is-contr (suc n) = Path-is-hlevel 0 (Ωⁿ⁺²S¹-is-contr n) πₙ₊₂S¹≡0 : ∀ n → πₙ₊₁ (suc n) S¹∙ ≡ Zero-group {lzero} πₙ₊₂S¹≡0 n = ∫-Path Groups-equational (Zero-group-is-terminal _ .centre) (is-contr→≃ (is-contr→∥-∥₀-is-contr (Ωⁿ⁺²S¹-is-contr n)) (hlevel 0) .snd)