Chapter 202Core route

Coverings, van Kampen, and the Fundamental Group

The constructor $loop : base = base$ does not reduce an arbitrary loop of the circle to a visible power of $loop$ . A family over the circle can, however, record how many times transport winds around that constructor. Building such a family turns the missing normal form into the calculation $Ω (S^{1}) ≃ Z$ .

Pointed types and homotopy groups

A loop space is based at a chosen point. We therefore work with pairs $(A, a_{0})$ , where $a_{0} : A$ .

Convention 69.1 — Ambient theory; basepoints ¶

Throughout this chapter the ambient theory is that of part IV: the intensional base with univalence (definition 65.6), truncations (definition 66.33 and the $n$ -truncations of chapter 66), and the higher inductive types of chapter 68. Spheres carry the suspension presentation $S^{0} : = 2$ , $S^{n + 1} : = Susp (S^{n})$ , pointed at $N$ ; the equivalence between $Susp 2$ and the higher inductive circle of definition 68.8 is written $e_{S} : Susp 2 ≃ S^{1}$ , with $e_{S} (N) = base$ ; pointed statements are transported explicitly along this equivalence when the presentations are compared.

Referenced from 3 locations

Coverings, van Kampen, and the Fundamental Group

Definition 69.2 — Pointed types and maps ¶

Use the pointed types and loop spaces of definition 62.15 and the based-map type ${Map}_{*}$ of definition 68.22. We write $f : (X, x_{0}) \to_{∙} (Y, y_{0})$ for an element of ${Map}_{*} ((X, x_{0}), (Y, y_{0}))$ ; such an element is a pointed map, a map together with a path carrying the chosen source point to the chosen target point. The zero map $0 : (X, x_{0}) \to_{∙} (Y, y_{0})$ is $(λ x . y_{0}, {refl}_{y_{0}})$ . A pointed equivalence is a pointed map whose underlying map is an equivalence (definition 62.21).

Referenced from 2 locations

Coverings, van Kampen, and the Fundamental Group

Definition 69.4 — Homotopy groups ¶

Let $(A, a_{0})$ be a pointed type. For $n \geq 1$ the $n$ -th homotopy group of $A$ at $a_{0}$ is the set $π_{n} (A, a_{0}) : = ‖ Ω^{n} (A, a_{0}) ‖_{0},$ the $0$ -truncation of the underlying type of the $n$ -fold loop space. We further set $π_{0} (A) : = ‖ A ‖_{0}$ ; it is a pointed set when $A$ is pointed, but carries no group structure and needs no basepoint to be defined. For a pointed type whose point has already been named $a_{0}$ , we write $π_{n} (A)$ for $π_{n} (A, a_{0})$ .

Referenced from 2 locations

Coverings, van Kampen, and the Fundamental Group

Proposition 69.5 — Group structure ¶

For $n \geq 1$ , path concatenation and inversion descend to $π_{n} (A, a_{0})$ , making it a group with unit $| refl |_{0}$ .

Referenced from 3 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Proposition 69.5 — Group structure

Proof. Write $X : = Ω^{n} (A, a_{0})$ . Since $‖ X ‖_{0}$ is a set, the map $λ p . λ q . | p \cdot q |_{0} : X \to X \to ‖ X ‖_{0}$ extends along the truncation in each argument by $0$ -truncation recursion (chapter 66), giving a binary operation on $‖ X ‖_{0}$ ; inversion extends likewise. Each group law is an equality in the set $‖ X ‖_{0}$ , hence a proposition, so by truncation induction it suffices to verify it on elements of the form $| p |_{0}$ , where it follows from the groupoid laws of the identity type (theorem 30.20). ◻

A double loop can be composed vertically or horizontally. The whiskering operations and their interchange law were constructed in construction 62.3, lemma 62.4; their Eckmann–Hilton application is theorem 62.17. We record only the new descent through set truncation.

Construction 69.6 — Whiskering and horizontal composition ¶

The operations used here are exactly those of construction 62.3: right whiskering, left whiskering, and the two horizontal composites. This paragraph introduces no second convention.

Referenced from 3 locations

Coverings, van Kampen, and the Fundamental Group

Lemma 69.7 — Interchange ¶

The two horizontal composites agree. At a doubly reflexive boundary they reduce, respectively, to the two orders of vertical composition.

Referenced from 3 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Lemma 69.7 — Interchange

Proof. This is lemma 62.4, followed by the reflexivity computations displayed in the proof of theorem 62.17. ◻

Theorem 69.8 — Eckmann–Hilton ¶

For every pointed type $(A, a_{0})$ and all $α, β : Ω^{2} (A, a_{0})$ we have $α \cdot β = β \cdot α$ .

Referenced from 2 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Theorem 69.8 — Eckmann–Hilton

Proof. This is theorem 62.17 at $(A, a_{0})$ . ◻

Corollary 69.9 ¶

For $n \geq 2$ , the group $π_{n} (A, a_{0})$ is abelian.

Referenced from 2 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Corollary 69.9

Proof. $π_{n} (A, a_{0}) = ‖ Ω^{2} (Ω^{n - 2} (A, a_{0})) ‖_{0}$ , and by theorem 62.17 concatenation on this double loop space is commutative; commutativity descends to the truncation as in proposition 69.5. ◻

Lemma 69.10 — Truncation and loop spaces ¶

For every type $A$ , points $a, b : A$ , and $n \geq - 1$ , $‖ a =_{A} b ‖_{n} ≃ (| a |_{n + 1} =_{‖ A ‖_{n + 1}} | b |_{n + 1}) .$ In particular $‖ Ω (A, a) ‖_{n} ≃ Ω (‖ A ‖_{n + 1}, | a |_{n + 1})$ .

Referenced from 3 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Lemma 69.10 — Truncation and loop spaces

Proof. Apply theorem 66.56 to $a, b : A$ . Its encode–decode equivalence sends $| p |_{n}$ to ${ap}_{| - |_{n + 1}} (p)$ and is the displayed map. ◻

Corollary 69.11 ¶

For $k \geq 0$ , $π_{k} (A, a_{0}) ≃ Ω^{k} (‖ A ‖_{k}, | a_{0} |_{k})$ .

Referenced from 2 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Corollary 69.11

Proof. Iterate lemma 69.10 $k$ times: $‖ Ω^{k} (A) ‖_{0} ≃ Ω (‖ Ω^{k - 1} (A) ‖_{1}) ≃ \dots ≃ Ω^{k} (‖ A ‖_{k})$ . ◻

Construction 69.12 — Functoriality ¶

A pointed map $f : (X, x_{0}) \to_{∙} (Y, y_{0})$ induces a pointed map $Ω f : Ω (X, x_{0}) \to_{∙} Ω (Y, y_{0}), (Ω f) (p) : = f_{0}^{- 1} \cdot {ap}_{f} (p) \cdot f_{0},$ At reflexivity this term is $f_{0}^{- 1} \cdot refl \cdot f_{0} = f_{0}^{- 1} \cdot f_{0} = {refl}_{y_{0}}$ by the unit and inverse laws; this path is the pointing witness. Iterating and truncating yields $π_{n} (f) : = ‖ Ω^{n} f ‖_{0} : π_{n} (X, x_{0}) \to π_{n} (Y, y_{0})$ , a group homomorphism for $n \geq 1$ .

Referenced from 3 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Construction 69.12 — Functoriality

Proof. The identity-type functoriality law ${ap}_{f} (p \cdot q) = {ap}_{f} (p) \cdot {ap}_{f} (q)$ follows by path induction on $p, q$ . Expanding the two conjugations in $(Ω f) (p) \cdot (Ω f) (q)$ , the adjacent $f_{0} \cdot f_{0}^{- 1}$ cancels by theorem 30.20, leaving $(Ω f) (p \cdot q)$ . Iteration preserves this equation. Double truncation induction then proves that $π_{n} (f)$ preserves the group operation; the unit follows from the same calculation at reflexivity. ◻

Proposition 69.13 — Homotopy invariance ¶

If $f : (X, x_{0}) \to_{∙} (Y, y_{0})$ is a pointed equivalence, then $π_{n} (f)$ is an isomorphism for every $n \geq 1$ , and $π_{0} (f)$ is a bijection.

Referenced from 4 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Proposition 69.13 — Homotopy invariance

Proof. If $f$ is an equivalence then so is ${ap}_{f}$ on each path space (chapter 62), hence so is $Ω f$ (composition with the invertible conjugation by $f_{0}$ ), hence so is $Ω^{n} f$ by iteration, hence so is $‖ Ω^{n} f ‖_{0}$ , since truncation preserves equivalences (chapter 66). A bijective homomorphism is an isomorphism. ◻

Example 69.14 ¶

If $A$ is contractible, then $π_{n} (A, a_{0}) = 0$ for all $n \geq 1$ and $π_{0} (A) = 1$ : contractibility is preserved by $Ω$ and by truncation. More generally proposition 69.13 computes the homotopy groups of any type equivalent to a known one.

Referenced from 3 locations

Coverings, van Kampen, and the Fundamental Group

Example 69.15 ¶

For pointed types $(A, a_{0})$ and $(B, b_{0})$ there is an isomorphism $π_{n} (A \times B) ≅ π_{n} (A) \times π_{n} (B)$ for $n \geq 1$ . The nondependent case of theorem 62.30 gives the pointed equivalence $Ω (A \times B, (a_{0}, b_{0})) ≃ Ω (A, a_{0}) \times Ω (B, b_{0}), p \mapsto ({ap}_{{pr}_{1}} p, {ap}_{{pr}_{2}} p) .$ Its inverse pairs two paths; path induction on both inputs proves the two inverse homotopies. Iterating gives the equivalence of $n$ -fold loop spaces, and set truncation preserves products and equivalences. Concatenation is componentwise, so the induced bijection is a group isomorphism.

Referenced from 4 locations

Coverings, van Kampen, and the Fundamental Group

Exercise 69.1 ¶

★★☆ Starting from construction 62.3, write out the path inductions for the whiskerings recalled in construction 69.6, state their computation rules at reflexivity, and reconstruct the proof of lemma 69.7.

Referenced from 3 locations

Exercise 69.2 ¶

★★☆ Prove that $π_{n} (f)$ of construction 69.12 is a group homomorphism for $n \geq 1$ , that $π_{n} (id) = id$ , and that $π_{n} (g \circ f) = π_{n} (g) \circ π_{n} (f)$ for composable pointed maps.

Referenced from 3 locations

Exercise 69.3 ¶

★☆☆ Using theorem 62.30, construct a pointed equivalence $Ω (A \times B) ≃ Ω (A) \times Ω (B)$ and deduce the isomorphism of example 69.15.

Referenced from 3 locations

The fundamental group of the circle

We use a concrete integer type rather than importing an abstract algebraic construction. Put $Z : = N + 1 + N$ with constructors $pos (n)$ for $n + 1$ , $0$ for the middle summand, and $neg (n)$ for $- (n + 1)$ . Define successor and predecessor by coproduct and natural-number elimination: $\begin{array}{ccccc} z & pos (n) & 0 & neg (0) & neg (n + 1) \\ {suc}_{Z} (z) & pos (n + 1) & pos (0) & 0 & neg (n) \\ {pred}_{Z} (z) & {\begin{cases} 0 & n = 0, \\ pos (m) & n = m + 1, \end{cases} & neg (0) & neg (1) & neg (n + 2) \end{array}$ The two rows are mutually inverse by case analysis, so ${suc}_{Z} : Z ≃ Z$ has chosen inverse ${pred}_{Z}$ . These displayed case equations are judgmental computation rules for the chosen coproduct presentation.

For $j, k : Z$ , define $j + k$ by integer induction on $k$ : start at $j + 0 \equiv j$ , iterate ${suc}_{Z}$ through the positive summand, and iterate ${pred}_{Z}$ through the negative summand. Consequently $j + (k + 1) = {suc}_{Z} (j + k), j + (k - 1) = {pred}_{Z} (j + k),$ with judgmental equalities after exposing the corresponding constructor of $k$ . The unit and associativity laws, and the facts that $1$ and $- 1$ act by successor and predecessor, follow by integer induction. Later calculations use only these equations.

The successor equivalence ${suc}_{Z} : Z ≃ Z$ determines a family $code : S^{1} \to U$ with $code (base) : = Z$ and monodromy ${suc}_{Z}$ . Transport in this family records a loop’s winding number. We use the displayed coproduct eliminator in the induction below.

Lemma 69.16 — Integer induction ¶

Let $P : Z \to U$ with $d_{0} : P (0)$ , $d_{+} : \prod_{n : N} P (n) \to P (n + 1)$ , and $d_{-} : \prod_{n : N} P (- n) \to P (- (n + 1))$ . Then there is $f : \prod_{k : Z} P (k)$ with $f (0) \equiv d_{0}$ , $f (n + 1) \equiv d_{+} (n, f (n))$ , and $f (- (n + 1)) \equiv d_{-} (n, f (- n))$ for $n : N$ .

Referenced from 6 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Lemma 69.16 — Integer induction

Proof. Take $Z : = N + 1 + N$ , with the middle summand representing $0$ , the left summand $n + 1$ , and the right summand $- (n + 1)$ . Eliminate the coproduct. Use $d_{0}$ in the middle case; in the positive and negative summands, use ordinary natural-number induction with steps $d_{+}$ and $d_{-}$ respectively. The three equations are the coproduct and natural-number computation rules. ◻

One cannot define a winding-number function $Ω (S^{1}, base) \to Z$ by path induction: path induction varies an endpoint, whereas a loop fixes both endpoints at $base$ , and its reflexivity case would collapse the generator. The repair is to define a family over a variable endpoint and let transport in that family record the winding. This is the universal cover below.

Definition 69.17 — Universal cover of the circle ¶

Define $code : S^{1} \to U_{0}$ by circle recursion (definition 68.8): $code (base) : = Z, {ap}_{code} (loop) : = ua ({suc}_{Z}),$ where $ua$ converts the successor equivalence into a path in the universe (construction 65.8).

Referenced from 3 locations

Coverings, van Kampen, and the Fundamental Group

The fiber of this family over $base$ is $Z$ ; transporting along $loop$ moves one step up the fiber. The element $k : Z$ will code the path that winds $k$ times around the circle. Univalence is essential here: it converts the nontrivial automorphism ${suc}_{Z}$ of $Z$ into a nontrivial path in $U_{0}$ .

Lemma 69.18 — Transport in the cover ¶

For all $k : Z$ , ${tr}_{loop}^{code} (k) = k + 1 and {tr}_{{loop}^{- 1}}^{code} (k) = k - 1.$

Referenced from 4 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Lemma 69.18 — Transport in the cover

Proof. For the first equation, $\begin{aligned} {tr}_{loop}^{code} (k) & = {tr}_{{ap}_{code} (loop)}^{X \mapsto X} (k) & (composite-family transport) \\ = {tr}_{ua ({suc}_{Z})}^{X \mapsto X} (k) & (circle recursion) \\ = k + 1 & (theorem 65.9 (i)). \end{aligned}$ The last equality is an identity in $Z$ , not a judgmental reduction of $ua$ . Since ${tr}_{p}^{P}$ and ${tr}_{p^{- 1}}^{P}$ are mutually inverse (theorem 30.20 and functoriality of transport), the second equation follows: ${tr}_{{loop}^{- 1}}^{code}$ is inverse to the successor, i.e. the predecessor. ◻

Construction 69.19 — Encoding ¶

Define $encode : \prod_{x : S^{1}} (base =_{S^{1}} x) \to code (x)$ by ${encode}_{x} (p) : = {tr}_{p}^{code} (0) .$

Referenced from 2 locations

Coverings, van Kampen, and the Fundamental Group

Construction 69.20 — Integer powers of the loop ¶

By lemma 69.16, define ${loop}^{(-)} : Z \to (base =_{S^{1}} base)$ by $\begin{aligned} {loop}^{0} & : = {refl}_{base}, \\ {loop}^{n + 1} & : = {loop}^{n} \cdot loop, \\ {loop}^{- (n + 1)} & : = {loop}^{- n} \cdot {loop}^{- 1} (n : N) . \end{aligned}$

Referenced from 2 locations

Coverings, van Kampen, and the Fundamental Group

Lemma 69.21 ¶

For all $k : Z$ , ${loop}^{k - 1} \cdot loop = {loop}^{k}$ .

Referenced from 4 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Lemma 69.21

Proof. By lemma 69.16 on $k$ . For $k = n + 1$ with $n \geq 0$ this is the defining equation. For $k = 0$ and $k = - n$ , unfold the definition of the negative powers and cancel ${loop}^{- 1} \cdot loop$ by the groupoid laws (theorem 30.20). ◻

Lemma 202.21 — Addition of winding powers ¶

For all $j, k : Z$ , ${loop}^{j + k} = {loop}^{j} \cdot {loop}^{k}$ .

Referenced from 3 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Lemma 202.21 — Addition of winding powers

Proof. Use integer induction on $k$ . At $0$ the claim is the right-unit law. For the positive step, unfold ${loop}^{k + 1} = {loop}^{k} \cdot loop$ , apply the induction hypothesis, and reassociate. From lemma 69.21, cancellation gives ${loop}^{m - 1} = {loop}^{m} \cdot {loop}^{- 1}$ for every $m$ . The negative step now follows from the induction hypothesis by appending ${loop}^{- 1}$ and reassociating. All cancellations and associations are laws of theorem 30.20. ◻

Construction 69.22 — Decoding ¶

Put $F (x) : = code (x) \to (base = x)$ . Circle induction defines $decode : \prod_{x : S^{1}} code (x) \to (base =_{S^{1}} x)$ . At $base$ take ${loop}^{(-)}$ ; the loop case asks for a path ${tr}_{loop}^{F} ({loop}^{(-)}) = {loop}^{(-)}$ .

Referenced from 2 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Construction 69.22 — Decoding

Proof. Put $r (q) : = q \cdot loop$ and $s (k) : = k - 1$ . For the required coherence, compute $\begin{aligned} {tr}_{loop}^{F} ({loop}^{(-)}) & = r \circ {loop}^{(-)} \circ s & (function-family transport) \\ = λ k . {loop}^{k - 1} \cdot loop \\ = λ k . {loop}^{k} & (lemma 69.21), \end{aligned}$ The first equality also uses transport in path families and lemma 69.18. The last step uses function extensionality (theorem 65.18). This is the loop coherence required by circle induction, which therefore defines $decode$ . ◻

Lemma 69.23 ¶

For all $x : S^{1}$ and $p : base =_{S^{1}} x$ , ${decode}_{x} ({encode}_{x} (p)) = p$ .

Referenced from 3 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Lemma 69.23

Proof. By path induction it suffices to consider $x \equiv base$ , $p \equiv {refl}_{base}$ . Then ${encode}_{base} (refl) \equiv {tr}_{refl}^{code} (0) \equiv 0$ and ${decode}_{base} (0) \equiv {loop}^{0} \equiv {refl}_{base}$ . ◻

Lemma 69.24 ¶

For all $x : S^{1}$ and $c : code (x)$ , ${encode}_{x} ({decode}_{x} (c)) = c$ .

Referenced from 3 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Lemma 69.24

Proof. Put $P (x) : = \prod_{c : code (x)} {encode}_{x} ({decode}_{x} (c)) = c$ . Each $P (x)$ is a proposition because $code (x)$ is a set. Hence the two endpoints required for the $loop$ case are equal, and circle induction reduces the proof to $P (base)$ . There we show ${encode}_{base} ({loop}^{k}) = k$ for all $k : Z$ , by lemma 69.16:

$k = 0$ : both sides are $0$ by definition.
$k = n + 1$ : $\begin{aligned} {encode}_{base} ({loop}^{n + 1}) & = {tr}_{{loop}^{n} \cdot loop}^{code} (0) \\ = {tr}_{loop}^{code} ({tr}_{{loop}^{n}}^{code} (0)) & (functoriality of transport) \\ = {tr}_{{loop}^{n}}^{code} (0) + 1 & (lemma 69.18) \\ = n + 1 & (inductive hypothesis). \end{aligned}$
$k = - (n + 1)$ : put $q_{n} : = {loop}^{- n}$ and $z_{n} : = {encode}_{base} ({loop}^{- (n + 1)})$ . Then $\begin{aligned} z_{n} & = {tr}_{q_{n} \cdot {loop}^{- 1}}^{code} (0) \\ = {tr}_{{loop}^{- 1}}^{code} ({tr}_{q_{n}}^{code} (0)) & (functoriality of transport) \\ = {tr}_{q_{n}}^{code} (0) - 1 & (lemma 69.18) \\ = - n - 1 & (inductive hypothesis) \\ = - (n + 1) . \end{aligned}$

◻

Theorem 69.25 — The fundamental group of the circle ¶

There is a family of equivalences $\prod_{x : S^{1}} (base =_{S^{1}} x) ≃ code (x) .$ Consequently $Ω (S^{1}, base) ≃ Z$ ; this equivalence carries concatenation to addition, so $π_{1} (S^{1}, base) ≅ Z and π_{n} (S^{1}, base) = 0 (n > 1) .$

Referenced from 5 locations

Proof of Theorem 69.25 — The fundamental group of the circle

Proof. By lemma 69.23, lemma 69.24, ${encode}_{x}$ and ${decode}_{x}$ are quasi-inverse, hence ${encode}_{x}$ is an equivalence (chapter 62). Instantiating at $x : = base$ gives $Ω (S^{1}) ≃ Z$ , with inverse ${loop}^{(-)}$ . By lemma 202.21, ${loop}^{j + k} = {loop}^{j} \cdot {loop}^{k}$ , so ${loop}^{(-)}$ is a bijective homomorphism $(Z, +) \to Ω (S^{1})$ ; applying $‖ - ‖_{0}$ and noting that $Z$ is a set yields $π_{1} (S^{1}) ≅ ‖ Z ‖_{0} ≅ Z$ .

For $n \geq 2$ : the pointed equivalence $Ω (S^{1}) ≃ (Z, 0)$ induces, by proposition 69.13, $Ω^{n} (S^{1}) ≃ Ω^{n - 1} (Z, 0)$ . Since $Z$ is a set, $Ω (Z, 0) = (0 =_{Z} 0)$ is an inhabited proposition, hence contractible, and so are all its iterated loop spaces; therefore $π_{n} (S^{1}) = ‖ Ω^{n} (S^{1}) ‖_{0} = 0$ by example 69.14. ◻

Remark 69.26 — Winding numbers ¶

The proof is computational in content: for a concrete loop such as $loop \cdot {loop}^{- 1} \cdot loop$ , the function $encode$ transports $0$ through the composite ${suc}_{Z} \circ {pred}_{Z} \circ {suc}_{Z}$ and returns the winding number $1$ . In the axiomatic theory of part IV the computation is a chain of propositional equalities, since $ua$ does not reduce.

Referenced from 2 locations

Coverings, van Kampen, and the Fundamental Group

Remark 69.27 — Univalence is necessary ¶

Without univalence, $Ω (S^{1}) ≃ Z$ is not provable in the displayed circle signature. Interpret its point constructor by the unique point of $1$ and its loop constructor by reflexivity. Given a set $X$ , a point $x : X$ , and a loop $p : x = x$ , proof irrelevance makes $p = {refl}_{x}$ , so the required circle recursor is the constant map at $x$ and satisfies the propositional loop equation. Thus the set model of definition 48.30 extends to precisely these circle rules and interprets $Ω (S^{1})$ as $1$ . Univalence gives the nontrivial path $ua ({suc}_{Z})$ in the universe that the cover transports along.

Referenced from 2 locations

Coverings, van Kampen, and the Fundamental Group

Alternatively, the total space $\sum_{x : S^{1}} code (x)$ is contractible. Since $encode$ induces an equivalence between this total space and the contractible singleton total space of based paths, its fiber maps are equivalences. This is Shulman’s helix argument; the direct calculation above is Licata’s encode–decode proof.

Exercise 69.4 ¶

★★☆ Fix a construction of $Z$ (say $N + 1 + N$ ) and prove lemma 69.16, including the three computation rules.

Referenced from 3 locations

Exercise 69.5 ¶

★☆☆ Prove that ${loop}^{j + k} = {loop}^{j} \cdot {loop}^{k}$ for all $j, k : Z$ , by integer induction on $k$ using lemma 69.21 and theorem 30.20.

Referenced from 4 locations

Exercise 69.6 ¶

★★☆ Prove that $\sum_{x : S^{1}} code (x)$ is contractible. Conclude again that ${encode}_{x}$ is a family of equivalences, using the fact that a fiberwise map between families with equivalent total spaces over the same base is a fiberwise equivalence.

Referenced from 3 locations

Exercise 69.7 ¶

★☆☆ Compute $π_{1} (S^{1} \times S^{1}) ≅ Z \times Z$ using theorem 69.25 and example 69.15.

Referenced from 3 locations

Set-valued coverings

A family of sets over $A$ is determined by its fibers and the transport action of paths in $A$ . For the circle this reduces a covering to one set equipped with one automorphism.

Definition 202.28 — Set-valued coverings ¶

A set-valued covering of a type $A$ is a family $P : A \to U_{0}$ together with $\prod_{x : A} isSet (P (x))$ . Its total space is $\sum_{x : A} P (x)$ , projected to $A$ . Every path $p : x = y$ acts on the fibers by the transport equivalence ${tr}_{p}^{P} : P (x) ≃ P (y)$ ; functoriality of transport makes concatenation act by composition.

Referenced from 2 locations

Coverings, van Kampen, and the Fundamental Group

Here “covering” means only a type family with set-valued fibers; no topology or local-triviality structure is part of the definition.

Theorem 202.29 — Coverings of the circle ¶

There is an equivalence $(\sum_{P : S^{1} \to U_{0}} \prod_{x : S^{1}} isSet (P (x))) ≃ (\sum_{S : U_{0}} isSet (S) \times (S ≃ S)) .$ Under this equivalence the universal cover definition 69.17 corresponds to $(Z, {suc}_{Z})$ .

Referenced from 4 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Theorem 202.29 — Coverings of the circle

Proof. Evaluate a family $P$ at $base$ and transport along $loop$ : $P \mapsto (P (base), {tr}_{loop}^{P} : P (base) ≃ P (base)) .$ The circle universal property identifies maps $S^{1} \to U_{0}$ with pairs $(S, p)$ where $S : U_{0}$ and $p : S = S$ . Univalence identifies the latter path with an equivalence $S ≃ S$ . Since $isSet (-)$ is a proposition and is preserved by equivalence, circle induction shows that a proof that every fiber is a set is determined by its value at $base$ ; its loop coherence is automatic. Conversely, from a set $S$ and $e : S ≃ S$ , circle recursion with loop image $ua (e)$ constructs the family, and circle induction constructs its fiberwise set proof.

The two composites are the identity by the uniqueness clause of circle recursion and the two inverse laws for univalence. For $P : = code$ , lemma 69.18 computes the selected automorphism as successor on $Z$ . ◻

Corollary 202.30 — Monodromy classification ¶

Set-valued coverings of $S^{1}$ are equivalently sets equipped with an action of the group $Z$ .

Referenced from 2 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Corollary 202.30 — Monodromy classification

Proof. An automorphism $e : S ≃ S$ defines $k \cdot s : = e^{k} (s)$ using integer powers; the action laws follow by integer induction and the equivalence laws. Conversely, an action restricts at $1 : Z$ to an automorphism, with inverse the action of $- 1$ . The unit and multiplication laws show that these constructions are inverse. Compose this equivalence with theorem 202.29. ◻

Example 202.31 — The universal action ¶

The universal cover carries the regular translation action $k \cdot n : = n + k$ on $Z$ . Its fiber records the winding number under the encode map.

Referenced from 2 locations

Coverings, van Kampen, and the Fundamental Group

Exercise 202.8 ¶

★★☆ For a set-valued covering $P : A \to U_{0}$ and basepoint $a_{0} : A$ , prove that $p \mapsto {tr}_{p}^{P}$ sends reflexivity to the identity equivalence and concatenation to composition. Explain why it descends to an action of $π_{1} (A, a_{0})$ on $P (a_{0})$ .

Referenced from 4 locations

Exercise 202.9 ¶

★★☆ Classify the coverings of $S^{1}$ with fiber $2$ by listing the automorphisms of $2$ . Compute the monodromy of the nontrivial cover on both Boolean points and show that traversing the generating loop twice acts as the identity.

Referenced from 4 locations

Pushout path codes and van Kampen

This section is an exact, optional import of the HoTT Book’s naive van Kampen construction. The four mutually indexed word types and their double-pushout coherence form a substantial independent development; the specimen below records only its input and conclusion. The chapter’s core results are independent of the imported theorem and its two consequences.

Let $f : A \to B$ and $g : A \to C$ , and let $W$ be their higher-inductive pushout, with constructors ${in}_{A} : B \to W$ , ${in}_{B} : C \to W$ , and ${glue}_{a} : {in}_{A} (f (a)) = {in}_{B} (g (a))$ . Write $Π_{1} X (x, y) : = ‖ x =_{X} y ‖_{0}$ for the fundamental groupoid hom-set.

The failed direct approach is to eliminate a path in $W$ and hope that its constructor history remains visible. Path induction forgets that history immediately. Encode–decode instead defines a set of words first and makes transport append one generator at a time.

Convention 202.32 — Imported pushout path words ¶

For endpoints $u, v : W$ , $VK (u, v)$ denotes the family $code (u, v)$ of the HoTT Book, §8.7.1, pp. 292–294 [Uni13]. The imported package contains the four endpoint-indexed set quotients of finite alternating path words, the four crossing equivalences, and their commuting square (8.7.2). For orientation only, a word from ${in}_{A} (b)$ to ${in}_{A} (b^{'})$ has the shape $(p_{0}, a_{1}, q_{1}, a_{1}^{'}, p_{1}, \dots, a_{n}, q_{n}, a_{n}^{'}, p_{n}),$ where $\begin{aligned} p_{0} & : Π_{1} B (b, f (a_{1})), & q_{k} & : Π_{1} C (g (a_{k}), g (a_{k}^{'})), \\ p_{k} & : Π_{1} B (f (a_{k}^{'}), f (a_{k + 1})) & (k < n), & p_{n} & : Π_{1} B (f (a_{n}^{'}), b^{'}) . \end{aligned}$ The $C$ – $C$ clause reverses the roles of $B, C$ and of the $p, q$ pieces; the $B$ – $C$ and $C$ – $B$ clauses change the parity so that a word begins and ends in the indicated summands. The two quotient generators delete a reflexive $B$ -piece between adjacent $C$ -pieces, or a reflexive $C$ -piece between adjacent $B$ -pieces, and compose the newly adjacent paths. The four crossing equivalences append or remove the appropriate reflexive crossing at either end. Thus $VK$ names the source’s complete package; the displayed $B$ – $B$ shape is not a local definition of it.

Referenced from 4 locations

Coverings, van Kampen, and the Fundamental Group

The code family is defined by double pushout induction. Transport in the second endpoint along a path in $B$ or $C$ concatenates that path onto the last word component; transport along ${glue}_{a}$ appends the crossing labelled by $a$ . The overlap equations hold in a set, so no higher word coherence remains.

Theorem 202.33 — Imported: naive van Kampen; path-space form ¶

For every span $B \overset{f}{\leftarrow} A \overset{g}{\to} C$ and all $u, v : W$ , there is an equivalence $Π_{1} W (u, v) ≃ VK (u, v) .$

Referenced from 4 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Theorem 202.33 — Imported: naive van Kampen; path-space form

Proof. This is imported exactly as HoTT Book Theorem 8.7.4 [Uni13], in the higher-inductive and set-truncation signature of convention 69.1. Its proof defines encode by transport from the reflexive word and decode by concatenating the images of word components; double pushout induction and quotient induction prove the two round trips. Those inductions, including square (8.7.2), belong to the cited proof and are not claimed as local derivations here. The theorem assumes neither connectedness, choice, nor excluded middle. ◻

Definition 202.34 — Alternating-word free product ¶

Let $G$ and $H$ be groups. Form finite words whose letters are tagged elements $ι_{G} (g)$ or $ι_{H} (h)$ . Quotient these words by the least congruence containing $\begin{aligned} w ι_{G} (1) w^{'} & \sim w w^{'}, & w ι_{H} (1) w^{'} & \sim w w^{'}, \\ w ι_{G} (g) ι_{G} (g^{'}) w^{'} & \sim w ι_{G} (g g^{'}) w^{'}, & w ι_{H} (h) ι_{H} (h^{'}) w^{'} & \sim w ι_{H} (h h^{'}) w^{'} . \end{aligned}$ The quotient is denoted $G * H$ . Multiplication is concatenation, the unit is the empty word, and inversion reverses a word and inverts each letter.

Referenced from 4 locations

Coverings, van Kampen, and the Fundamental Group

Lemma 202.35 ¶

The operations of definition 202.34 are well defined and make $G * H$ a group.

Referenced from 2 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Lemma 202.35

Proof. Concatenating the same prefix and suffix preserves each generating relation, so concatenation descends to the congruence quotient. Reversal with letterwise inversion sends an identity-deletion relation to another identity-deletion relation and sends a multiplication relation in one factor to the corresponding multiplication relation in reverse order. It therefore also descends. Associativity and the unit laws descend from lists. In the product of a word with its reversed inverse, adjacent inverse letters reduce successively to identities and then disappear; the same reduction in the opposite order proves the other inverse law. ◻

Corollary 202.36 — van Kampen for a wedge ¶

For pointed connected types $(B, b_{0})$ and $(C, c_{0})$ , $π_{1} (B \lor C) ≅ π_{1} (B) * π_{1} (C),$ where $*$ is the free product of groups.

Referenced from 3 locations

Coverings, van Kampen, and the Fundamental Group

Proof of Corollary 202.36 — van Kampen for a wedge

Proof. Specialize theorem 202.33 to $A : = 1$ , $f (⋆) : = b_{0}$ , and $g (⋆) : = c_{0}$ . Every crossing label is then $⋆$ , so a loop code is an alternating word of elements of $π_{1} (B)$ and $π_{1} (C)$ . The two quotient generators delete identity letters and multiply adjacent letters from the same factor. By definition 202.34, the resulting quotient is $π_{1} (B) * π_{1} (C)$ . Decoding concatenates the two inclusions of loops, hence preserves multiplication, so the equivalence of sets in theorem 202.33 is a group isomorphism. ◻

Example 202.37 — A wedge of two circles ¶

By theorem 69.25, corollary 202.36, $π_{1} (S^{1} \lor S^{1}) ≅ Z * Z,$ the free group on the two generating loops. The word ${in}_{A} (loop) \cdot {in}_{B} (loop) \cdot {in}_{A} (loop)^{- 1}$ is already reduced; the code remembers its three alternating letters rather than merely an integer winding number.

Referenced from 2 locations

Coverings, van Kampen, and the Fundamental Group

Exercise 202.10 ¶

★★☆ Write the four endpoint forms of $VK (u, v)$ and their reflexive words. Check that transport along a $B$ -path appends to the last $B$ -component and that decoding this transported word concatenates the image of that path.

Referenced from 4 locations

Exercise 202.11 ¶

★☆☆ For the wedge of two circles, reduce the words $a a^{- 1} b$ , $a b b^{- 1}$ , and $a b a^{- 1} b^{- 1}$ using only the two quotient generators of convention 202.32. Which word represents the commutator?

Referenced from 4 locations

Suggested first pass.

Begin with exercise 69.5, exercise 202.8, continue with exercise 202.9, exercise 202.10, and finish with exercise 202.11. None of these problems is a premise of a later theorem.

The practical project is a reduced-word evaluator for $π_{1} (S^{1} \lor S^{1})$ . Represent the two generators and their inverses by four constructors. Implement insertion with cancellation of adjacent inverse letters, and test that concatenation followed by reduction respects the quotient generators of convention 202.32. The mathematical invariant is that the output has no adjacent inverse pair and decodes to the same loop as the input.

Exercise 202.12 ¶

★★★ Starting only from circle recursion and univalence, reconstruct both directions of theorem 202.29. Mark the single point where proof irrelevance of $isSet (S)$ discharges a loop coherence.

Referenced from 3 locations

Exercise 202.13 ¶

★★★ Practical project.van-kampen-word-reducer Specify the reduced-word evaluator above as a terminating recursion on lists. Prove preservation of decoding for one cancellation step and then for the whole evaluator. Give inputs whose reductions are the empty word, a one-letter word, and the four-letter commutator.

Referenced from 4 locations

Bibliographic notes

The circle cover and its encode–decode calculation follow the HoTT Book’s Chapter 8.1 development. The classification of set-valued circle families is the monodromy form of the same construction. The path-word proof of van Kampen is the HoTT Book’s Theorem 8.7.4; its wedge specialization is the classical free-product calculation internalized through set truncation [Uni13].