The fundamental group of a topological monoid is abelian

Let M be a topological space with a continuous multiplication and a two-sided unit 1, for instance a topological group. Two loops γ and δ at 1 can be multiplied pointwise, t ↦ γ t * δ t, and the result is again a loop at 1 * 1 = 1. This file shows that the class of the pointwise product is the product of the classes in π₁(M, 1), and that π₁(M, 1) is commutative.

Both facts are the Eckmann–Hilton argument, applied through Mathlib's EckmannHilton.mul and EckmannHilton.mul_comm. Multiplication M × M → M induces a homomorphism π₁(M, 1) × π₁(M, 1) ≃ π₁(M × M, (1, 1)) → π₁(M, 1), the first map being TauCeti.FundamentalGroup.prodMulEquiv, and on a pair of loop classes it is the class of the pointwise product. So pointwise multiplication of loop classes is a binary operation on π₁(M, 1) over which the group law distributes, and since 1 is a strict unit of M, the constant loop is a two-sided unit for it. Eckmann–Hilton then says that the two operations agree and are commutative.

For a topological group G the pointwise product is the group law of the universal cover based at 1, and the first fact identifies the kernel of the covering homomorphism with π₁(G, 1) (TauCeti.UniversalCover.kerProjHomEquivFundamentalGroup).

Main results

• FundamentalGroup.cast_map_prod_mul: the class of the pointwise product of two loops at 1 is their product in the fundamental group.
• FundamentalGroup.instCommGroup: the fundamental group at 1 is commutative.

References

• B. Eckmann and P. J. Hilton, Group-like structures in general categories I. Multiplications and comultiplications, Math. Ann. 145 (1962), 227–255.

theorem FundamentalGroup.cast_map_prod_mul {M : Type u_1} [TopologicalSpace M] [MulOneClass M] [ContinuousMul M] (a b : FundamentalGroup M 1) : ((Path.Homotopic.prod a b).map { toFun := fun (x : M × M) => x.1 * x.2, continuous_toFun := ⋯ }).cast ⋯ ⋯ = a * b

The pointwise product of loops is their product in the fundamental group. In a space with a continuous multiplication and a two-sided unit 1, the class of the loop t ↦ γ t * δ t is the product in π₁(M, 1) of the classes of the loops γ and δ at 1.

@[instance_reducible]

noncomputable instance FundamentalGroup.instCommGroup {M : Type u_1} [TopologicalSpace M] [MulOneClass M] [ContinuousMul M] : CommGroup (FundamentalGroup M 1)

The fundamental group of a topological monoid is abelian. In a space with a continuous multiplication and a two-sided unit 1, the fundamental group at 1 is commutative, since the group law distributes over pointwise multiplication of loops, which has the same unit.

Equations

• FundamentalGroup.instCommGroup = { toGroup := inferInstance, mul_comm := ⋯ }