Eckmann-Hilton argument

The Eckmann-Hilton argument says that if a type carries two monoid structures that distribute over one another, then they are equal, and in addition commutative. The main application lies in proving that higher homotopy groups (πₙ for n ≥ 2) are commutative.

Main declarations

eckmann_hilton.comm_monoid: If a type carries two unital binary operations that distribute over each other, then these operations are equal, and form a commutative monoid structure.
eckmann_hilton.comm_group: If a type carries a group structure that distributes over a unital binary operation, then the group is commutative.

source

@[class]

structure eckmann_hilton.is_unital {X : Type u} (m : X → X → X) (e : X) :

Prop

one_mul : ∀ (x : X), m e x = x
mul_one : ∀ (x : X), m x e = x

is_unital m e expresses that e : X is a left and right unit for the binary operation m : X → X → X.

source

theorem eckmann_hilton.group.is_unital {X : Type u} [G : group X] :

eckmann_hilton.is_unital has_mul.mul 1

source

theorem add_group.is_unital {X : Type u} [G : add_group X] :

eckmann_hilton.is_unital has_add.add 0

source

theorem eckmann_hilton.one {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X} (h₁ : eckmann_hilton.is_unital m₁ e₁) (h₂ : eckmann_hilton.is_unital m₂ e₂) (distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :

e₁ = e₂

If a type carries two unital binary operations that distribute over each other, then they have the same unit elements.

In fact, the two operations are the same, and give a commutative monoid structure, see eckmann_hilton.comm_monoid.

source

theorem eckmann_hilton.mul {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X} (h₁ : eckmann_hilton.is_unital m₁ e₁) (h₂ : eckmann_hilton.is_unital m₂ e₂) (distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :

m₁ = m₂

If a type carries two unital binary operations that distribute over each other, then these operations are equal.

In fact, they give a commutative monoid structure, see eckmann_hilton.comm_monoid.

source

theorem eckmann_hilton.mul_comm {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X} (h₁ : eckmann_hilton.is_unital m₁ e₁) (h₂ : eckmann_hilton.is_unital m₂ e₂) (distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :

is_commutative X m₂

If a type carries two unital binary operations that distribute over each other, then these operations are commutative.

In fact, they give a commutative monoid structure, see eckmann_hilton.comm_monoid.

source

theorem eckmann_hilton.mul_assoc {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X} (h₁ : eckmann_hilton.is_unital m₁ e₁) (h₂ : eckmann_hilton.is_unital m₂ e₂) (distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :

is_associative X m₂

If a type carries two unital binary operations that distribute over each other, then these operations are associative.

In fact, they give a commutative monoid structure, see eckmann_hilton.comm_monoid.

source

def eckmann_hilton.add_comm_monoid {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X} (h₁ : eckmann_hilton.is_unital m₁ e₁) (h₂ : eckmann_hilton.is_unital m₂ e₂) (distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :

add_comm_monoid X

If a type carries two unital binary operations that distribute over each other, then these operations are equal, and form a additive commutative monoid structure.

source

def eckmann_hilton.comm_monoid {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X} (h₁ : eckmann_hilton.is_unital m₁ e₁) (h₂ : eckmann_hilton.is_unital m₂ e₂) (distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :

comm_monoid X

If a type carries two unital binary operations that distribute over each other, then these operations are equal, and form a commutative monoid structure.

Equations

eckmann_hilton.comm_monoid h₁ h₂ distrib = {mul := m₂, mul_assoc := _, one := e₂, one_mul := _, mul_one := _, mul_comm := _}

source

def eckmann_hilton.comm_group {X : Type u} {m₁ : X → X → X} {e₁ : X} (h₁ : eckmann_hilton.is_unital m₁ e₁) [G : group X] (distrib : ∀ (a b c d : X), m₁ (a * b) (c * d) = (m₁ a c) * m₁ b d) :

comm_group X

If a type carries a group structure that distributes over a unital binary operation, then the group is commutative.

Equations

eckmann_hilton.comm_group h₁ distrib = {mul := group.mul G, mul_assoc := _, one := group.one G, one_mul := _, mul_one := _, inv := group.inv G, div := group.div G, div_eq_mul_inv := _, mul_left_inv := _, mul_comm := _}

source

def eckmann_hilton.add_comm_group {X : Type u} {m₁ : X → X → X} {e₁ : X} (h₁ : eckmann_hilton.is_unital m₁ e₁) [G : add_group X] (distrib : ∀ (a b c d : X), m₁ (a + b) (c + d) = m₁ a c + m₁ b d) :

add_comm_group X

If a type carries an additive group structure that distributes over a unital binary operation, then the additive group is commutative.