Documentation

Mathlib.Topology.Homotopy.HSpaces

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

Main Results #

To Do #

References #

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

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.

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

    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.

    Instances For

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

      Instances For

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

        Instances For
          theorem unitInterval.qRight_zero_right (t : unitInterval) :
          ↑(unitInterval.qRight (t, 0)) = if t 1 / 2 then 2 * t else 1
          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 γ.

          Instances For
            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) :
            theorem Path.delayReflRight_one {X : Type u} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
            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 ∧ γ.

            Instances For
              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) :
              theorem Path.delayReflLeft_one {X : Type u} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :

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