[[!redirects Eilenberg-MacLane spaces]] [[!redirects Eilenberg-Mac Lane space]] [[!redirects Eilenberg-MacLane space]] [[!redirects Eilenberg-Mac lane space]] [[!redirects Eilenberg-Maclane space]] [[!redirects Eilenberg-MacLane spaces]] [[!redirects Eilenberg-Mac lane spaces]] [[!redirects Eilenberg-Maclane spaces]] ## Idea ## 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 its other [[homotopy groups]] trivial. These spaces are a basic tool in classical algebraic topology, they can be used to define [[cohomology]]. ## Definition ## Let $G$ be an group, the **Eilenberg-MacLane space** $K(G,1)$, the [[higher inductive type|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 [[identity type|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$ ### Recursion principle ### 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)$ ## Properties ## ## See also ## ## References ## * [[HoTT book]] * [[Eilenberg-MacLane Spaces in Homotopy Type Theory]] category: homotopy theory