Homotopy Type Theory
James construction (Rev #9)

Definition

The James construction JAJ A on a pointed type AA. Is the higher inductive type given by

  • ϵ JA:JA\epsilon_{J A} : J A
  • α JA:AJAJA\alpha_{J A} : A \to J A \to J A
  • δ JA: x:JAx=α A(* A,x)\delta_{J A} : \prod_{x : J A} x = \alpha_A (*_A, x)

Properties

We have an equivalence of types JAΩΣAJA \simeq \Omega \Sigma A if AA is 0-connected.

We can see that JAJ A is simply the free monoid on AA. The higher inductive type is recursive which can make it difficult to study. This however can be remedied by defining a sequence of types (J nA) n:(J_n A)_{n: \mathbb{N}} together with maps (i n:J nAJ n+1A) n:(i_n : J_n A \to J_{n+1} A)_{n:\mathbb{N}} such that the type J AJ_\infty A defined as the sequential colimit of (J nA) n:(J_n A)_{n:\mathbb{N}} is equivalent to JAJ A.

This is useful as we can study the lower homotopy groups of ΩΣX\Omega \Sigma X by studying the lower homotopy groups of the sequential colimit. Which is what allows Brunerie to show π 4(S 3)=/n\pi_4(S^3) = \mathbb{Z} / n \mathbb{Z}.

References

category: homotopy theory

Revision on September 4, 2018 at 12:59:39 by Ali Caglayan. See the history of this page for a list of all contributions to it.