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 : X → X → X) (e : X) extends Std.LawfulIdentity m e : Prop

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

• left_id (a : X) : m e a = a
• right_id (a : X) : m a e = a

theorem EckmannHilton.MulOneClass.isUnital {X : Type u} [_G : MulOneClass X] : IsUnital (fun (x1 x2 : X) => x1 * x2) 1

theorem EckmannHilton.AddZeroClass.IsUnital {X : Type u} [_G : AddZeroClass X] : EckmannHilton.IsUnital (fun (x1 x2 : X) => x1 + x2) 0

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

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

theorem EckmannHilton.mul_comm {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X} (h₁ : IsUnital m₁ e₁) (h₂ : IsUnital m₂ e₂) (distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) : Std.Commutative 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.CommMonoid.

theorem EckmannHilton.mul_assoc {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X} (h₁ : IsUnital m₁ e₁) (h₂ : IsUnital m₂ e₂) (distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) : Std.Associative 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.CommMonoid.

@[reducible, inline]

abbrev EckmannHilton.commMonoid {X : Type u} {m₁ : X → X → X} {e₁ : X} (h₁ : IsUnital m₁ e₁) [h : MulOneClass X] (distrib : ∀ (a b c d : X), m₁ (a * b) (c * d) = m₁ a c * m₁ b d) : CommMonoid X

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

Equations

• EckmannHilton.commMonoid h₁ distrib = CommMonoid.mk ⋯

@[reducible, inline]

abbrev EckmannHilton.addCommMonoid {X : Type u} {m₁ : X → X → X} {e₁ : X} (h₁ : IsUnital m₁ e₁) [h : AddZeroClass X] (distrib : ∀ (a b c d : X), m₁ (a + b) (c + d) = m₁ a c + m₁ b d) : AddCommMonoid X

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.

Equations

• EckmannHilton.addCommMonoid h₁ distrib = AddCommMonoid.mk ⋯

@[reducible, inline]

abbrev EckmannHilton.commGroup {X : Type u} {m₁ : X → X → X} {e₁ : X} (h₁ : IsUnital m₁ e₁) [G : Group X] (distrib : ∀ (a b c d : X), m₁ (a * b) (c * d) = m₁ a c * m₁ b d) : CommGroup X

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

Equations

• EckmannHilton.commGroup h₁ distrib = CommGroup.mk ⋯

@[reducible, inline]

abbrev EckmannHilton.addCommGroup {X : Type u} {m₁ : X → X → X} {e₁ : X} (h₁ : IsUnital m₁ e₁) [G : AddGroup X] (distrib : ∀ (a b c d : X), m₁ (a + b) (c + d) = m₁ a c + m₁ b d) : AddCommGroup X

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

Equations

• EckmannHilton.addCommGroup h₁ distrib = AddCommGroup.mk ⋯