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 α] [SMulCommClass M N α] [SMul N β] : SMul Mᵈᵐᵃ (α →[N] β)

Equations

• DomMulAct.instSMulDomMulActMulActionHom = { smul := fun (c : Mᵈᵐᵃ) (f : α →[N] β) => MulActionHom.comp f (SMulCommClass.toMulActionHom N α (DomMulAct.mk.symm c)) }

instance DomMulAct.instSMulCommClassDomMulActDomMulActMulActionHomInstSMulDomMulActMulActionHomInstSMulDomMulActMulActionHom {M : Type u_1} {α : Type u_2} {N : Type u_3} {β : Type u_4} [SMul M α] [SMul N α] [SMulCommClass M N α] [SMul N β] {M' : Type u_5} [SMul M' α] [SMulCommClass M' N α] [SMulCommClass M M' α] : SMulCommClass Mᵈᵐᵃ M'ᵈᵐᵃ (α →[N] β)

Equations

• ⋯ = ⋯

theorem DomMulAct.smul_mulActionHom_apply {M : Type u_1} {α : Type u_3} {N : Type u_4} {β : Type u_2} [SMul M α] [SMul N α] [SMulCommClass M 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 α] [SMulCommClass M 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} [Monoid M] [MulAction M α] [SMul N α] [SMulCommClass M N α] [SMul N β] : MulAction Mᵈᵐᵃ (α →[N] β)

Equations

• DomMulAct.instMulActionDomMulActMulActionHomInstMonoidDomMulActMonoid = Function.Injective.mulAction (fun (f : α →[N] β) => ⇑f) ⋯ ⋯

instance DomMulAct.instSMulDomMulActDistribMulActionHom {A : Type u_1} {M : Type u_2} {N : Type u_3} {B : Type u_4} [AddMonoid A] [DistribSMul M A] [Monoid N] [AddMonoid B] [DistribMulAction N A] [SMulCommClass M N A] [DistribMulAction N B] : SMul Mᵈᵐᵃ (A →+[N] B)

Equations

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

instance DomMulAct.instSMulCommClassDomMulActDomMulActDistribMulActionHomInstSMulDomMulActDistribMulActionHomInstSMulDomMulActDistribMulActionHom {A : Type u_1} {M : Type u_2} {N : Type u_3} {B : Type u_4} [AddMonoid A] [DistribSMul M A] [Monoid N] [AddMonoid B] [DistribMulAction N A] [SMulCommClass M N A] [DistribMulAction N B] {M' : Type u_5} [DistribSMul M' A] [SMulCommClass M' N A] [SMulCommClass M M' A] : SMulCommClass Mᵈᵐᵃ M'ᵈᵐᵃ (A →+[N] B)

Equations

• ⋯ = ⋯

theorem DomMulAct.smul_mulDistribActionHom_apply {A : Type u_3} {M : Type u_1} {N : Type u_4} {B : Type u_2} [AddMonoid A] [DistribSMul M A] [Monoid N] [AddMonoid B] [DistribMulAction N A] [SMulCommClass M N A] [DistribMulAction N B] (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} [AddMonoid A] [DistribSMul M A] [Monoid N] [AddMonoid B] [DistribMulAction N A] [SMulCommClass M N A] [DistribMulAction N B] (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} [Monoid M] [AddMonoid A] [DistribMulAction M A] [Monoid N] [AddMonoid B] [DistribMulAction N A] [SMulCommClass M N A] [DistribMulAction N B] : MulAction Mᵈᵐᵃ (A →+[N] B)

Equations

• DomMulAct.instMulActionDomMulActDistribMulActionHomInstMonoidDomMulActMonoid = Function.Injective.mulAction (fun (f : A →+[N] B) => ⇑f) ⋯ ⋯