MulAction of quotient group on fixed points

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

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