The Eckmann-Hilton Argument
Content created by Raymond Baker and Egbert Rijke.
Created on 2023-09-24.
Last modified on 2023-11-24.
module synthetic-homotopy-theory.eckmann-hilton-argument where
Imports
open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.interchange-law open import foundation.path-algebra open import foundation.universe-levels open import structured-types.pointed-equivalences open import structured-types.pointed-types open import synthetic-homotopy-theory.double-loop-spaces open import synthetic-homotopy-theory.functoriality-loop-spaces open import synthetic-homotopy-theory.loop-spaces open import synthetic-homotopy-theory.triple-loop-spaces
Idea
There are two classical statements of the Eckmann-Hilton argument. The first
states that a group object in the category of groups is abelian. The second
states that π₂ (X)
is abelian, for any space X
. The former is an algebraic
statement, while the latter is a homotopy theoretic statment. As it turns out,
the two are equivalent. See the following
wikipedia article.
Both these phrasing, however, are about set level structures. Since we have access to untruncated types, it is more natural to prove untruncated analogs of the above two statements. Thus, we will work with the following statement of the Eckmann-Hilton argument:
(α β : Ω² X) → α ∙ β = β ∙ α
For fixed 2-loops, we will call the resulting identification "the Eckmann-Hilton identification". In this file we will give two different constructions of this identification, one that corresponds to the more algebraic statement and one that corresponds to the more homotopy theoretic statement. We will call the constructions themselves "the Eckmann-Hilton argument".
Definitions
Constructing the Eckmann-Hilton identification from the interchange law
The more algebraic argument uses the interchange law
interchange-Ω²
.
The interchange law essentially expresses that
horizontal-concat-Ω²
is a group homomorphism of
vertical-concat-Ω²
in each variable.
outer-eckmann-hilton-interchange-connection-Ω² : {l : Level} {A : UU l} {a : A} (α δ : type-Ω² a) → Id (horizontal-concat-Ω² α δ) (vertical-concat-Ω² α δ) outer-eckmann-hilton-interchange-connection-Ω² α δ = ( z-concat-Id³ (inv right-unit) (inv left-unit)) ∙ ( ( interchange-Ω² α refl refl δ) ∙ ( y-concat-Id³ ( right-unit-law-horizontal-concat-Ω² {α = α}) ( left-unit-law-horizontal-concat-Ω² {α = δ}))) inner-eckmann-hilton-interchange-connection-Ω² : {l : Level} {A : UU l} {a : A} (β γ : type-Ω² a) → Id ( horizontal-concat-Ω² β γ) (vertical-concat-Ω² γ β) inner-eckmann-hilton-interchange-connection-Ω² β γ = ( z-concat-Id³ (inv left-unit) (inv right-unit)) ∙ ( ( interchange-Ω² refl β γ refl) ∙ ( y-concat-Id³ ( left-unit-law-horizontal-concat-Ω² {α = γ}) ( right-unit-law-horizontal-concat-Ω² {α = β}))) eckmann-hilton-interchange-Ω² : {l : Level} {A : UU l} {a : A} (α β : type-Ω² a) → Id (α ∙ β) (β ∙ α) eckmann-hilton-interchange-Ω² α β = ( inv (outer-eckmann-hilton-interchange-connection-Ω² α β)) ∙ ( inner-eckmann-hilton-interchange-connection-Ω² α β) interchange-concat-Ω² : {l : Level} {A : UU l} {a : A} (α β γ δ : type-Ω² a) → ((α ∙ β) ∙ (γ ∙ δ)) = ((α ∙ γ) ∙ (β ∙ δ)) interchange-concat-Ω² = interchange-law-commutative-and-associative ( _∙_) ( eckmann-hilton-interchange-Ω²) ( assoc)
Constructing the Eckmann-Hilton identification using the naturality condition of the operation of whiskering a fixed 2-path by a 1-path
The motivation
Now we give the more homotopy theoretic version of the Eckmann-Hilton argument.
Consider 2-loops α β : Ω² (X , base)
. The more homotopy theoretic
Eckmann-Hilton argument is often depicted as follows:
| α | | refl-Ω² | α | | β | refl-Ω² | | β |
----- = ---------------- = ---------------- = ----
| β | | β | refl-Ω² | | refl-Ω² | α | | α |
The first picture represents the vertical concatination of α
and β
. The
notation | γ | δ |
represents the horizontal concatination of 2-dimensional
identifications γ
and δ
. Then | refl | α |
is just
identification-left-whisk refl-Ω² α
.
The first and last equality come from the unit laws of whiskering. And the
middle equality can be recognized as
path-swap-nat-identification-left-whisk
,
which is the naturality condition of htpy-identification-left-whisk α
applied
to β
.
Since this version of the Eckmann-Hilton argument may seem more complicated than the algbraic version, the reader is entitled to wonder why we bother giving this second version.
This version of the Eckmann-Hilton argument makes more salient the connection
between the Eckmann-Hilton argument and the 2-D descent data of a fibration. For
now, consider the family of based path spaces Id base : X → UU
. A 1-loop l
induces an autoequivalence Ω X ≃ Ω X
given by concatinating on the right by
l
. This is shown in
tr-Id-right
.
A 2-loop s
induces a homotpy id {A = Ω X} ~ id
given by
htpy-identification-left-whisk
.
This claim is shown in TODO (provide link). Thus, the 2-D descent data of
Id base
is (up to equivalence) exactly the homotopy at the heart of this
version of the Eckmann-Hilton argument.
Recall that homotpies of type id ~ id
automatically commute with each other
via
eckmann-hilton-htpy
.
This identification is constructed using the naturality condition of the two
homotopies involved. Thus, in the case of Id base
, we can see a very close
correspondence between the Eckmann-Hilton identification of 2-loops in the base
type X
and the Eckmann-Hilton identification of the homotopies induced by said
2-loops.
Of course Id base
is a special type family. But this idea generalizes
nonetheless. Given a type family B : X → UU
, any 2-loops α β : Ω X
induce
homotopies tr² B α
and tr² B β
of type id {A = B base} ~ id
. Again, these
homotpies automatically commute with each other via their naturality conditions.
Then, the naturality condition that makes α
and β
commute in Ω² X
is sent
by tr³ B
to the naturality condition that makes the induced homotopies
commute. This is recorded in
tr³-htpy-swap-path-swap
.
From this, it is easy to show that "transport preserves the Eckmann-Hilton
identification" by proving that the additional coherence paths in the definition
of eckmann-hilton
and eckmann-hilton-htpy
are compatible.
This connection has important consequences, one of which being the connection between the Eckmann-Hilton argument and the Hopf fibration.
The construction, using left whiskering
module _ {l : Level} {A : Pointed-Type l} where eckmann-hilton-Ω² : (α β : type-Ω² (point-Pointed-Type A)) → α ∙ β = β ∙ α eckmann-hilton-Ω² α β = equational-reasoning_ (α ∙ β) = ( identification-left-whisk refl α) ∙ ( identification-right-whisk β refl) by ( inv ( horizontal-concat-Id² ( left-unit-law-identification-left-whisk-Ω² α) ( right-unit-law-identification-right-whisk-Ω² β))) = ( identification-right-whisk β refl) ∙ ( identification-left-whisk refl α) by ( path-swap-nat-identification-left-whisk α β) = β ∙ α by ( horizontal-concat-Id² ( right-unit-law-identification-right-whisk-Ω² β) ( left-unit-law-identification-left-whisk-Ω² α))
Using right whiskering
There is another natural construction of an Eckmann-Hilton identification along
these lines. If we think of the first construction as "rotating clockwise", this
alternate version "rotates counter-clockwise". In terms of braids, the previous
construction of Eckmann-Hilton braids α
over β
, while this new construction
braids α
under β
. This difference shows up nicely in the type theory. The
first version uses the naturality of the operation of whiskering on the left,
while the second version uses the naturality of the operation of whiskering on
the right. Based on the intution of braiding, we should expect these two version
of the Eckmann-Hilton identification to naturally "undo" each other, which the
do. Thus, we will refer to this alternate construction of Eckmann-Hilton as "the
inverse Eckmann-Hilton argument", and the corresponding identification "the
inverse Eckmann-Hilton identification".
module _ {l : Level} {A : Pointed-Type l} where eckmann-hilton-inverse-Ω² : (α β : type-Ω² (point-Pointed-Type A)) → α ∙ β = β ∙ α eckmann-hilton-inverse-Ω² α β = equational-reasoning_ (α ∙ β) = (identification-right-whisk α refl) ∙ (identification-left-whisk refl β) by ( inv ( horizontal-concat-Id² ( right-unit-law-identification-right-whisk-Ω² α) ( left-unit-law-identification-left-whisk-Ω² β))) = (identification-left-whisk refl β) ∙ (identification-right-whisk α refl) by path-swap-nat-identification-right-whisk α β = β ∙ α by ( horizontal-concat-Id² ( left-unit-law-identification-left-whisk-Ω² β)) ( right-unit-law-identification-right-whisk-Ω² α)
We now prove that this Eckmann-Hilton identification "undoes" the previously
constructed Eckmann-Hilton identification. If we think of braiding α
over β
,
then braiding β
under α
, we should end up with the trivial braid. Thus, we
should have
eckmann-hilton-Ω² α β ∙ eckman-hilton-inverse-Ω² β α = refl
This is equivalent to,
inv eckman-hilton-inverse-Ω² β α = eckmann-hilton-Ω² α β
which is what we prove. Note that the above property is distinct from syllepsis, since it concerns two different construction of the Eckmann-Hilton identification. Further, it works for all 2-loops, not just 3-loops.
module _ {l : Level} {A : Pointed-Type l} where eckmann-hilton-inverse-Ω²-undoes-eckmann-hilton-Ω² : (α β : type-Ω² (point-Pointed-Type A)) → inv (eckmann-hilton-inverse-Ω² β α) = (eckmann-hilton-Ω² α β) eckmann-hilton-inverse-Ω²-undoes-eckmann-hilton-Ω² α β = equational-reasoning_ ( inv (eckmann-hilton-inverse-Ω² β α)) = concat ( inv ( horizontal-concat-Id² ( left-unit-law-identification-left-whisk-Ω² α) ( right-unit-law-identification-right-whisk-Ω² β))) ( _) ( inv ( concat ( inv ( horizontal-concat-Id² ( right-unit-law-identification-right-whisk-Ω² β) ( left-unit-law-identification-left-whisk-Ω² α))) ( _) ( path-swap-nat-identification-right-whisk β α))) by distributive-inv-concat ( concat ( inv ( horizontal-concat-Id² ( right-unit-law-identification-right-whisk-Ω² β) ( left-unit-law-identification-left-whisk-Ω² α))) ( _) ( path-swap-nat-identification-right-whisk β α)) ( horizontal-concat-Id² ( left-unit-law-identification-left-whisk-Ω² α) ( right-unit-law-identification-right-whisk-Ω² β)) = concat ( inv ( horizontal-concat-Id² ( left-unit-law-identification-left-whisk-Ω² α) ( right-unit-law-identification-right-whisk-Ω² β))) ( _) ( concat ( inv (path-swap-nat-identification-right-whisk β α)) ( _) ( inv ( inv ( horizontal-concat-Id² ( right-unit-law-identification-right-whisk-Ω² β) ( left-unit-law-identification-left-whisk-Ω² α))))) by identification-left-whisk ( inv ( horizontal-concat-Id² ( left-unit-law-identification-left-whisk-Ω² α) ( right-unit-law-identification-right-whisk-Ω² β))) ( distributive-inv-concat ( inv ( horizontal-concat-Id² ( right-unit-law-identification-right-whisk-Ω² β) ( left-unit-law-identification-left-whisk-Ω² α))) ( path-swap-nat-identification-right-whisk β α)) = concat ( inv ( horizontal-concat-Id² ( left-unit-law-identification-left-whisk-Ω² α) ( right-unit-law-identification-right-whisk-Ω² β))) ( _) ( concat ( path-swap-nat-identification-left-whisk α β) ( _) ( horizontal-concat-Id² ( right-unit-law-identification-right-whisk-Ω² β) ( left-unit-law-identification-left-whisk-Ω² α))) by identification-left-whisk ( inv ( horizontal-concat-Id² ( left-unit-law-identification-left-whisk-Ω² α) ( right-unit-law-identification-right-whisk-Ω² β))) ( horizontal-concat-Id² ( path-swap-right-undoes-path-swap-left α β) ( inv-inv ( horizontal-concat-Id² ( right-unit-law-identification-right-whisk-Ω² β) ( left-unit-law-identification-left-whisk-Ω² α)))) = eckmann-hilton-Ω² α β by inv ( assoc ( inv ( horizontal-concat-Id² ( left-unit-law-identification-left-whisk-Ω² α) ( right-unit-law-identification-right-whisk-Ω² β))) ( path-swap-nat-identification-left-whisk α β) ( horizontal-concat-Id² ( right-unit-law-identification-right-whisk-Ω² β) ( left-unit-law-identification-left-whisk-Ω² α)))
Properties
We can apply each eckmann-hilton-Ω²
and eckmann-hilton-inverse-Ω²
to a single 2-loop to obtain a 3-loop
module _ {l : Level} {A : UU l} {a : A} (s : type-Ω² a) where 3-loop-eckmann-hilton-Ω² : type-Ω³ a 3-loop-eckmann-hilton-Ω² = map-equiv-pointed-equiv ( pointed-equiv-2-loop-pointed-identity (Ω (A , a)) (s ∙ s)) ( eckmann-hilton-Ω² s s) 3-loop-eckmann-hilton-inverse-Ω² : type-Ω³ a 3-loop-eckmann-hilton-inverse-Ω² = map-equiv-pointed-equiv ( pointed-equiv-2-loop-pointed-identity (Ω (A , a)) (s ∙ s)) ( eckmann-hilton-inverse-Ω² s s)
The above two 3-loops are inverses
module _ {l : Level} {A : UU l} {a : A} (s : type-Ω² a) where Id-inv-3-loop-eckmann-hilton-inverse-Ω²-3-loop-eckmann-hilton-Ω² : inv (3-loop-eckmann-hilton-inverse-Ω² s) = 3-loop-eckmann-hilton-Ω² s Id-inv-3-loop-eckmann-hilton-inverse-Ω²-3-loop-eckmann-hilton-Ω² = concat ( inv ( preserves-inv-map-Ω ( pointed-map-pointed-equiv ( pointed-equiv-loop-pointed-identity (Ω (A , a)) (s ∙ s))) (eckmann-hilton-inverse-Ω² s s))) ( _) ( ap ( map-Ω ( pointed-map-pointed-equiv ( pointed-equiv-loop-pointed-identity (Ω (A , a)) (s ∙ s)))) ( eckmann-hilton-inverse-Ω²-undoes-eckmann-hilton-Ω² s s))
Recent changes
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-09-26. Raymond Baker. The inverse Eckmann-Hilton argument (#798).
- 2023-09-24. Raymond Baker. Refactor Eckmann-Hilton (#788).