Group actions applied to various types of group #
This file contains lemmas about SMul
on GroupWithZero
, and Group
.
AddMonoid.toAddAction
is faithful on additive cancellative monoids.
Monoid.toMulAction
is faithful on cancellative monoids.
Given an action of an additive group α
on β
, each g : α
defines a permutation of β
.
Instances For
Given an action of a group α
on β
, each g : α
defines a permutation of β
.
Instances For
AddAction.toPerm
is injective on faithful actions.
MulAction.toPerm
is injective on faithful actions.
Given an action of a group α
on a set β
, each g : α
defines a permutation of β
.
Instances For
Given an action of an additive group α
on a set β
, each g : α
defines a permutation of
β
.
Instances For
The tautological action by Equiv.Perm α
on α
.
This generalizes Function.End.applyMulAction
.
Equiv.Perm.applyMulAction
is faithful.
Monoid.toMulAction
is faithful on nontrivial cancellative monoids with zero.
Each element of the group defines an additive monoid isomorphism.
This is a stronger version of MulAction.toPerm
.
Instances For
Each element of the group defines an additive monoid isomorphism.
This is a stronger version of MulAction.toPermHom
.
Instances For
Each non-zero element of a GroupWithZero
defines an additive monoid isomorphism of an
AddMonoid
on which it acts distributively.
This is a stronger version of DistribMulAction.toAddMonoidHom
.
Instances For
Each element of the group defines a multiplicative monoid isomorphism.
This is a stronger version of MulAction.toPerm
.
Instances For
Each element of the group defines a multiplicative monoid isomorphism.
This is a stronger version of MulAction.toPermHom
.
Instances For
If G
acts on A
, then it acts also on A → B
, by (g +ᵥ F) a = F (g⁻¹ +ᵥ a)
Instances For
If G
acts on A
, then it acts also on A → B
, by (g • F) a = F (g⁻¹ • a)
.
Instances For
When B
is a monoid, ArrowAction
is additionally a MulDistribMulAction
.