EckmannHilton.one
theorem EckmannHilton.one :
∀ {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X},
EckmannHilton.IsUnital m₁ e₁ →
EckmannHilton.IsUnital m₂ e₂ → (∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) → e₁ = e₂
This theorem, named `EckmannHilton.one`, states that if a type has two unital binary operations that distribute over each other, then these operations must have the same unit elements. In other words, for any type `X` and any two operations `m₁` and `m₂` with respective unit elements `e₁` and `e₂`, if `m₁` and `m₂` are both unital and if the operation `m₂` distributes over `m₁` (and vice versa), then `e₁` is equal to `e₂`. This theorem is a key part of the Eckmann-Hilton argument, which is used to show that two structures that interact in a certain way are actually the same, giving rise to a commutative monoid structure.
More concisely: If two unital binary operations on a type distribute over each other, then they have the same unit element.
|
EckmannHilton.mul_comm
theorem EckmannHilton.mul_comm :
∀ {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X},
EckmannHilton.IsUnital m₁ e₁ →
EckmannHilton.IsUnital m₂ e₂ →
(∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) → Std.Commutative m₂
The theorem `EckmannHilton.mul_comm` states that if a type X has two unital binary operations m₁ and m₂, with respective units e₁ and e₂, and if these two operations distribute over each other, then the binary operation m₂ is commutative. In other words, for all a, b, c, d of type X, if m₁ of m₂(a, b) and m₂(c, d) equals m₂ of m₁(a, c) and m₁(b, d), then for any two elements x and y of type X, m₂(x, y) equals m₂(y, x). This theorem is part of the Eckmann-Hilton argument that shows the operations actually form a commutative monoid structure.
More concisely: If two binary operations on a type with units and distributivity over each other are equal when swapping arguments, then they are commutative.
|
EckmannHilton.mul_assoc
theorem EckmannHilton.mul_assoc :
∀ {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X},
EckmannHilton.IsUnital m₁ e₁ →
EckmannHilton.IsUnital m₂ e₂ →
(∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) → Std.Associative m₂
This theorem, often referred to as the Eckmann-Hilton Argument, states that given a type with two unital binary operations that distribute over each other, these operations are associative. More specifically, if a type `X` has two operations `m₁` and `m₂` with respective unital elements `e₁` and `e₂`, such that for all elements `a, b, c, d` in `X`, the operation `m₁` applied to the results of `m₂` on these elements is equal to the operation `m₂` applied to the results of `m₁` on these elements, then the operation `m₂` is associative. This forms the basis of the Eckmann-Hilton argument, which further demonstrates that these operations give a commutative monoid structure.
More concisely: Given two unital binary operations `m₁` and `m₂` on a type `X` with unital elements `e₁` and `e₂` such that `m₁(m₂(a, b), c) = m₂(m₁(a, b), c)` for all `a, b, c` in `X`, then `m₂` is associative.
|
EckmannHilton.mul
theorem EckmannHilton.mul :
∀ {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X},
EckmannHilton.IsUnital m₁ e₁ →
EckmannHilton.IsUnital m₂ e₂ → (∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) → m₁ = m₂
This theorem, named Eckmann Hilton's theorem, states that if a type has two unital binary operations that distribute over each other, then these two operations must be identical. More specifically, for a particular type `X`, if operations `m₁` and `m₂` are unital with unit elements `e₁` and `e₂` respectively, and if these operations distribute over each other for all elements `a, b, c, d` of `X` (i.e., `m₁` of (`m₂` of `a` and `b`) and (`m₂` of `c` and `d`) equals `m₂` of (`m₁` of `a` and `c`) and (`m₁` of `b` and `d`)), then `m₁` equals `m₂`. This theorem also implies that these operations give a commutative monoid structure.
More concisely: If two unital binary operations `m₁` and `m₂` on a type `X` distribute over each other, then they are identical.
|