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 #
eckmann_hilton.comm_monoid
: If a type carries two unital binary operations that distribute over each other, then these operations are equal, and form a commutative monoid structure.eckmann_hilton.comm_group
: If a type carries a group structure that distributes over a unital binary operation, then the group is commutative.
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 two unital binary operations that distribute over each other, then these operations are equal, and form a additive commutative monoid structure.
If a type carries two unital binary operations that distribute over each other, then these operations are equal, and form a commutative monoid structure.
If a type carries a group structure that distributes over a unital binary operation, then the group is commutative.
If a type carries an additive group structure that distributes over a unital binary operation, then the additive group is commutative.