12. H-spaces🔗

Recall that an H-space is a pointed topological space X with a jointly continuous multiplication map X × X → X, often denoted (x, y) ↦ x ∧ y. The distinguished point e acts as an identity up to homotopy in the sense that:

• e ∧ e = e

• x ↦ x ∧ e is homotopic to the identity (through maps fixing e)

• x ↦ e ∧ x is homotopic to the identity (through maps fixing e)

In the sections which follow we outline how to discuss H-spaces in Mathlib.

1. 12.1. Defining an H-space
2. 12.2. Products
3. 12.3. Examples