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 fun x ↦e ⋀ x and fun 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 fun 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

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.

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

theorem HSpace.hmul_e_e {X : Type u} [TopologicalSpace X] [self : HSpace X] : HSpace.hmul (HSpace.e, HSpace.e) = HSpace.e

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

The binary operation hmul on an H-space

Equations

• HSpaces.«term_⋀_» = Lean.ParserDescr.trailingNode `HSpaces.term_⋀_ 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋀") (Lean.ParserDescr.cat `term 0))

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

Equations

• One or more equations did not get rendered due to their size.

theorem TopologicalAddGroup.toHSpace.proof_6 (M : Type u_1) [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] : { toFun := Function.uncurry Add.add, continuous_toFun := ⋯ }.comp ((ContinuousMap.id M).prodMk (ContinuousMap.const M 0)) = ContinuousMap.id M

theorem TopologicalAddGroup.toHSpace.proof_3 (M : Type u_1) [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] : { toFun := Function.uncurry Add.add, continuous_toFun := ⋯ }.comp ((ContinuousMap.const M 0).prodMk (ContinuousMap.id M)) = { toFun := Function.uncurry Add.add, continuous_toFun := ⋯ }.comp ((ContinuousMap.const M 0).prodMk (ContinuousMap.id M))

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

theorem TopologicalAddGroup.toHSpace.proof_5 (M : Type u_1) [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] : { toFun := Function.uncurry Add.add, continuous_toFun := ⋯ }.comp ((ContinuousMap.id M).prodMk (ContinuousMap.const M 0)) = { toFun := Function.uncurry Add.add, continuous_toFun := ⋯ }.comp ((ContinuousMap.id M).prodMk (ContinuousMap.const M 0))

theorem TopologicalAddGroup.toHSpace.proof_4 (M : Type u_1) [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] : { toFun := Function.uncurry Add.add, continuous_toFun := ⋯ }.comp ((ContinuousMap.const M 0).prodMk (ContinuousMap.id M)) = ContinuousMap.id M

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

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[instance 600]

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

Equations

• TopologicalAddGroup.hSpace G = TopologicalAddGroup.toHSpace G

@[instance 600]

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

Equations

• TopologicalGroup.hSpace G = TopologicalGroup.toHSpace 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.

Equations

• unitInterval.qRight p = Set.projIcc 0 1 unitInterval.qRight.proof_1 (2 * ↑p.1 / (1 + ↑p.2))

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

Equations

• Path.delayReflRight θ γ = { toFun := fun (t : ↑unitInterval) => γ (unitInterval.qRight (t, θ)), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

theorem Path.continuous_delayReflRight {X : Type u} [TopologicalSpace X] {x : X} {y : X} : Continuous fun (p : ↑unitInterval × Path x y) => Path.delayReflRight p.1 p.2

theorem Path.delayReflRight_zero {X : Type u} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) : Path.delayReflRight 0 γ = γ.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 ∧ γ.

Equations

• Path.delayReflLeft θ γ = (Path.delayReflRight θ γ.symm).symm

theorem Path.continuous_delayReflLeft {X : Type u} [TopologicalSpace X] {x : X} {y : X} : Continuous fun (p : ↑unitInterval × Path x y) => Path.delayReflLeft p.1 p.2

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

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

instance Path.instHSpace {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).

Equations

• One or more equations did not get rendered due to their size.