Homotopy Type Theory
Seifert-van Kampen theorem

Idea

The van Kampen theorem calculates the fundamental group π 1\pi_1 of a pushout of spaces. It is traditionally stated for a topological space XX which is the union of two open subspaces UU and VV, but in homotopy-theoretic terms, this is just a a convenient way of ensuring that XX is the pushout of UU and VV over their intersection.

Groupoids

It is useful to generalise the fundamental group π 1()Ω() 0\pi_1(-)\equiv \| \Omega(-) \|_0 of a type XX to the fundamental groupoid Π 1X:XX𝒰 \Pi_1 X : X \to X \to \mathcal{U}

Π 1X(x,y)x=y 0\Pi_1 X (x, y) \equiv \| x = y \|_0

This has induced groupoid operations coming from the identity type: concatenation, inverses, identity and function application.

Theorem

Let A,B,CA, B, C be types? and f:ABf : A \to B and g:ACg : A \to C functions?. Let PB ACP\equiv B \sqcup_A C be their pushout.

By defining a special code function the statement of the theorem becomes:

Π 1P(u,v)code(u,v)\Pi_1 P(u, v) \simeq code(u,v)

this is the encode-decode method?.

Code

There are (at least) two code functions that can be given. These are listed in the HoTT Book section 8.7. The first is a “naive” van Kampen theorem. The second version is the van Kampen at a set of basepoints.

Formalisation

References

category: homotopy theory

Created on January 19, 2019 at 14:04:22. See the history of this page for a list of all contributions to it.