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.instSMulMulActionHomId {M : Type u_1} {α : Type u_2} {N : Type u_3} {β : Type u_4} [SMul M α] [SMul N α] [SMulCommClass M N α] [SMul N β] :
Equations
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' α] :
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 β] :
Equations
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] :
Equations
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] :
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)
Equations