James construction (changes)

Showing changes from revision #8 to #9:
Added | ~~Removed~~ | ~~Chan~~ged

The James construction $\mathrm{JAJ}A$~~ JA~~ J A on a pointed type $A$. Is the higher inductive type given by

- ${\u03f5}_{\mathrm{JA}}:\mathrm{JAJ}A$
~~\epsilon_{JA}~~\epsilon_{J A} :~~JA~~J A - ${\alpha}_{\mathrm{JA}}:A\to \mathrm{JAJ}A\to \mathrm{JAJ}A$
~~\alpha_{JA}~~\alpha_{J A} : A \to~~JA~~J A \to~~JA~~J A - ${\delta}_{\mathrm{JA}}:{\prod}_{x:\mathrm{JAJ}A}x={\alpha}_{A}({*}_{A},x)$
~~\delta_{JA}~~\delta_{J A} : \prod_{x :~~JA}~~J A} x = \alpha_A (*_A, x)

We have an equivalence of types $JA \simeq \Omega \Sigma A$ if $A$ is 0-connected.

We can see that $\mathrm{JAJ}A$~~ JA~~ J A is simply the free monoid on $A$. 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_n A)_{n: \mathbb{N}}$ together with maps $(i_n : J_n A \to J_{n+1} A)_{n:\mathbb{N}}$ such that the type $J_\infty A$ defined as the sequential colimit of $(J_n A)_{n:\mathbb{N}}$ is equivalent to $\mathrm{JAJ}A$~~ JA~~ J A.

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

category: homotopy theory

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