H-spaces

This file defines H-spaces mainly following the approach proposed by Serre in his paper Homologie singulière des espaces fibrés. The idea beneath H-spaces is that they are topological spaces with a binary operation ⋀ : X → X → X that is a homotopic-theoretic weakening of an operation what would make X into a topological monoid. In particular, there exists a "neutral element" e : X such that λ x, e ⋀ x and λ x, x ⋀ e are homotopic to the identity on X, see the Wikipedia page of H-spaces.

Some notable properties of H-spaces are

• Their fundamental group is always abelian (by the same argument for topological groups);
• Their cohomology ring comes equipped with a structure of a Hopf-algebra;
• The loop space based at every x : X carries a structure of an H-spaces.

Main Results

• Every topological group G is an H-space using its operation * : G → G → G (this is already true if G has an instance of a MulOneClass and ContinuousMul);
• Given two H-spaces X and Y, their product is again an H-space. We show in an example that starting with two topological groups G, G', the H-space structure on G × G' is definitionally equal to the product of H-space structures on G and G'.
• The loop space based at every x : X carries a structure of an H-spaces.

To Do

• Prove that for every NormedAddTorsor Z and every z : Z, the operation λ x y, midpoint x y defines an H-space structure with z as a "neutral element".
• Prove that S^0, S^1, S^3 and S^7 are the unique spheres that are H-spaces, where the first three inherit the structure because they are topological groups (they are Lie groups, actually), isomorphic to the invertible elements in ℤ, in ℂ and in the quaternion; and the fourth from the fact that S^7 coincides with the octonions of norm 1 (it is not a group, in particular, only has an instance of MulOneClass).

References

• [J.-P. Serre, Homologie singulière des espaces fibrés. Applications, Ann. of Math (2) 1951, 54, 425–505][serre1951]

class HSpace (X : Type u) [TopologicalSpace X] : Type u

• hmul : C(X × X, X)
• e : X
• hmul_e_e : ↑HSpace.hmul (HSpace.e, HSpace.e) = HSpace.e
• eHmul : ContinuousMap.HomotopyRel (ContinuousMap.comp HSpace.hmul (ContinuousMap.prodMk (ContinuousMap.const X HSpace.e) (ContinuousMap.id X))) (ContinuousMap.id X) {HSpace.e}
• hmulE : ContinuousMap.HomotopyRel (ContinuousMap.comp HSpace.hmul (ContinuousMap.prodMk (ContinuousMap.id X) (ContinuousMap.const X HSpace.e))) (ContinuousMap.id X) {HSpace.e}

A topological space X is an H-space if it behaves like a (potentially non-associative) topological group, but where the axioms for a group only hold up to homotopy.

def HSpaces.«term_⋀_» : Lean.TrailingParserDescr

instance HSpace.prod (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] [HSpace X] [HSpace Y] : HSpace (X × Y)

theorem TopologicalAddGroup.toHSpace.proof_1 (M : Type u_1) [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] : Continuous fun p => p.fst + p.snd

theorem TopologicalAddGroup.toHSpace.proof_2 (M : Type u_1) [AddZeroClass M] : 0 + 0 = 0

theorem TopologicalAddGroup.toHSpace.proof_4 (M : Type u_1) [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] : ContinuousMap.comp (ContinuousMap.mk (Function.uncurry Add.add)) (ContinuousMap.prodMk (ContinuousMap.const M 0) (ContinuousMap.id M)) = ContinuousMap.id M

theorem TopologicalAddGroup.toHSpace.proof_5 (M : Type u_1) [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] : ContinuousMap.comp (ContinuousMap.mk (Function.uncurry Add.add)) (ContinuousMap.prodMk (ContinuousMap.id M) (ContinuousMap.const M 0)) = ContinuousMap.comp (ContinuousMap.mk (Function.uncurry Add.add)) (ContinuousMap.prodMk (ContinuousMap.id M) (ContinuousMap.const M 0))

theorem TopologicalAddGroup.toHSpace.proof_6 (M : Type u_1) [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] : ContinuousMap.comp (ContinuousMap.mk (Function.uncurry Add.add)) (ContinuousMap.prodMk (ContinuousMap.id M) (ContinuousMap.const M 0)) = ContinuousMap.id M

theorem TopologicalAddGroup.toHSpace.proof_3 (M : Type u_1) [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] : ContinuousMap.comp (ContinuousMap.mk (Function.uncurry Add.add)) (ContinuousMap.prodMk (ContinuousMap.const M 0) (ContinuousMap.id M)) = ContinuousMap.comp (ContinuousMap.mk (Function.uncurry Add.add)) (ContinuousMap.prodMk (ContinuousMap.const M 0) (ContinuousMap.id M))

def TopologicalAddGroup.toHSpace (M : Type u) [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] : HSpace M

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 TopologicalAddGroup.hSpace an instance.

def TopologicalGroup.toHSpace (M : Type u) [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] : HSpace M

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 TopologicalGroup.hSpace an instance."

instance TopologicalAddGroup.hSpace (G : Type u) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : HSpace G

instance TopologicalGroup.hSpace (G : Type u) [TopologicalSpace G] [Group G] [TopologicalGroup G] : HSpace G

theorem TopologicalGroup.one_eq_hSpace_e {G : Type u} [TopologicalSpace G] [Group G] [TopologicalGroup G] : 1 = HSpace.e

def unitInterval.qRight (p : ↑unitInterval × ↑unitInterval) : ↑unitInterval

qRight is analogous to the function Q defined on p. 475 of [serre1951] that helps proving continuity of delayReflRight.

theorem unitInterval.continuous_qRight : Continuous unitInterval.qRight

theorem unitInterval.qRight_zero_left (θ : ↑unitInterval) : unitInterval.qRight (0, θ) = 0

theorem unitInterval.qRight_one_left (θ : ↑unitInterval) : unitInterval.qRight (1, θ) = 1

theorem unitInterval.qRight_zero_right (t : ↑unitInterval) : ↑(unitInterval.qRight (t, 0)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1

theorem unitInterval.qRight_one_right (t : ↑unitInterval) : unitInterval.qRight (t, 1) = t

def Path.delayReflRight {X : Type u} [TopologicalSpace X] {x : X} {y : X} (θ : ↑unitInterval) (γ : Path x y) : Path x y

This is the function analogous to the one on p. 475 of [serre1951], defining a homotopy from the product path γ ∧ e to γ.

theorem Path.continuous_delayReflRight {X : Type u} [TopologicalSpace X] {x : X} {y : X} : Continuous fun p => Path.delayReflRight p.fst p.snd

theorem Path.delayReflRight_zero {X : Type u} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : Path.delayReflRight 0 γ = Path.trans γ (Path.refl y)

theorem Path.delayReflRight_one {X : Type u} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : Path.delayReflRight 1 γ = γ

def Path.delayReflLeft {X : Type u} [TopologicalSpace X] {x : X} {y : X} (θ : ↑unitInterval) (γ : Path x y) : Path x y

This is the function on p. 475 of [serre1951], defining a homotopy from a path γ to the product path e ∧ γ.

theorem Path.continuous_delayReflLeft {X : Type u} [TopologicalSpace X] {x : X} {y : X} : Continuous fun p => Path.delayReflLeft p.fst p.snd

theorem Path.delayReflLeft_zero {X : Type u} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : Path.delayReflLeft 0 γ = Path.trans (Path.refl x) γ

theorem Path.delayReflLeft_one {X : Type u} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : Path.delayReflLeft 1 γ = γ

instance Path.instHSpacePathTopologicalSpace {X : Type u} [TopologicalSpace X] (x : X) : HSpace (Path x x)

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).