Actions by subgroups #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
These are just copies of the definitions about submonoid starting from submonoid.mul_action.
Tags #
subgroup, subgroups
@[protected, instance]
def
add_subgroup.add_action
{G : Type u_1}
[add_group G]
{α : Type u_2}
[add_action G α]
(S : add_subgroup G) :
add_action ↥S α
The additive action by an add_subgroup is the action by the underlying add_group.
Equations
@[protected, instance]
def
subgroup.mul_action
{G : Type u_1}
[group G]
{α : Type u_2}
[mul_action G α]
(S : subgroup G) :
mul_action ↥S α
The action by a subgroup is the action by the underlying group.
Equations
theorem
add_subgroup.vadd_def
{G : Type u_1}
[add_group G]
{α : Type u_2}
[add_action G α]
{S : add_subgroup G}
(g : ↥S)
(m : α) :
@[protected, instance]
def
subgroup.smul_comm_class_left
{G : Type u_1}
[group G]
{α : Type u_2}
{β : Type u_3}
[mul_action G β]
[has_smul α β]
[smul_comm_class G α β]
(S : subgroup G) :
smul_comm_class ↥S α β
@[protected, instance]
def
add_subgroup.vadd_comm_class_left
{G : Type u_1}
[add_group G]
{α : Type u_2}
{β : Type u_3}
[add_action G β]
[has_vadd α β]
[vadd_comm_class G α β]
(S : add_subgroup G) :
vadd_comm_class ↥S α β
@[protected, instance]
def
subgroup.smul_comm_class_right
{G : Type u_1}
[group G]
{α : Type u_2}
{β : Type u_3}
[has_smul α β]
[mul_action G β]
[smul_comm_class α G β]
(S : subgroup G) :
smul_comm_class α ↥S β
@[protected, instance]
def
add_subgroup.vadd_comm_class_right
{G : Type u_1}
[add_group G]
{α : Type u_2}
{β : Type u_3}
[has_vadd α β]
[add_action G β]
[vadd_comm_class α G β]
(S : add_subgroup G) :
vadd_comm_class α ↥S β
@[protected, instance]
def
subgroup.is_scalar_tower
{G : Type u_1}
[group G]
{α : Type u_2}
{β : Type u_3}
[has_smul α β]
[mul_action G α]
[mul_action G β]
[is_scalar_tower G α β]
(S : subgroup G) :
is_scalar_tower ↥S α β
Note that this provides is_scalar_tower S G G which is needed by smul_mul_assoc.
@[protected, instance]
def
subgroup.has_faithful_smul
{G : Type u_1}
[group G]
{α : Type u_2}
[mul_action G α]
[has_faithful_smul G α]
(S : subgroup G) :
@[protected, instance]
def
subgroup.distrib_mul_action
{G : Type u_1}
[group G]
{α : Type u_2}
[add_monoid α]
[distrib_mul_action G α]
(S : subgroup G) :
The action by a subgroup is the action by the underlying group.
Equations
@[protected, instance]
def
subgroup.mul_distrib_mul_action
{G : Type u_1}
[group G]
{α : Type u_2}
[monoid α]
[mul_distrib_mul_action G α]
(S : subgroup G) :
The action by a subgroup is the action by the underlying group.
Equations
@[protected, instance]
def
subgroup.center.smul_comm_class_left
{G : Type u_1}
[group G] :
smul_comm_class ↥(subgroup.center G) G G
The center of a group acts commutatively on that group.
@[protected, instance]
def
subgroup.center.smul_comm_class_right
{G : Type u_1}
[group G] :
smul_comm_class G ↥(subgroup.center G) G
The center of a group acts commutatively on that group.