Equivalences of H-spaces

Content created by Egbert Rijke.

Created on 2024-03-23.
Last modified on 2024-03-23.

module structured-types.equivalences-h-spaces where
Imports 
open import foundation.action-on-higher-identifications-functions
open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.commuting-squares-of-identifications
open import foundation.commuting-triangles-of-identifications
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.path-algebra
open import foundation.universe-levels
open import foundation.whiskering-identifications-concatenation

open import group-theory.homomorphisms-semigroups

open import structured-types.h-spaces
open import structured-types.morphisms-h-spaces
open import structured-types.pointed-equivalences
open import structured-types.pointed-maps
open import structured-types.pointed-types

Idea

Consider two H-spaces X and Y. An equivalence of H-spaces from X to Y consists of a pointed equivalence e : X ≃∗ Y that preserves the unital binary operation

  α : (x x' : X) → e (μ x x') ＝ μ (e x) (e x')

and which furthermore comes equipped with the following structure, witnessing that the unit laws are preserved:

  • For each x' : X an identification α₁ x' witnessing that the triangle

                                α * x'
                e (μ * x') -------> μ (e *) (e x')
                      \                 /
                       \               / ap (μ - (e x')) e₁
                        \             /
                         \           ∨
  ap e (left-unit-law x') \       μ * (e x')
                           \       /
                            \     / left-unit-law (e x')
                             \   /
                              ∨ ∨
                              e x'

    commutes.

  • For each x : X an identification α₂ x witnessing that the triangle

                                α x *
                e (μ x *) --------> μ (e x) (e *)
                      \                 /
                       \               / ap (μ (e x) -) e₁
                        \             /
                         \           ∨
  ap e (right-unit-law x) \       μ (e x) *
                           \       /
                            \     / right-unit-law (e x)
                             \   /
                              ∨ ∨
                              e x

    commutes.

  • An identification α₃ witnessing that the square

                                                       α₁
   α₀ * * ∙ (ap (μ - (e *)) e₁ ∙ left-unit-law *) ---> ap e (left-unit-law *)
                     |                                         |
       (α₀ * *) ·l β |                                         |
                     ∨                                         ∨
  α₀ * * ∙ (ap (μ (e *) -) e₁ ∙ right-unit-law *) ---> ap e (right-unit-law *)
                                                   α₂

    Here, the identification on the left is obtained by left whiskering the identification witnessing that the square

                                 ap (μ (e *)) e₁
              μ (e *) (e *) -----------------> μ (e *) *
                    |                               |
  ap (μ - (e *)) e₁ |                 β             | right-unit-law (e *)
                    ∨                               ∨
                 μ * (e *) ----------------------> e *
                             left-unit-law (e *)

    commutes, with the identification α * * : e (μ * *) ＝ μ (e *) (e *). The quickest way to see that this square commutes is by identification elimination on the identification e₁ : e * ＝ *, using the coherence left-unit-law * ＝ right-unit-law *. Alternatively, note that all the squares in the diagram

                                 ap (μ (e *)) e₁
              μ (e *) (e *) -----------------> μ (e *) * --------> e *
                    |                               |               |
  ap (μ - (e *)) e₁ |                 ap (μ - *) e₁ |               |
                    ∨                               ∨               ∨
                 μ * (e *) ---------------------> μ * * ----------> *
                    |            ap (μ *) e₁        |               |
                    |                               |  coh ·r refl  | refl
                    ∨                               ∨               ∨
                   e * ---------------------------> * ------------> *
                                     e₁                  refl

    commute. Therefore we obtain an identification

      ap (μ - (e *)) e₁ ∙ (left-unit-law (e *) ∙ e₁) ＝
  ap (μ (e *) -) e₁ ∙ (right-unit-law (e *) ∙ e₁).

    By unwhiskering of commuting squares of identifications, i.e., by cancelling out e₁ on both sides, it follows that the asserted square commutes.

Definition

The predicate of preserving H-space structure on a pointed type

module _
  {l1 l2 : Level} (M : H-Space l1) (N : H-Space l2)
  where

  preserves-mul-pointed-equiv-H-Space :
    (pointed-type-H-Space M ≃∗ pointed-type-H-Space N) → UU (l1 ⊔ l2)
  preserves-mul-pointed-equiv-H-Space e =
    preserves-mul-pointed-map-H-Space M N (pointed-map-pointed-equiv e)

  preserves-left-unit-law-mul-pointed-equiv-H-Space :
    (e : pointed-type-H-Space M ≃∗ pointed-type-H-Space N) →
    preserves-mul-pointed-equiv-H-Space e → UU (l1 ⊔ l2)
  preserves-left-unit-law-mul-pointed-equiv-H-Space e =
    preserves-left-unit-law-mul-pointed-map-H-Space M N
      ( pointed-map-pointed-equiv e)

  preserves-right-unit-law-mul-pointed-equiv-H-Space :
    (e : pointed-type-H-Space M ≃∗ pointed-type-H-Space N) →
    preserves-mul-pointed-equiv-H-Space e → UU (l1 ⊔ l2)
  preserves-right-unit-law-mul-pointed-equiv-H-Space e =
    preserves-right-unit-law-mul-pointed-map-H-Space M N
      ( pointed-map-pointed-equiv e)

  preserves-coherence-unit-laws-mul-pointed-equiv-H-Space :
    (e : pointed-type-H-Space M ≃∗ pointed-type-H-Space N) →
    (μ : preserves-mul-pointed-equiv-H-Space e) →
    (ν : preserves-left-unit-law-mul-pointed-equiv-H-Space e μ) →
    (ρ : preserves-right-unit-law-mul-pointed-equiv-H-Space e μ) → UU l2
  preserves-coherence-unit-laws-mul-pointed-equiv-H-Space e =
    preserves-coherence-unit-laws-mul-pointed-map-H-Space M N
      ( pointed-map-pointed-equiv e)

  preserves-unital-mul-pointed-equiv-H-Space :
    (e : pointed-type-H-Space M ≃∗ pointed-type-H-Space N) →
    UU (l1 ⊔ l2)
  preserves-unital-mul-pointed-equiv-H-Space e =
    preserves-unital-mul-pointed-map-H-Space M N (pointed-map-pointed-equiv e)

Equivalences of H-spaces

module _
  {l1 l2 : Level} (M : H-Space l1) (N : H-Space l2)
  where

  equiv-H-Space : UU (l1 ⊔ l2)
  equiv-H-Space =
    Σ ( pointed-type-H-Space M ≃∗ pointed-type-H-Space N)
      ( preserves-unital-mul-pointed-equiv-H-Space M N)

module _
  {l1 l2 : Level} {M : H-Space l1} {N : H-Space l2} (e : equiv-H-Space M N)
  where

  pointed-equiv-equiv-H-Space : pointed-type-H-Space M ≃∗ pointed-type-H-Space N
  pointed-equiv-equiv-H-Space = pr1 e

  map-equiv-H-Space : type-H-Space M → type-H-Space N
  map-equiv-H-Space = map-pointed-equiv pointed-equiv-equiv-H-Space

  preserves-unit-equiv-H-Space :
    map-equiv-H-Space (unit-H-Space M) ＝ unit-H-Space N
  preserves-unit-equiv-H-Space =
    preserves-point-pointed-equiv pointed-equiv-equiv-H-Space

  preserves-unital-mul-equiv-H-Space :
    preserves-unital-mul-pointed-equiv-H-Space M N pointed-equiv-equiv-H-Space
  preserves-unital-mul-equiv-H-Space = pr2 e

  preserves-mul-equiv-H-Space :
    preserves-mul-pointed-equiv-H-Space M N pointed-equiv-equiv-H-Space
  preserves-mul-equiv-H-Space =
    pr1 preserves-unital-mul-equiv-H-Space

  preserves-left-unit-law-mul-equiv-H-Space :
    preserves-left-unit-law-mul-pointed-equiv-H-Space M N
      ( pointed-equiv-equiv-H-Space)
      ( preserves-mul-equiv-H-Space)
  preserves-left-unit-law-mul-equiv-H-Space =
    pr1 (pr2 preserves-unital-mul-equiv-H-Space)

  preserves-right-unit-law-mul-equiv-H-Space :
    preserves-right-unit-law-mul-pointed-equiv-H-Space M N
      ( pointed-equiv-equiv-H-Space)
      ( preserves-mul-equiv-H-Space)
  preserves-right-unit-law-mul-equiv-H-Space =
    pr1 (pr2 (pr2 preserves-unital-mul-equiv-H-Space))

  preserves-coherence-unit-laws-mul-equiv-H-Space :
    preserves-coherence-unit-laws-mul-pointed-equiv-H-Space M N
      ( pointed-equiv-equiv-H-Space)
      ( preserves-mul-equiv-H-Space)
      ( preserves-left-unit-law-mul-equiv-H-Space)
      ( preserves-right-unit-law-mul-equiv-H-Space)
  preserves-coherence-unit-laws-mul-equiv-H-Space =
    pr2 (pr2 (pr2 preserves-unital-mul-equiv-H-Space))

Recent changes