mathlib3 documentation

topology.homotopy.H_spaces

H-spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines H-spaces mainly following the approach proposed by Serre in his paper Homologie singulière des espaces fibrés. The idea beaneath 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 #

source
@[class]
structure H_space (X : Type u) [topological_space 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.

Instances of this typeclass
Instances of other typeclasses for H_space
  • H_space.has_sizeof_inst
source
@[protected, instance]
def H_space.prod (X : Type u) (Y : Type v) [topological_space X] [topological_space Y] [H_space X] [H_space Y] :
H_space (X × Y)
Equations
source
def topological_group.to_H_space (M : Type u) [mul_one_class M] [topological_space M] [has_continuous_mul M] :
H_space M

The definition to_H_space is not an instance because its @additive version would lead to a diamond since a topological field would inherit two H_space structures, one from the mul_one_class and one from the add_zero_class. In the case of a group, we make topological_group.H_space an instance."

Equations
source
def topological_add_group.to_H_space (M : Type u) [add_zero_class M] [topological_space M] [has_continuous_add M] :
H_space M

The definition to_H_space 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 H_space structures, one from the mul_one_class and one from the add_zero_class. In the case of an additive group, we make topological_group.H_space an instance.

Equations
source
@[protected, instance]
def topological_add_group.H_space (G : Type u) [topological_space G] [add_group G] [topological_add_group G] :
H_space G
Equations
source
@[protected, instance]
def topological_group.H_space (G : Type u) [topological_space G] [group G] [topological_group G] :
H_space G
Equations
source
theorem topological_group.one_eq_H_space_e {G : Type u} [topological_space G] [group G] [topological_group G] :
1 = H_space.e
source
noncomputable def unit_interval.Q_right (p : ↥unit_interval × ↥unit_interval) :
↥unit_interval

Q_right is analogous to the function Q defined on p. 475 of [Ser51] that helps proving continuity of delay_refl_right.

Equations
source
theorem unit_interval.continuous_Q_right  :
continuous unit_interval.Q_right
source
theorem unit_interval.Q_right_zero_left (θ : ↥unit_interval) :
unit_interval.Q_right (0, θ) = 0
source
theorem unit_interval.Q_right_one_left (θ : ↥unit_interval) :
unit_interval.Q_right (1, θ) = 1
source
theorem unit_interval.Q_right_zero_right (t : ↥unit_interval) :
↑(unit_interval.Q_right (t, 0)) = ite (↑t ≤ 1 / 2) (2 * ↑t) 1
source
theorem unit_interval.Q_right_one_right (t : ↥unit_interval) :
unit_interval.Q_right (t, 1) = t
source
noncomputable def path.delay_refl_right {X : Type u} [topological_space X] {x y : X} (θ : ↥unit_interval) (γ : path x y) :
path x y

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

Equations
source
theorem path.continuous_delay_refl_right {X : Type u} [topological_space X] {x y : X} :
continuous (λ (p : ↥unit_interval × path x y), path.delay_refl_right p.fst p.snd)
source
theorem path.delay_refl_right_zero {X : Type u} [topological_space X] {x y : X} (γ : path x y) :
path.delay_refl_right 0 γ = γ.trans (path.refl y)
source
theorem path.delay_refl_right_one {X : Type u} [topological_space X] {x y : X} (γ : path x y) :
path.delay_refl_right 1 γ = γ
source
noncomputable def path.delay_refl_left {X : Type u} [topological_space X] {x y : X} (θ : ↥unit_interval) (γ : path x y) :
path x y

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

Equations
source
theorem path.continuous_delay_refl_left {X : Type u} [topological_space X] {x y : X} :
continuous (λ (p : ↥unit_interval × path x y), path.delay_refl_left p.fst p.snd)
source
theorem path.delay_refl_left_zero {X : Type u} [topological_space X] {x y : X} (γ : path x y) :
path.delay_refl_left 0 γ = (path.refl x).trans γ
source
theorem path.delay_refl_left_one {X : Type u} [topological_space X] {x y : X} (γ : path x y) :
path.delay_refl_left 1 γ = γ
source
@[protected, instance]
noncomputable def path.H_space {X : Type u} [topological_space X] (x : X) :
H_space (path x x)

The loop space at x carries a structure of a H-space. Note that the field e_Hmul (resp. Hmul_e) neither implies nor is implied by path.homotopy.refl_trans (resp. path.homotopy.trans_refl).

Equations