Documentation

Mathlib.GroupTheory.Subgroup.Actions

Actions by Subgroups #

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

Tags #

subgroup, subgroups

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

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.
source
ink
instance Subgroup.instMulActionSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupToMonoidToMonoidToDivInvMonoidToSubmonoid {G : Type u_1} [inst : Group G] {α : Type u_2} [inst : MulAction G α] (S : Subgroup G) :
MulAction { x // x ∈ S } α

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

Equations
source
ink
theorem AddSubgroup.vadd_def {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst : AddAction G α] {S : AddSubgroup G} (g : { x // x ∈ S }) (m : α) :
g +ᵥ m = ↑g +ᵥ m
source
ink
theorem Subgroup.smul_def {G : Type u_1} [inst : Group G] {α : Type u_2} [inst : MulAction G α] {S : Subgroup G} (g : { x // x ∈ S }) (m : α) :
g • m = ↑g • m
source
ink
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
source
ink
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 } α β
Equations
source
ink
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 } α β
Equations
source
ink
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 } β
Equations
source
ink
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
source
ink
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 } β
Equations
source
ink
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.
source
ink
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.
source
ink
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
source
ink
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.
source
ink
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.

Equations
source
ink
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.

Equations