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

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
    theorem HSpace.hmul_e_e {X : Type u} [TopologicalSpace X] [self : HSpace X] :
    HSpace.hmul (HSpace.e, HSpace.e) = HSpace.e

    The binary operation hmul on an H-space

    Equations
    Instances For
      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_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

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

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

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

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

            Equations
            Instances For
              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) :
              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
              Instances For
                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) :
                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.