English
A topological group is naturally an H-space via its multiplication.
Русский
Топологическая группа естественным образом является H-пространством через свою умножение.
LaTeX
$$$\text{IsTopologicalGroup.hSpace}(G) = \text{toHSpace}(G)$$$
Lean4
/-- The definition `toHSpace` is not an instance because its additive version would
lead to a diamond since a topological field would inherit two `HSpace` structures, one from the
`MulOneClass` and one from the `AddZeroClass`. In the case of a group, we make
`IsTopologicalGroup.hSpace` an instance." -/
@[to_additive /-- The definition `toHSpace` is not an instance because it comes together with a
multiplicative version which would lead to a diamond since a topological field would inherit
two `HSpace` structures, one from the `MulOneClass` and one from the `AddZeroClass`.
In the case of an additive group, we make `IsTopologicalAddGroup.hSpace` an instance. -/
]
def toHSpace (M : Type u) [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] : HSpace M
where
hmul := ⟨Function.uncurry Mul.mul, continuous_mul⟩
e := 1
hmul_e_e := one_mul 1
eHmul := (HomotopyRel.refl _ _).cast rfl (by ext1; apply one_mul)
hmulE := (HomotopyRel.refl _ _).cast rfl (by ext1; apply mul_one)
