# Group actions on embeddings #

This file provides a MulAction G (α ↪ β) instance that agrees with the MulAction G (α → β) instances defined by Pi.mulAction.

Note that unlike the Pi instance, this requires G to be a group.

instance Function.Embedding.vadd {G : Type u_1} {α : Type u_3} {β : Type u_4} [] [] :
Equations
• Function.Embedding.vadd = { vadd := fun (g : G) (f : α β) => f.trans }
instance Function.Embedding.smul {G : Type u_1} {α : Type u_3} {β : Type u_4} [] [] :
SMul G (α β)
Equations
• Function.Embedding.smul = { smul := fun (g : G) (f : α β) => f.trans }
theorem Function.Embedding.vadd_def {G : Type u_1} {α : Type u_3} {β : Type u_4} [] [] (g : G) (f : α β) :
g +ᵥ f = f.trans
theorem Function.Embedding.smul_def {G : Type u_1} {α : Type u_3} {β : Type u_4} [] [] (g : G) (f : α β) :
g f = f.trans
@[simp]
theorem Function.Embedding.vadd_apply {G : Type u_1} {α : Type u_3} {β : Type u_4} [] [] (g : G) (f : α β) (a : α) :
(g +ᵥ f) a = g +ᵥ f a
@[simp]
theorem Function.Embedding.smul_apply {G : Type u_1} {α : Type u_3} {β : Type u_4} [] [] (g : G) (f : α β) (a : α) :
(g f) a = g f a
theorem Function.Embedding.coe_vadd {G : Type u_1} {α : Type u_3} {β : Type u_4} [] [] (g : G) (f : α β) :
(g +ᵥ f) = g +ᵥ f
theorem Function.Embedding.coe_smul {G : Type u_1} {α : Type u_3} {β : Type u_4} [] [] (g : G) (f : α β) :
(g f) = g f
instance Function.Embedding.instIsScalarTower {G : Type u_1} {G' : Type u_2} {α : Type u_3} {β : Type u_4} [] [Group G'] [SMul G G'] [] [MulAction G' β] [IsScalarTower G G' β] :
IsScalarTower G G' (α β)
Equations
• =
instance Function.Embedding.instVAddCommClass {G : Type u_1} {G' : Type u_2} {α : Type u_3} {β : Type u_4} [] [AddGroup G'] [] [AddAction G' β] [VAddCommClass G G' β] :
Equations
• =
instance Function.Embedding.instSMulCommClass {G : Type u_1} {G' : Type u_2} {α : Type u_3} {β : Type u_4} [] [Group G'] [] [MulAction G' β] [SMulCommClass G G' β] :
SMulCommClass G G' (α β)
Equations
• =
instance Function.Embedding.instIsCentralScalar {G : Type u_1} {α : Type u_3} {β : Type u_4} [] [] [] [] :
Equations
• =
theorem Function.Embedding.instAddAction.proof_1 {α : Type u_1} {β : Type u_2} :
Function.Injective fun (f : α β) => f
instance Function.Embedding.instAddAction {G : Type u_1} {α : Type u_3} {β : Type u_4} [] [] :