Eckmann-Hilton argument #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
eckmann_hilton.comm_monoid: If a type carries a unital magma structure that distributes over a unital binary operation, then the magma is a commutative monoid.eckmann_hilton.comm_group: If a type carries a group structure that distributes over a unital binary operation, then the group is commutative.
- to_is_left_id : is_left_id X m e
- to_is_right_id : is_right_id X m e
is_unital m e expresses that e : X is a left and right unit
for the binary operation m : X → X → X.
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.comm_monoid.
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.comm_monoid.
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.comm_monoid.
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.comm_monoid.
If a type carries a unital additive magma structure that distributes over a unital binary operations, then the additive magma structure is a commutative additive monoid.
Equations
- eckmann_hilton.add_comm_monoid h₁ distrib = {add := has_add.add (add_zero_class.to_has_add X), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul._default 0 has_add.add add_zero_class.zero_add add_zero_class.add_zero, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
If a type carries a unital magma structure that distributes over a unital binary operations, then the magma structure is a commutative monoid.
Equations
- eckmann_hilton.comm_monoid h₁ distrib = {mul := has_mul.mul (mul_one_class.to_has_mul X), mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow._default 1 has_mul.mul mul_one_class.one_mul mul_one_class.mul_one, npow_zero' := _, npow_succ' := _, mul_comm := _}
If a type carries a group structure that distributes over a unital binary operation, then the group is commutative.
Equations
- eckmann_hilton.comm_group h₁ distrib = {mul := comm_monoid.mul (eckmann_hilton.comm_monoid h₁ distrib), mul_assoc := _, one := comm_monoid.one (eckmann_hilton.comm_monoid h₁ distrib), one_mul := _, mul_one := _, npow := comm_monoid.npow (eckmann_hilton.comm_monoid h₁ distrib), npow_zero' := _, npow_succ' := _, inv := group.inv G, div := group.div G, div_eq_mul_inv := _, zpow := group.zpow G, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
If a type carries an additive group structure that distributes over a unital binary operation, then the additive group is commutative.
Equations
- eckmann_hilton.add_comm_group h₁ distrib = {add := add_comm_monoid.add (eckmann_hilton.add_comm_monoid h₁ distrib), add_assoc := _, zero := add_comm_monoid.zero (eckmann_hilton.add_comm_monoid h₁ distrib), zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (eckmann_hilton.add_comm_monoid h₁ distrib), nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg G, sub := add_group.sub G, sub_eq_add_neg := _, zsmul := add_group.zsmul G, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}