module Homotopy.Space.Sphere where
The -1 and 0 spheresš
In classical topology, the topological space is typically defined as the subspace of consisting of all points at unit distance from the origin. We see from this definition that the is the discrete two point space and that the sphere is the empty subspace We will recycle existing types and define:
Sā»Ā¹ : Type Sā»Ā¹ = ā„ Sā° : Type Sā° = Bool
We note that Sā°
may be identified with
Susp Sā»Ā¹
. Since the pattern matching checker can prove that
merid x i
is impossible when x : ā„
, the case
for this constructor does not need to be written, this makes the proof
look rather tautologous.
open is-iso SuspSā»Ā¹āSā° : Susp Sā»Ā¹ ā Sā° SuspSā»Ā¹āSā° = SuspSā»Ā¹āSā° , is-isoāis-equiv iso-pf where SuspSā»Ā¹āSā° : Susp Sā»Ā¹ ā Sā° SuspSā»Ā¹āSā° north = true SuspSā»Ā¹āSā° south = false Sā°āSuspSā»Ā¹ : Sā° ā Susp Sā»Ā¹ Sā°āSuspSā»Ā¹ true = north Sā°āSuspSā»Ā¹ false = south iso-pf : is-iso SuspSā»Ā¹āSā° iso-pf .from = Sā°āSuspSā»Ā¹ iso-pf .rinv false = refl iso-pf .rinv true = refl iso-pf .linv north = refl iso-pf .linv south = refl
n-Spheresš
The spheres of higher dimension can be defined inductively: that is, suspending the constructs the
The spheres are essentially indexed by the natural numbers, except that we want to start at instead of To remind ourselves of this, we name our spheres with a superscript
Sāæā»Ā¹ : Nat ā Type Sāæā»Ā¹ zero = Sā»Ā¹ Sāæā»Ā¹ (suc n) = Susp (Sāæā»Ā¹ n)
By convention, the (for is considered as a pointed type with base point the north pole
Sāæ : Nat ā Typeā lzero Sāæ n = Sāæā»Ā¹ (suc n) , north
A slightly less trivial example of definitions lining up is the
verification that Sāæā»Ā¹ 2
is equivalent to our previous
definition of S¹
:
SuspSā°āS¹ : Sāæā»Ā¹ 2 ā S¹ SuspSā°āS¹ = SuspSā°āS¹ , is-isoāis-equiv iso-pf where
In Sāæā»Ā¹ 2
, we have two point constructors joined by two
paths, while in S¹
we have a single point constructor and a
loop. Geometrically, we can picture morphing Sāæā»Ā¹ 2
into
S¹
by squashing one of the meridians down to a point, thus
bringing N
and S
together. This intuition
leads to a definition:
SuspSā°āS¹ : Sāæā»Ā¹ 2 ā S¹ SuspSā°āS¹ north = base SuspSā°āS¹ south = base SuspSā°āS¹ (merid north i) = base SuspSā°āS¹ (merid south i) = loop i
In the other direction, we send base
to N
,
and then need to send loop
to some path N ā” N
.
Since this map should define an equivalence, we make it such that loop
wraps around the space Sāæ 2
by way of traversing both
meridians.
S¹āSuspSā° : S¹ ā Sāæā»Ā¹ 2 S¹āSuspSā° base = north S¹āSuspSā° (loop i) = (merid south ā sym (merid north)) i
We then verify that these maps are inverse equivalences. One of the
steps involves a slightly tricky hcomp
, although this can
be avoided by working with transports instead of dependent paths, and
then by using lemmas on transport in pathspaces.
iso-pf : is-iso SuspSā°āS¹ iso-pf .from = S¹āSuspSā° iso-pf .rinv base = refl iso-pf .rinv (loop i) = ap (Ī» p ā p i) (ap SuspSā°āS¹ (merid south ā sym (merid north)) ā”⨠ap-ā SuspSā°āS¹ (merid south) (sym (merid north))ā©ā” loop ā refl ā”⨠ā-idr _ ā©ā” loop ā) iso-pf .linv north = refl iso-pf .linv south = merid north iso-pf .linv (merid north i) j = merid north (i ā§ j) iso-pf .linv (merid south i) j = hcomp (ā i ⨠ā j) Ī» where k (k = i0) ā merid south i k (i = i0) ā north k (i = i1) ā merid north (j ⨠~ k) k (j = i0) ā ā-filler (merid south) (sym (merid north)) k i k (j = i1) ā merid south i