MulAction and MulDistribMulAction of quotient group on fixed points

Given a MulAction/MulDistribMulAction of a group G on A and a normal subgroup H of G, there is a MulAction/MulDistribMulAction of the quotient group G ⧸ H on fixedPoints H A.

@[instance_reducible]

instance MulAction.instQuotientSubgroupElemFixedPointsSubtypeMem {G : Type u_1} [Group G] {A : Type u_2} [MulAction G A] {H : Subgroup G} [H.Normal] : MulAction (G ⧸ H) ↑(fixedPoints (↥H) A)

Equations

• MulAction.instQuotientSubgroupElemFixedPointsSubtypeMem = MulAction.ofEndHom (QuotientGroup.lift H MulAction.toEndHom ⋯)

@[simp]

theorem MulAction.coe_quotient_smul_fixedPoints {G : Type u_1} [Group G] {A : Type u_2} [MulAction G A] {H : Subgroup G} [H.Normal] (g : G) (a : ↑(fixedPoints (↥H) A)) : ↑g • a = g • a

@[simp]

theorem MulAction.quotient_out_smul_fixedPoints {G : Type u_1} [Group G] {A : Type u_2} [MulAction G A] {H : Subgroup G} [H.Normal] (g : G ⧸ H) (a : ↑(fixedPoints (↥H) A)) : Quotient.out g • a = g • a

@[instance_reducible]

instance MulDistribMulAction.instQuotientSubgroupSubtypeMemSubmonoidSubmonoid {G : Type u_1} [Group G] {A : Type u_2} [Monoid A] [MulDistribMulAction G A] {H : Subgroup G} [H.Normal] : MulDistribMulAction (G ⧸ H) ↥(FixedPoints.submonoid (↥H) A)

Equations

• MulDistribMulAction.instQuotientSubgroupSubtypeMemSubmonoidSubmonoid = { toMulAction := inferInstance, smul_one := ⋯, smul_mul := ⋯ }

@[instance_reducible]

instance MulDistribMulAction.instQuotientSubgroupSubtypeMemSubgroup {G : Type u_1} [Group G] {H : Subgroup G} [H.Normal] {α : Type u_3} [Group α] [MulDistribMulAction G α] : MulDistribMulAction (G ⧸ H) ↥(FixedPoints.subgroup (↥H) α)

Equations

• One or more equations did not get rendered due to their size.