Homotopy Type Theory
Eilenberg-MacLane space (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Idea

Let GG be an abelian group?, and nn a natural number?. The Eilenberg-MacLane space K(G,n)K(G,n) is the unique space that has π n(K(G,n)G\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.

Definition

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

  • base:K(G,1)base : K(G,1)
  • loop:G(base=base)loop : G \to (base = base)
  • id:loop(e)=refl baseid : loop(e) = refl_{base}
  • comp: (x,y:G)loop(xy)=loop(y)loop(x)comp : \prod_{(x,y:G)} loop(x \cdot y) = loop(y) \circ loop(x)

basebase is a point of K(G,1)K(G,1), looploop is a function that constructs a path from basebase to basebase for each element of GG. idid says the path constructed from the identity element is the trivial loop. Finally, compcomp 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:

  • x,y:K(G,1) p,q:x=y r,s:p=qr=s\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)Cf : K(G,1) \to C for some type CC, it suffices to give

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

Then ff satisfies the equations

f(base)cf(base) \equiv c
ap f(loop(x))=l(x)ap_{f} (loop(x))=l(x)

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

  • a proof that CC is a 1-type
  • a point c:Cc : C
  • a group homomorphism from GG to Ω(C,c)\Omega(C,c)

Properties

See also

References

category: homotopy theory

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