# Documentation

Mathlib.GroupTheory.GroupAction.DomAct.ActionHom

# Action of Mᵈᵐᵃ on α →[N] β and A →+[N] B#

In this file we define action of DomMulAct M = Mᵈᵐᵃ on α →[N] β and on A →+[N] B. At the time of writing, these homomorphisms are not widely used in the library, so we put these instances into a separate file, not with the definition of DomMulAct.

## TODO #

Add left actions of, e.g., M on α →[N] β to Mathlib.Algebra.Hom.GroupAction and SMulCommClass instances saying that left and right actions commute.

instance DomMulAct.instSMulDomMulActMulActionHom {M : Type u_1} {α : Type u_2} {N : Type u_3} {β : Type u_4} [SMul M α] [SMul N α] [] [SMul N β] :
SMul Mᵈᵐᵃ (α →[N] β)
theorem DomMulAct.smul_mulActionHom_apply {M : Type u_1} {α : Type u_3} {N : Type u_4} {β : Type u_2} [SMul M α] [SMul N α] [] [SMul N β] (c : Mᵈᵐᵃ) (f : α →[N] β) (a : α) :
↑(c f) a = f (DomMulAct.mk.symm c a)
@[simp]
theorem DomMulAct.mk_smul_mulActionHom_apply {M : Type u_4} {α : Type u_2} {N : Type u_3} {β : Type u_1} [SMul M α] [SMul N α] [] [SMul N β] (c : M) (f : α →[N] β) (a : α) :
↑(DomMulAct.mk c f) a = f (c a)
instance DomMulAct.instMulActionDomMulActMulActionHomInstMonoidDomMulActMonoid {M : Type u_1} {α : Type u_2} {N : Type u_3} {β : Type u_4} [] [] [SMul N α] [] [SMul N β] :
instance DomMulAct.instSMulDomMulActDistribMulActionHom {A : Type u_1} {M : Type u_2} {N : Type u_3} {B : Type u_4} [] [] [] [] [] [] [] :
theorem DomMulAct.smul_mulDistribActionHom_apply {A : Type u_3} {M : Type u_1} {N : Type u_4} {B : Type u_2} [] [] [] [] [] [] [] (c : Mᵈᵐᵃ) (f : A →+[N] B) (a : A) :
↑(c f) a = f (DomMulAct.mk.symm c a)
@[simp]
theorem DomMulAct.mk_smul_mulDistribActionHom_apply {A : Type u_2} {M : Type u_4} {N : Type u_3} {B : Type u_1} [] [] [] [] [] [] [] (c : M) (f : A →+[N] B) (a : A) :
↑(DomMulAct.mk c f) a = f (c a)
instance DomMulAct.instMulActionDomMulActDistribMulActionHomInstMonoidDomMulActMonoid {M : Type u_1} {A : Type u_2} {N : Type u_3} {B : Type u_4} [] [] [] [] [] [] [] [] :