English
The loop space at x, namely Path x x, admits an H-space structure with concatenation as multiplication, unit as the constant path at x, and explicit homotopies implementing the axioms.
Русский
Цикловое пространство в точке x, Path x x, обладает структурой H-пространства, где умножение — конкатенация путей, единица — константный путь в x, и заданы необходимые гомотопии.
LaTeX
$$Path x x is equipped with an H-space structure with hmul ρ = ρ.1.trans ρ.2, e = refl x, and the corresponding homotopies.$$
Lean4
/-- The loop space at x carries a structure of an H-space. Note that the field `eHmul`
(resp. `hmulE`) neither implies nor is implied by `Path.Homotopy.reflTrans`
(resp. `Path.Homotopy.transRefl`).
-/
instance (x : X) : HSpace (Path x x)
where
hmul := ⟨fun ρ => ρ.1.trans ρ.2, continuous_trans⟩
e := refl x
hmul_e_e := refl_trans_refl
eHmul :=
{ toHomotopy :=
⟨⟨fun p : I × Path x x ↦ delayReflLeft p.1 p.2, continuous_delayReflLeft⟩, delayReflLeft_zero,
delayReflLeft_one⟩
prop' := by rintro t _ rfl; exact refl_trans_refl.symm }
hmulE :=
{ toHomotopy :=
⟨⟨fun p : I × Path x x ↦ delayReflRight p.1 p.2, continuous_delayReflRight⟩, delayReflRight_zero,
delayReflRight_one⟩
prop' := by rintro t _ rfl; exact refl_trans_refl.symm }
