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

• AddSubgroup.instAddAction = inferInstanceAs (AddAction (↥S.toAddSubmonoid) α)

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

• Subgroup.instMulAction = inferInstanceAs (MulAction (↥S.toSubmonoid) α)

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

• (_ : VAddCommClass (↥S) α β) = (_ : VAddCommClass (↥S.toAddSubmonoid) α β)

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

• (_ : SMulCommClass (↥S) α β) = (_ : SMulCommClass (↥S.toSubmonoid) α β)

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

• (_ : VAddCommClass α (↥S) β) = (_ : VAddCommClass α (↥S.toAddSubmonoid) β)

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

• (_ : SMulCommClass α (↥S) β) = (_ : SMulCommClass α (↥S.toSubmonoid) β)

instance Subgroup.instIsScalarTowerSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupSmulToMulOneClassToMonoidToDivInvMonoidToSMulToSubmonoidSmulToSMul {G : Type u_1} {α : Type u_2} {β : Type u_3} [Group G] [SMul α β] [MulAction G α] [MulAction G β] [IsScalarTower G α β] (S : Subgroup G) : IsScalarTower (↥S) α β

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

Equations

• (_ : IsScalarTower (↥S) α β) = (_ : IsScalarTower (↥S.toSubmonoid) α β)

instance Subgroup.instFaithfulSMulSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupSmulToMulOneClassToMonoidToDivInvMonoidToSMulToSubmonoid {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [FaithfulSMul G α] (S : Subgroup G) : FaithfulSMul (↥S) α

Equations

• (_ : FaithfulSMul (↥S) α) = (_ : FaithfulSMul (↥S.toSubmonoid) α)

instance Subgroup.instDistribMulActionSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupToMonoidToMonoidToDivInvMonoidToSubmonoid {G : Type u_1} {α : Type u_2} [Group G] [AddMonoid α] [DistribMulAction G α] (S : Subgroup G) : DistribMulAction (↥S) α

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

Equations

• Subgroup.instDistribMulActionSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupToMonoidToMonoidToDivInvMonoidToSubmonoid S = inferInstanceAs (DistribMulAction (↥S.toSubmonoid) α)

instance Subgroup.instMulDistribMulActionSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupToMonoidToMonoidToDivInvMonoidToSubmonoid {G : Type u_1} {α : Type u_2} [Group G] [Monoid α] [MulDistribMulAction G α] (S : Subgroup G) : MulDistribMulAction (↥S) α

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

Equations

• Subgroup.instMulDistribMulActionSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupToMonoidToMonoidToDivInvMonoidToSubmonoid S = inferInstanceAs (MulDistribMulAction (↥S.toSubmonoid) α)

instance Subgroup.center.smulCommClass_left {G : Type u_1} [Group G] : SMulCommClass (↥(Subgroup.center G)) G G

The center of a group acts commutatively on that group.

Equations

• (_ : SMulCommClass (↥(Subgroup.center G)) G G) = (_ : SMulCommClass (↥(Submonoid.center G)) G G)

instance Subgroup.center.smulCommClass_right {G : Type u_1} [Group G] : SMulCommClass G (↥(Subgroup.center G)) G

The center of a group acts commutatively on that group.

Equations

• (_ : SMulCommClass G (↥(Subgroup.center G)) G) = (_ : SMulCommClass G (↥(Submonoid.center G)) G)