Group actions applied to various types of group #
This file contains lemmas about smul
on group_with_zero
, and group
.
monoid.to_mul_action
is faithful on cancellative monoids.
add_monoid.to_add_action
is faithful on additive cancellative monoids.
Given an action of a group α
on β
, each g : α
defines a permutation of β
.
Given an action of an additive group α
on β
, each g : α
defines a permutation of β
.
add_action.to_perm
is injective on faithful actions.
mul_action.to_perm
is injective on faithful actions.
Given an action of a group α
on a set β
, each g : α
defines a permutation of β
.
Equations
- mul_action.to_perm_hom α β = {to_fun := mul_action.to_perm _inst_2, map_one' := _, map_mul' := _}
Given an action of a additive group α
on a set β
, each g : α
defines a permutation of
β
.
Equations
- add_action.to_perm_hom β α = {to_fun := λ (a : α), ⇑additive.of_mul (add_action.to_perm a), map_zero' := _, map_add' := _}
The tautological action by equiv.perm α
on α
.
This generalizes function.End.apply_mul_action
.
Equations
- equiv.perm.apply_mul_action α = {to_has_smul := {smul := λ (f : equiv.perm α) (a : α), ⇑f a}, one_smul := _, mul_smul := _}
equiv.perm.apply_mul_action
is faithful.
monoid.to_mul_action
is faithful on nontrivial cancellative monoids with zero.
Each element of the group defines an additive monoid isomorphism.
This is a stronger version of mul_action.to_perm
.
Equations
- distrib_mul_action.to_add_equiv β x = {to_fun := (distrib_mul_action.to_add_monoid_hom β x).to_fun, inv_fun := (⇑(mul_action.to_perm_hom α β) x).inv_fun, left_inv := _, right_inv := _, map_add' := _}
Each element of the group defines an additive monoid isomorphism.
This is a stronger version of mul_action.to_perm_hom
.
Equations
- distrib_mul_action.to_add_aut α β = {to_fun := distrib_mul_action.to_add_equiv β _inst_3, map_one' := _, map_mul' := _}
Each element of the group defines a multiplicative monoid isomorphism.
This is a stronger version of mul_action.to_perm
.
Equations
- mul_distrib_mul_action.to_mul_equiv β x = {to_fun := (mul_distrib_mul_action.to_monoid_hom β x).to_fun, inv_fun := (⇑(mul_action.to_perm_hom α β) x).inv_fun, left_inv := _, right_inv := _, map_mul' := _}
Each element of the group defines an multiplicative monoid isomorphism.
This is a stronger version of mul_action.to_perm_hom
.
Equations
- mul_distrib_mul_action.to_mul_aut α β = {to_fun := mul_distrib_mul_action.to_mul_equiv β _inst_3, map_one' := _, map_mul' := _}
If G
acts on A
, then it acts also on A → B
, by (g • F) a = F (g⁻¹ • a)
.
Equations
- arrow_action = {to_has_smul := {smul := λ (g : G) (F : A → B) (a : A), F (g⁻¹ • a)}, one_smul := _, mul_smul := _}
If G
acts on A
, then it acts also on A → B
, by
(g +ᵥ F) a = F (g⁻¹ +ᵥ a)
Equations
- arrow_add_action = {to_has_vadd := {vadd := λ (g : G) (F : A → B) (a : A), F (-g +ᵥ a)}, zero_vadd := _, add_vadd := _}
When B
is a monoid, arrow_action
is additionally a mul_distrib_mul_action
.
Equations
- arrow_mul_distrib_mul_action = {to_mul_action := arrow_action _inst_2, smul_mul := _, smul_one := _}
Given groups G H
with G
acting on A
, G
acts by
multiplicative automorphisms on A → H
.
Equations
- mul_aut_arrow = mul_distrib_mul_action.to_mul_aut G (A → H)