Homotopy Type Theory H-space > history (changes)

Showing changes from revision #14 to #15: Added | Removed | Changed

Idea

< H-space

Sometimes we can equip a

type with a certain structure, called a H-space, allowing us to derive some nice properties about the type or even construct fibrations

Definition

A H-Space consists of

  • A type AA,
  • A basepoint e:Ae:A
  • A binary operation μ:AAA\mu : A \to A \to A
  • A left unitor
    λ: (a:A)μ(e,a)=a\lambda:\prod_{(a:A)} \mu(e,a)=a
  • A right unitor
    ρ: (a:A)μ(a,e)=a\rho:\prod_{(a:A)} \mu(a,e)=a

Properties

Let AA be a connected? H-space. Then for every a:Aa:A, the maps? μ(a,),μ(,a):AA\mu(a,-),\mu(-,a):A \to A are equivalences.

Examples

  • There is a H-space structure on the circle. See Lemma 8.5.8 of the HoTT book.

Proof. We define μ:S 1S 1S 1\mu : S^1 \to S^1 \to S^1 by circle induction:

μ(base)id S 1ap μfunext(h)\mu(base)\equiv id_{S^1}\qquad ap_{\mu}\equiv funext(h)

where h: x:S 1x=xh : \prod_{x : S^1} x = x is defined in Lemma 6.4.2 of the HoTT book. We now need to show that μ(x,e)=μ(e,x)=x\mu(x,e)=\mu(e,x)=x for every x:S 1x : S^1. Showing μ(e,x)=x\mu(e,x)=x is quite simple, the other way requires some more manipulation. Both of which are done in the book.

  • Every loop space is naturally a H-space with path concatenation as the operation. In fact every loop space is a group.

  • The type of maps? AAA \to A has the structure of a H-space, with basepoint id Aid_A, operation function composition.

  • An A3-space AA is an H-space with an equality μ(μ(a,b),c)=μ(a,μ(b,c))\mu(\mu(a, b),c)=\mu(a,\mu(b,c)) for every a:Aa:A, b:Ab:A, c:Ac:A representing associativity up to homotopy.

  • A unital magma is a 0-truncated H-space.

See also

On the nlab

Classically, an H-space is a homotopy type equipped with the structure of a unital magma in the homotopy category (only).

References

HoTT book

category: homotopy theory

Last revised on June 9, 2022 at 10:45:04. See the history of this page for a list of all contributions to it.