Actions by Subgroups

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

Tags

subgroup, subgroups

instance AddSubgroup.instAddActionSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupToAddMonoidToAddMonoidToSubNegAddMonoidToAddSubmonoid {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] (S : AddSubgroup G) : AddAction { x // x ∈ S } α

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

instance Subgroup.instMulActionSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupToMonoidToMonoidToDivInvMonoidToSubmonoid {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] (S : Subgroup G) : MulAction { x // x ∈ S } α

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

theorem AddSubgroup.vadd_def {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {S : AddSubgroup G} (g : { x // x ∈ S }) (m : α) : g +ᵥ m = ↑g +ᵥ m

theorem Subgroup.smul_def {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {S : Subgroup G} (g : { x // x ∈ S }) (m : α) : g • m = ↑g • m

theorem AddSubgroup.vaddCommClass_left.proof_1 {G : Type u_1} [AddGroup G] {α : Type u_2} {β : Type u_3} [AddAction G β] [VAdd α β] [VAddCommClass G α β] (S : AddSubgroup G) : VAddCommClass { x // x ∈ S.toAddSubmonoid } α β

instance AddSubgroup.vaddCommClass_left {G : Type u_1} [AddGroup G] {α : Type u_2} {β : Type u_3} [AddAction G β] [VAdd α β] [VAddCommClass G α β] (S : AddSubgroup G) : VAddCommClass { x // x ∈ S } α β

instance Subgroup.smulCommClass_left {G : Type u_1} [Group G] {α : Type u_2} {β : Type u_3} [MulAction G β] [SMul α β] [SMulCommClass G α β] (S : Subgroup G) : SMulCommClass { x // x ∈ S } α β

instance AddSubgroup.vaddCommClass_right {G : Type u_1} [AddGroup G] {α : Type u_2} {β : Type u_3} [VAdd α β] [AddAction G β] [VAddCommClass α G β] (S : AddSubgroup G) : VAddCommClass α { x // x ∈ S } β

theorem AddSubgroup.vaddCommClass_right.proof_1 {G : Type u_1} [AddGroup G] {α : Type u_2} {β : Type u_3} [VAdd α β] [AddAction G β] [VAddCommClass α G β] (S : AddSubgroup G) : VAddCommClass α { x // x ∈ S.toAddSubmonoid } β

instance Subgroup.smulCommClass_right {G : Type u_1} [Group G] {α : Type u_2} {β : Type u_3} [SMul α β] [MulAction G β] [SMulCommClass α G β] (S : Subgroup G) : SMulCommClass α { x // x ∈ S } β

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

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

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

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

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

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

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

instance Subgroup.center.smulCommClass_left {G : Type u_1} [Group G] : SMulCommClass { x // x ∈ Subgroup.center G } G G

The center of a group acts commutatively on that group.

instance Subgroup.center.smulCommClass_right {G : Type u_1} [Group G] : SMulCommClass G { x // x ∈ Subgroup.center G } G

The center of a group acts commutatively on that group.