# Documentation

Mathlib.GroupTheory.EckmannHilton

# 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 #

• EckmannHilton.commMonoid: If a type carries a unital magma structure that distributes over a unital binary operation, then the magma is a commutative monoid.
• EckmannHilton.commGroup: If a type carries a group structure that distributes over a unital binary operation, then the group is commutative.
structure EckmannHilton.IsUnital {X : Type u} (m : XXX) (e : X) extends , :

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

Instances For
theorem EckmannHilton.AddZeroClass.IsUnital {X : Type u} [_G : ] :
EckmannHilton.IsUnital (fun x x_1 => x + x_1) 0
theorem EckmannHilton.MulOneClass.isUnital {X : Type u} [_G : ] :
EckmannHilton.IsUnital (fun x x_1 => x * x_1) 1
theorem EckmannHilton.one {X : Type u} {m₁ : XXX} {m₂ : XXX} {e₁ : X} {e₂ : X} (h₁ : ) (h₂ : ) (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.CommMonoid.

theorem EckmannHilton.mul {X : Type u} {m₁ : XXX} {m₂ : XXX} {e₁ : X} {e₂ : X} (h₁ : ) (h₂ : ) (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.CommMonoid.

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

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.CommMonoid.

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

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.CommMonoid.

theorem EckmannHilton.addCommMonoid.proof_4 {X : Type u_1} {m₁ : XXX} {e₁ : X} (h₁ : ) [h : ] (distrib : ∀ (a b c d : X), m₁ (a + b) (c + d) = m₁ a c + m₁ b d) (a : X) (b : X) :
a + b = b + a
theorem EckmannHilton.addCommMonoid.proof_3 {X : Type u_1} [h : ] :
∀ (n : ) (x : X), nsmulRec (n + 1) x = nsmulRec (n + 1) x
@[reducible]
def EckmannHilton.addCommMonoid {X : Type u} {m₁ : XXX} {e₁ : X} (h₁ : ) [h : ] (distrib : ∀ (a b c d : X), m₁ (a + b) (c + d) = m₁ a c + m₁ b d) :

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

Instances For
theorem EckmannHilton.addCommMonoid.proof_1 {X : Type u_1} {m₁ : XXX} {e₁ : X} (h₁ : ) [h : ] (distrib : ∀ (a b c d : X), m₁ (a + b) (c + d) = m₁ a c + m₁ b d) (a : X) (b : X) (c : X) :
a + b + c = a + (b + c)
theorem EckmannHilton.addCommMonoid.proof_2 {X : Type u_1} [h : ] :
∀ (x : X), nsmulRec 0 x = nsmulRec 0 x
@[reducible]
def EckmannHilton.commMonoid {X : Type u} {m₁ : XXX} {e₁ : X} (h₁ : ) [h : ] (distrib : ∀ (a b c d : X), m₁ (a * b) (c * d) = m₁ a c * m₁ b d) :

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

Instances For
@[reducible]
def EckmannHilton.addCommGroup {X : Type u} {m₁ : XXX} {e₁ : X} (h₁ : ) [G : ] (distrib : ∀ (a b c d : X), m₁ (a + b) (c + d) = m₁ a c + m₁ b d) :

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

Instances For
@[reducible]
def EckmannHilton.commGroup {X : Type u} {m₁ : XXX} {e₁ : X} (h₁ : ) [G : ] (distrib : ∀ (a b c d : X), m₁ (a * b) (c * d) = m₁ a c * m₁ b d) :

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

Instances For