open import 1Lab.Prelude

open import Algebra.Magma.Unital
open import Algebra.Semigroup
open import Algebra.Monoid

module Algebra.Magma.Unital.EckmannHilton where

The Eckmann-Hilton Argument🔗

The Eckmann-Hilton argument shows that two unital magmas on the same carrier type that satisfy a particular interchange law are not only equal to another, but are also commutative and associative.

More precisely, let $(A,e,\star)$ and $(A,e',\star')$ two unital magmas such that $(a \star b) \star' (c \star d) = (a \star' c) \star (b \star' d)$.

module _ {ℓ : _} {A : Type ℓ} {_⋆_ : A → A → A} {_⋆'_ : A → A → A} {e : A} {e' : A}
  (unital-mgm : is-unital-magma e _⋆_) (unital-mgm' : is-unital-magma e' _⋆'_)
  (interchange : (a b c d : A) → (a ⋆ b) ⋆' (c ⋆ d) ≡ (a ⋆' c) ⋆ (b ⋆' d)) where

Then, one can first show that both operations share a unit, i.e. $e = e'$. Notably, this holds because the units can be expanded to products of themselves, which can then be transformed into another by making use of the interchange equation.

  units-equal : e ≡ e'
  units-equal =
    e                        ≡⟨ sym (idl unital-mgm) ⟩≡
    (e ⋆ e)                  ≡⟨ ap₂ _⋆_ (sym (idl unital-mgm')) (sym (idr unital-mgm')) ⟩≡
    ((e' ⋆'  e) ⋆ (e ⋆' e')) ≡⟨ sym (interchange e' e e e') ⟩≡
    ((e' ⋆ e) ⋆' (e ⋆ e'))   ≡⟨ ap₂ _⋆'_ (idr unital-mgm) (idl unital-mgm) ⟩≡
    (e' ⋆' e')               ≡⟨ idl unital-mgm' ⟩≡
    e' ∎

From there on, we are able to derive that one operation is equal to the dual of the other, once again by using the interchange law as well as swapping units whenever needed.

  ⋆-reverse-⋆' : (x y : A) → x ⋆ y ≡ y ⋆' x
  ⋆-reverse-⋆' x y =
    x ⋆ y                 ≡⟨ ap₂ _⋆_ (sym (idl unital-mgm')) (sym (idr unital-mgm')) ⟩≡
    (e' ⋆' x) ⋆ (y ⋆' e') ≡⟨ sym (interchange e' y x e') ⟩≡
    (e' ⋆ y) ⋆' (x ⋆ e')  ≡⟨ ap₂ _⋆'_ (ap (_⋆ y) (sym units-equal)) (ap (x ⋆_) (sym units-equal)) ⟩≡
    (e ⋆ y) ⋆' (x ⋆ e)    ≡⟨ ap₂ _⋆'_ (idl unital-mgm) (idr unital-mgm) ⟩≡
    y ⋆' x ∎

By a similar method, we can show pointwise equality of the two operators.

  operations-equal : (x y : A) → x ⋆ y ≡ x ⋆' y
  operations-equal x y =
    x ⋆ y                 ≡⟨ ap₂ _⋆_ (sym (idr unital-mgm')) (sym (idl unital-mgm')) ⟩≡
    (x ⋆' e') ⋆ (e' ⋆' y) ≡⟨ sym (interchange x e' e' y) ⟩≡
    (x ⋆ e') ⋆' (e' ⋆ y)  ≡⟨ ap₂ _⋆'_ (sym (ap (_⋆_ x) units-equal)) (sym (ap (_⋆ y) units-equal)) ⟩≡
    (x ⋆ e) ⋆' (e ⋆ y)    ≡⟨ ap₂ _⋆'_ (idr unital-mgm) (idl unital-mgm) ⟩≡
    x ⋆' y ∎

These two properties make it rather straightforward to show that $\star$ is commutative - since we know that $a \star b = a \star' b$ as well as $a \star b = b \star' a$, the proof can be completed by simple path concatenation.

  ⋆-commutative : (x y : A) → x ⋆ y ≡ y ⋆ x
  ⋆-commutative x y = ⋆-reverse-⋆' x y ∙ sym (operations-equal y x)

Finally, associativity of the operation can be established by what can be informally described as rotating the elements of the product, using commutativity inside the factors of a products that can then be interchanged and reduced. Thus, associativity combined with the assumed unitality allows us to prove that the operation is a monoid.

  ⋆-associative : (x y z : A) → x ⋆ (y ⋆ z) ≡ (x ⋆ y) ⋆ z
  ⋆-associative x y z = sym (
    (x ⋆ y) ⋆ z         ≡⟨ ap (λ a → (x ⋆ y) ⋆ a) (sym (idr unital-mgm)) ⟩≡
    (x ⋆ y) ⋆ (z ⋆ e)   ≡⟨ ap (λ x → x ⋆ (z ⋆ e)) (⋆-commutative x y) ⟩≡
    (y ⋆ x) ⋆ (z ⋆ e)   ≡⟨ operations-equal (y ⋆ x) (z ⋆ e) ⟩≡
    (y ⋆ x) ⋆' (z ⋆ e)  ≡⟨ interchange y x z e ⟩≡
    (y ⋆' z) ⋆ (x ⋆' e) ≡⟨ ⋆-commutative (y ⋆' z) (x ⋆' e) ⟩≡
    (x ⋆' e) ⋆ (y ⋆' z) ≡⟨ ap₂ _⋆_ (sym (operations-equal x e)) (sym (operations-equal y z)) ⟩≡
    (x ⋆ e) ⋆ (y ⋆ z)   ≡⟨ ap (_⋆ (y ⋆ z)) (idr unital-mgm) ⟩≡
    x ⋆ (y ⋆ z) ∎)

  ⋆-is-monoid : is-monoid e _⋆_
  ⋆-is-monoid .has-is-semigroup .has-is-magma = unital-mgm .has-is-magma
  ⋆-is-monoid .has-is-semigroup .associative = ⋆-associative _ _ _
  ⋆-is-monoid .idl = unital-mgm .idl
  ⋆-is-monoid .idr = unital-mgm .idr