Actions by Subgroup
s #
These are just copies of the definitions about Submonoid
starting from Submonoid.mulAction
.
Tags #
subgroup, subgroups
instance
AddSubgroup.instAddActionSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupToAddMonoidToAddMonoidToSubNegAddMonoidToAddSubmonoid
{G : Type u_1}
[inst : AddGroup G]
{α : Type u_2}
[inst : AddAction G α]
(S : AddSubgroup G)
:
The additive action by an add_subgroup is the action by the underlying AddGroup
.
Equations
- One or more equations did not get rendered due to their size.
instance
Subgroup.instMulActionSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupToMonoidToMonoidToDivInvMonoidToSubmonoid
{G : Type u_1}
[inst : Group G]
{α : Type u_2}
[inst : MulAction G α]
(S : Subgroup G)
:
The action by a subgroup is the action by the underlying group.
Equations
- Subgroup.instMulActionSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupToMonoidToMonoidToDivInvMonoidToSubmonoid S = inferInstanceAs (MulAction { x // x ∈ S.toSubmonoid } α)
def
AddSubgroup.vaddCommClass_left.proof_1
{G : Type u_1}
[inst : AddGroup G]
{α : Type u_2}
{β : Type u_3}
[inst : AddAction G β]
[inst : VAdd α β]
[inst : VAddCommClass G α β]
(S : AddSubgroup G)
:
VAddCommClass { x // x ∈ S.toAddSubmonoid } α β
Equations
- (_ : VAddCommClass { x // x ∈ S.toAddSubmonoid } α β) = (_ : VAddCommClass { x // x ∈ S.toAddSubmonoid } α β)
instance
AddSubgroup.vaddCommClass_left
{G : Type u_1}
[inst : AddGroup G]
{α : Type u_2}
{β : Type u_3}
[inst : AddAction G β]
[inst : VAdd α β]
[inst : VAddCommClass G α β]
(S : AddSubgroup G)
:
VAddCommClass { x // x ∈ S } α β
instance
Subgroup.smulCommClass_left
{G : Type u_1}
[inst : Group G]
{α : Type u_2}
{β : Type u_3}
[inst : MulAction G β]
[inst : SMul α β]
[inst : SMulCommClass G α β]
(S : Subgroup G)
:
SMulCommClass { x // x ∈ S } α β
instance
AddSubgroup.vaddCommClass_right
{G : Type u_1}
[inst : AddGroup G]
{α : Type u_2}
{β : Type u_3}
[inst : VAdd α β]
[inst : AddAction G β]
[inst : VAddCommClass α G β]
(S : AddSubgroup G)
:
VAddCommClass α { x // x ∈ S } β
def
AddSubgroup.vaddCommClass_right.proof_1
{G : Type u_1}
[inst : AddGroup G]
{α : Type u_2}
{β : Type u_3}
[inst : VAdd α β]
[inst : AddAction G β]
[inst : VAddCommClass α G β]
(S : AddSubgroup G)
:
VAddCommClass α { x // x ∈ S.toAddSubmonoid } β
Equations
- (_ : VAddCommClass α { x // x ∈ S.toAddSubmonoid } β) = (_ : VAddCommClass α { x // x ∈ S.toAddSubmonoid } β)
instance
Subgroup.smulCommClass_right
{G : Type u_1}
[inst : Group G]
{α : Type u_2}
{β : Type u_3}
[inst : SMul α β]
[inst : MulAction G β]
[inst : SMulCommClass α G β]
(S : Subgroup G)
:
SMulCommClass α { x // x ∈ S } β
instance
Subgroup.instIsScalarTowerSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupSmulToMulOneClassToMonoidToDivInvMonoidToSMulToSubmonoidSmulToSMul
{G : Type u_1}
[inst : Group G]
{α : Type u_2}
{β : Type u_3}
[inst : SMul α β]
[inst : MulAction G α]
[inst : MulAction G β]
[inst : IsScalarTower G α β]
(S : Subgroup G)
:
IsScalarTower { x // x ∈ S } α β
Note that this provides IsScalarTower S G G
which is needed by smul_mul_assoc
.
Equations
- One or more equations did not get rendered due to their size.
instance
Subgroup.instFaithfulSMulSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupSmulToMulOneClassToMonoidToDivInvMonoidToSMulToSubmonoid
{G : Type u_1}
[inst : Group G]
{α : Type u_2}
[inst : MulAction G α]
[inst : FaithfulSMul G α]
(S : Subgroup G)
:
FaithfulSMul { x // x ∈ S } α
Equations
- One or more equations did not get rendered due to their size.
instance
Subgroup.instDistribMulActionSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupToMonoidToMonoidToDivInvMonoidToSubmonoid
{G : Type u_1}
[inst : Group G]
{α : Type u_2}
[inst : AddMonoid α]
[inst : DistribMulAction G α]
(S : Subgroup G)
:
DistribMulAction { x // x ∈ S } α
The action by a subgroup is the action by the underlying group.
Equations
instance
Subgroup.instMulDistribMulActionSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupToMonoidToMonoidToDivInvMonoidToSubmonoid
{G : Type u_1}
[inst : Group G]
{α : Type u_2}
[inst : Monoid α]
[inst : MulDistribMulAction G α]
(S : Subgroup G)
:
MulDistribMulAction { x // x ∈ S } α
The action by a subgroup is the action by the underlying group.
Equations
- One or more equations did not get rendered due to their size.
instance
Subgroup.center.smulCommClass_left
{G : Type u_1}
[inst : 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}
[inst : Group G]
:
SMulCommClass G { x // x ∈ Subgroup.center G } G
The center of a group acts commutatively on that group.