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.instSMulMulActionHomId {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ᵈᵐᵃ (α →ₑ[id] β)

Equations

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

instance DomMulAct.instSMulCommClassMulActionHomId {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'ᵈᵐᵃ (α →ₑ[id] β)

Equations

• ⋯ = ⋯

theorem DomMulAct.smul_mulActionHom_apply {M : Type u_1} {α : Type u_2} {N : Type u_3} {β : Type u_4} [SMul M α] [SMul N α] [SMulCommClass M N α] [SMul N β] (c : Mᵈᵐᵃ) (f : α →ₑ[id] β) (a : α) : (c • f) a = f (DomMulAct.mk.symm c • a)

@[simp]

theorem DomMulAct.mk_smul_mulActionHom_apply {M : Type u_1} {α : Type u_2} {N : Type u_3} {β : Type u_4} [SMul M α] [SMul N α] [SMulCommClass M N α] [SMul N β] (c : M) (f : α →ₑ[id] β) (a : α) : (DomMulAct.mk c • f) a = f (c • a)

instance DomMulAct.instMulActionMulActionHomIdOfSMulCommClass {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ᵈᵐᵃ (α →ₑ[id] β)

Equations

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

instance DomMulAct.instSMulDistribMulActionHomId {M : Type u_1} {N : Type u_2} {A : 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

• DomMulAct.instSMulDistribMulActionHomId = { smul := fun (c : Mᵈᵐᵃ) (f : A →+[N] B) => f.comp (SMulCommClass.toDistribMulActionHom N A (DomMulAct.mk.symm c)) }

instance DomMulAct.instSMulCommClassDistribMulActionHomId {M : Type u_1} {N : Type u_2} {A : 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 {M : Type u_1} {N : Type u_2} {A : 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] (c : Mᵈᵐᵃ) (f : A →+[N] B) (a : A) : (c • f) a = f (DomMulAct.mk.symm c • a)

@[simp]

theorem DomMulAct.mk_smul_mulDistribActionHom_apply {M : Type u_1} {N : Type u_2} {A : 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] (c : M) (f : A →+[N] B) (a : A) : (DomMulAct.mk c • f) a = f (c • a)

instance DomMulAct.instMulActionDistribMulActionHomIdOfSMulCommClass {M : Type u_1} {N : Type u_2} {A : 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.instMulActionDistribMulActionHomIdOfSMulCommClass = Function.Injective.mulAction (fun (f : A →+[N] B) => ⇑f) ⋯ ⋯