Quest 1 - Loop Space of the Circle
Part 0 - Definition of the Loop Space
In this quest, we continue to formalise the problem statement.
The problem statement
The fundamental group of S¹
is ℤ
.
Intuitively,
the fundamental group of S¹
at base
consists of loops based as base
up to homotopy of paths.
In homotopy type theory,
we have a native description of loops based at base
:
it is the space base ≡ base
.
In general the loop space of a space A
at a point a
is defined as follows :
loopSpace : (A : Type) (a : A) → Type
loopSpace A a = a ≡ a
For now, we will treat the loop space of S¹
as the fundamental group.
Later we will understand why this is illegal in general
(the fundamental group is set truncated)
but legitimate in this special case
(the loop space of S¹
turns out to be a set anyway).
Exercise - loop_times
Clearly for each integer n : ℤ
we have a path
that is “loop
around n
times”.
Locate loop_times
in 1FundamentalGroup/Quest1.agda
(note how agda
treats underscores)
loop_times : ℤ → loopSpace S¹ base
loop n times = {!!}
Note
You can use underscores when you name a function.
agda
will put the inputs in the underscores in order.
Try casing on n
, you should see
loop_times : ℤ → loopSpace S¹ base
loop pos n times = {!!}
loop negsuc n times = {!!}
It says to map out of ℤ
it suffices to
map the non-negative integers (pos
)
and the negative integers (negsuc
).
The definition of ℤ
in agda
is
data ℤ : Type where
pos : ℕ → ℤ
negsuc : ℕ → ℤ
It says is ℤ
is two copies of ℕ
where the first
copy represents 0, 1, 2, ...
,
and the second represents -1, -2, ...
(negsuc n
is meant to mean - (n + 1)
).
This definition of ℤ
uses the naturals, so try
casing on n
again, you should see
loop_times : ℤ → Ω S¹ base
loop pos zero times = {!!}
loop pos (suc n) times = {!!}
loop negsuc n times = {!!}
It says to map out of ℕ
it suffices to map zero
and
map each successive integer suc n
inductively.
We can do the same with negsuc n
,
obtaining four cases.
loop_times : ℤ → Ω S¹ base
loop pos zero times = {!!}
loop pos (suc n) times = {!!}
loop negsuc zero times = {!!}
loop negsuc (suc n) times = {!!}
These four cases represent :
If you “loop 0 times” then you stay at
base
.If you “loop n + 1 times”, you “loop n times” then “loop once more”.
If you “loop -1 times”, you “loop once in reverse”
If you “loop -(n + 2) times”, you loop “loop -(n + 1) times” then “loop once more in reverse”
Individually
Try filling the first hole with what we get when we loop
0
(pos zero
) times.For looping
pos (suc n)
times we loopn
times and loop once more. For this we need composition of paths._∙_ : x ≡ y → y ≡ z → x ≡ z
Try typing
_∙_
or? ∙ ?
in the hole (input\.
) and refining. Checking the new holes you should see that now you need to give two loops.loop pos (suc n) times = {!!} ∙ {!!}
Try giving it “
loop n times
” concatenated withloop
.To “loop in reverse” we use
sym : x ≡ y → y ≡ x
Use this to define “loop -1 times”.
For the last case “concatenate loop -(n + 1) times with loop in reverse”.
Part 1 - Making a Path From ℤ
to Itself
In the previous part we have defined the map loop_times : ℤ → Ω S¹ base
.
Creating the inverse map is difficult without access to the entire circle.
Similarly to how we used doubleCover
to distinguish refl
(Refl
is now refl
which is more general) from loop
,
the idea is to replace Bool
with ℤ
,
allowing us to distinguish between all loops on S¹
.
In this quest we will construct one of the two comparison maps
across the whole circle, called windingNumber
.
The plan is :
Define a function
sucℤ : ℤ → ℤ
that increases every integer by oneProve that
sucℤ
is an isomorphism by constructing an inverse mappredℤ : ℤ → ℤ
.Turn the isomorphism
sucℤ
into a pathsucℤPath : ℤ ≡ ℤ
usingisoToPath
Define
helix : S¹ → Type
by mappingbase
toℤ
and a generic pointloop i
tosucℤPath i
.Use
helix
andendPt
to define the mapwindingNumberBase : base ≡ base → ℤ
. Intuitively it counts how many times a path loops aroundS¹
. a generic pointloop i
tosucℤPath i
.Generalize this across the circle.
In this part, we focus on 1
, 2
and 3
.
Defining sucℤ
Set up the definition of
sucℤ
so that it is of the form :Name : TypeOfSpace Name inputs = ?
Just writing in the name and the type of the space is enough for now. Load the file and check that it is looks like:
Solution:
sucℤ : ℤ → ℤ sucℤ = ?
We will define
sucℤ
the same way we definedloop_times
: by induction. Do cases on the input ofsucℤ
. You should have something like :Solution:
sucℤ : ℤ → ℤ sucℤ pos n = ? sucℤ negsuc n = ?
For the non-negative integers
pos n
we want to map to its successor. Recall that then
here is a point of the naturalsℕ
whose definition is :data ℕ : Type where zero : ℕ suc : ℕ → ℕ
Use
suc
to mappos n
to its successor.The negative integers require a bit more care. Recall that annoyingly
negsuc n
means “- (n + 1)
”. We want to map- (n + 1)
to- n
. Try doing this. Then realise “you run out of negative integers at-(0 + 1)
” so you must do cases onn
and treat the-(0 + 1)
case separately.Hint
Do
C-c C-c
onn
. Then mapnegsuc zero
topos zero
. Fornegsuc (suc n)
, map it tonegsuc n
.This completes the definition of
sucℤ
. UseC-c C-n
to check it computes correctly. E.g. check thatsucℤ (negsuc zero)
computes topos zero
andsucℤ (pos zero)
computes topos (suc zero)
.
sucℤ
is an Isomorphism
The goal is to define
predℤ : ℤ → ℤ
which “takesn
to its predecessorn - 1
”. This will act as the (homotopical) inverse ofsucℤ
. Now that you have experience from definingsucℤ
, try definingpredℤ
.Imitating what we did with
flipIso
and give a pointsucℤIso : ℤ ≅ ℤ
by usingpredℤ
as the inverse and provingsection sucℤ predℤ
andretract sucℤ predℤ
.
sucℤ
is a Path
Imitating what we did with
flipPath
, upgradesucℤIso
tosucℤPath
.
Part 2 - Winding Number
The ℤ
-bundle helix
We want to make a ℤ
-bundle over S¹
by
‘copying ℤ across the loop via sucℤPath
’.
In Quest1.agda
locate
helix : S¹ → Type
helix = {!!}
Try to imitate the definition of doubleCover
to define the bundle helix
.
You should compare your definition to ours in Quest1Solutions.agda
.
Note that we have called this helix
, since the picture of this ℤ
-bundle
looks like
Counting Loops
Now we can do what was originally difficult - constructing an inverse map
(over all points).
Now we want to be able to count how many times a path base ≡ base
loops around
S¹
, which we can do now using helix
and finding end points of ‘lifted’ paths.
For example the path loop
should loop around once,
counted by looking at the end point of ‘lifted’ loop
, starting at 0
.
Hence try to define
windingNumberBase : base ≡ base → helix base
windingNumberBase = {!!}
Hint
endPt
evaluates the end point of ‘lifted paths’.
Try computing a few values using C-c C-n
,
you can try it on refl
, loop
, ‘loop three times’, ‘loop negative one times’ and so on.
Generalising
The function windingNumberBase
can actually be improved without any extra work to a function on all of S¹
.
windingNumber : (x : S¹) → base ≡ x → helix x
windingNumber = {!!}
Try filling this in.
We will show that this and a general version of loop_times
are
inverses of each other over S¹
, in particular obtaining an isomorphism
between base ≡ base
and ℤ
.