Documentation

Mathlib.GroupTheory.Subgroup.Actions

Actions by Subgroups #

These are just copies of the definitions about Submonoid starting from Submonoid.mulAction.

Tags #

subgroup, subgroups

instance AddSubgroup.instAddAction {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {S : AddSubgroup G} :
AddAction (S) α

The additive action by an add_subgroup is the action by the underlying AddGroup.

Equations
instance Subgroup.instMulAction {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {S : Subgroup G} :
MulAction (S) α

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

Equations
theorem AddSubgroup.vadd_def {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {S : AddSubgroup G} (g : S) (m : α) :
g +ᵥ m = g +ᵥ m
theorem Subgroup.smul_def {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {S : Subgroup G} (g : S) (m : α) :
g m = g m
@[simp]
theorem AddSubgroup.mk_vadd {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {S : AddSubgroup G} (g : G) (hg : g S) (a : α) :
{ val := g, property := hg } +ᵥ a = g +ᵥ a
@[simp]
theorem Subgroup.mk_smul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {S : Subgroup G} (g : G) (hg : g S) (a : α) :
{ val := g, property := hg } a = g a
instance AddSubgroup.vaddCommClass_left {G : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup G] [AddAction G β] [VAdd α β] [VAddCommClass G α β] (S : AddSubgroup G) :
VAddCommClass (S) α β
Equations
instance Subgroup.smulCommClass_left {G : Type u_1} {α : Type u_2} {β : Type u_3} [Group G] [MulAction G β] [SMul α β] [SMulCommClass G α β] (S : Subgroup G) :
SMulCommClass (S) α β
Equations
instance AddSubgroup.vaddCommClass_right {G : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup G] [VAdd α β] [AddAction G β] [VAddCommClass α G β] (S : AddSubgroup G) :
VAddCommClass α (S) β
Equations
instance Subgroup.smulCommClass_right {G : Type u_1} {α : Type u_2} {β : Type u_3} [Group G] [SMul α β] [MulAction G β] [SMulCommClass α G β] (S : Subgroup G) :
SMulCommClass α (S) β
Equations

Note that this provides IsScalarTower S G G which is needed by smul_mul_assoc.

Equations

The center of a group acts commutatively on that group.

Equations

The center of a group acts commutatively on that group.

Equations