mathlib3 documentation

group_theory.subgroup.actions

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) :

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) :

The action by a subgroup is the action by the underlying group.

Equations
theorem subgroup.smul_def {G : Type u_1} [group G] {α : Type u_2} [mul_action G α] {S : subgroup G} (g : S) (m : α) :
g m = g m
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 : α) :
g +ᵥ m = g +ᵥ 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) :
@[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) :
@[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) :
@[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) :
@[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) :

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]

The action by a subgroup is the action by the underlying group.

Equations
@[protected, instance]

The center of a group acts commutatively on that group.

@[protected, instance]

The center of a group acts commutatively on that group.