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 : Prop

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

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

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

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

theorem EckmannHilton.addCommMonoid.proof_4 {X : Type u_1} {m₁ : X → X → X} {e₁ : X} (h₁ : EckmannHilton.IsUnital m₁ e₁) [h : AddZeroClass X] (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

@[reducible]

def EckmannHilton.addCommMonoid {X : Type u} {m₁ : X → X → X} {e₁ : X} (h₁ : EckmannHilton.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 (_ : ∀ (a b : X), a + b = b + a)

theorem EckmannHilton.addCommMonoid.proof_3 {X : Type u_1} [h : AddZeroClass X] : ∀ (n : ℕ) (x : X), nsmulRec (n + 1) x = nsmulRec (n + 1) x

theorem EckmannHilton.addCommMonoid.proof_2 {X : Type u_1} [h : AddZeroClass X] : ∀ (x : X), nsmulRec 0 x = nsmulRec 0 x

theorem EckmannHilton.addCommMonoid.proof_1 {X : Type u_1} {m₁ : X → X → X} {e₁ : X} (h₁ : EckmannHilton.IsUnital m₁ e₁) [h : AddZeroClass X] (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)

@[reducible]

def EckmannHilton.commMonoid {X : Type u} {m₁ : X → X → X} {e₁ : X} (h₁ : EckmannHilton.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 (_ : ∀ (a b : X), a * b = b * a)

theorem EckmannHilton.addCommGroup.proof_1 {X : Type u_1} [G : AddGroup X] (a : X) (b : X) : a - b = a + -b

theorem EckmannHilton.addCommGroup.proof_2 {X : Type u_1} [G : AddGroup X] (a : X) : SubNegMonoid.zsmul 0 a = 0

@[reducible]

def EckmannHilton.addCommGroup {X : Type u} {m₁ : X → X → X} {e₁ : X} (h₁ : EckmannHilton.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 = let src := EckmannHilton.addCommMonoid h₁ distrib; AddCommGroup.mk (_ : ∀ (a b : X), a + b = b + a)

theorem EckmannHilton.addCommGroup.proof_4 {X : Type u_1} [G : AddGroup X] (n : ℕ) (a : X) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a

theorem EckmannHilton.addCommGroup.proof_3 {X : Type u_1} [G : AddGroup X] (n : ℕ) (a : X) : SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a

@[reducible]

def EckmannHilton.commGroup {X : Type u} {m₁ : X → X → X} {e₁ : X} (h₁ : EckmannHilton.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 = let src := EckmannHilton.commMonoid h₁ distrib; CommGroup.mk (_ : ∀ (a b : X), a * b = b * a)