Eilenberg-MacLane space (changes)

Showing changes from revision #1 to #2:
Added | ~~Removed~~ | ~~Chan~~ged

~~
~~

Let $G$ be an abelian group?, and $n$ a natural number?. The Eilenberg-MacLane space $K(G,n)$ is the unique space that has $\pi_n(K(G,n)\cong G$ and it’s other homotopy groups trivial.

These spaces are a basic tool in classical algebraic topology, they can be used to define cohomology.

Let $G$ be an group, the **Eilenberg-MacLane space** $K(G,1)$, the higher inductive 1-type with the following constructors:

- $base : K(G,1)$
- $loop : G \to (base = base)$
- $id : loop(e) = refl_{base}$
- $comp : \prod_{(x,y:G)} loop(x \cdot y) = loop(y) \circ loop(x)$

$base$ is a point of $K(G,1)$, $loop$ is a function that constructs a path from $base$ to $base$ for each element of $G$. $id$ says the path constructed from the identity element is the trivial loop. Finally, $comp$ says that the path constructed from group multiplication of elements is the concatenation of paths.

It should be noted that this type is 1-truncated? which could be added as another constructor:

- $\displaystyle \prod_{x,y:K(G,1)} \prod_{p,q:x=y} \prod_{r,s:p=q} r = s$

To define a function $f : K(G,1) \to C$ for some type $C$, it suffices to give

- a point $c : C$
- a family of loops $l : G \to (c = c)$
- a path $l(e)=id$
- a path $l(x \cdot y) = l(y) \circ l(x)$
- a proof that $C$ is a 1-type.

Then $f$ satisfies the equations

$f(base) \equiv c$

$ap_{f} (loop(x))=l(x)$

It should be noted that the above can be compressed, to specify a function $f : K(G,1) \to C$, it suffices to give:

- a proof that $C$ is a 1-type
- a point $c : C$
- a group homomorphism from $G$ to $\Omega(C,c)$

category: homotopy theory

Last revised on January 19, 2019 at 13:39:40. See the history of this page for a list of all contributions to it.