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≥ 2) are commutative.

Main declarations #

structure EckmannHilton.IsUnital {X : Type u} (m : XXX) (e : X) extends IsLeftId , IsRightId :

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

    Instances For
      theorem EckmannHilton.one {X : Type u} {m₁ : XXX} {m₂ : XXX} {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₁ : XXX} {m₂ : XXX} {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₁ : XXX} {m₂ : XXX} {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)) :

      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₁ : 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)) :

      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.

      def EckmannHilton.addCommMonoid.proof_4 {X : Type u_1} {m₁ : XXX} {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
      Equations
      • (_ : ∀ (a b : X), a + b = b + a) = (_ : ∀ (a b : X), a + b = b + a)
      def EckmannHilton.addCommMonoid.proof_3 {X : Type u_1} [h : AddZeroClass X] :
      ∀ (n : ) (x : X), nsmulRec (n + 1) x = nsmulRec (n + 1) x
      Equations
      • (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x) = (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x)
      def EckmannHilton.addCommMonoid {X : Type u} {m₁ : XXX} {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) :

      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
      def EckmannHilton.addCommMonoid.proof_1 {X : Type u_1} {m₁ : XXX} {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)
      Equations
      • (_ : ∀ (a b c : X), a + b + c = a + (b + c)) = (_ : ∀ (a b c : X), a + b + c = a + (b + c))
      def EckmannHilton.addCommMonoid.proof_2 {X : Type u_1} [h : AddZeroClass X] :
      ∀ (x : X), nsmulRec 0 x = nsmulRec 0 x
      Equations
      • (_ : nsmulRec 0 x = nsmulRec 0 x) = (_ : nsmulRec 0 x = nsmulRec 0 x)
      def EckmannHilton.commMonoid {X : Type u} {m₁ : XXX} {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) :

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

      Equations
      def EckmannHilton.addCommGroup {X : Type u} {m₁ : XXX} {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) :

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

      Equations
      def EckmannHilton.commGroup {X : Type u} {m₁ : XXX} {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) :

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

      Equations