Documentation

Mathlib.Algebra.Module.Hom

Bundled Hom instances for module and multiplicative actions #

This file defines instances for Module, MulAction and related structures on bundled Hom types.

These are analogous to the instances in Algebra.Module.Pi, but for bundled instead of unbundled functions.

We also define bundled versions of (c • ·) and (· • ·) as AddMonoidHom.smulLeft and AddMonoidHom.smul, respectively.

Instances for AddMonoidHom #

instance AddMonoidHom.instDistribSMul {M : Type u_3} {A : Type u_4} {B : Type u_5} [AddZeroClass A] [AddCommMonoid B] [DistribSMul M B] :
Equations
instance AddMonoidHom.instDistribMulAction {R : Type u_1} {A : Type u_4} {B : Type u_5} [Monoid R] [AddMonoid A] [AddCommMonoid B] [DistribMulAction R B] :
Equations
@[simp]
theorem AddMonoidHom.coe_smul {R : Type u_1} {A : Type u_4} {B : Type u_5} [Monoid R] [AddMonoid A] [AddCommMonoid B] [DistribMulAction R B] (r : R) (f : A →+ B) :
(r f) = r f
theorem AddMonoidHom.smul_apply {R : Type u_1} {A : Type u_4} {B : Type u_5} [Monoid R] [AddMonoid A] [AddCommMonoid B] [DistribMulAction R B] (r : R) (f : A →+ B) (x : A) :
(r f) x = r f x
instance AddMonoidHom.smulCommClass {R : Type u_1} {S : Type u_2} {A : Type u_4} {B : Type u_5} [Monoid R] [Monoid S] [AddMonoid A] [AddCommMonoid B] [DistribMulAction R B] [DistribMulAction S B] [SMulCommClass R S B] :
Equations
instance AddMonoidHom.isScalarTower {R : Type u_1} {S : Type u_2} {A : Type u_4} {B : Type u_5} [Monoid R] [Monoid S] [AddMonoid A] [AddCommMonoid B] [DistribMulAction R B] [DistribMulAction S B] [SMul R S] [IsScalarTower R S B] :
Equations
Equations
instance AddMonoidHom.instModule {R : Type u_1} {A : Type u_4} {B : Type u_5} [Semiring R] [AddMonoid A] [AddCommMonoid B] [Module R B] :
Module R (A →+ B)
Equations

Instances for AddMonoid.End #

These are direct copies of the instances above.

Equations
  • AddMonoid.End.instDistribSMul = AddMonoidHom.instDistribSMul
Equations
  • AddMonoid.End.instDistribMulAction = AddMonoidHom.instDistribMulAction
@[simp]
theorem AddMonoid.End.coe_smul {R : Type u_1} {A : Type u_4} [Monoid R] [AddCommMonoid A] [DistribMulAction R A] (r : R) (f : AddMonoid.End A) :
(r f) = r f
theorem AddMonoid.End.smul_apply {R : Type u_1} {A : Type u_4} [Monoid R] [AddCommMonoid A] [DistribMulAction R A] (r : R) (f : AddMonoid.End A) (x : A) :
(r f) x = r f x
instance AddMonoid.End.smulCommClass {R : Type u_1} {S : Type u_2} {A : Type u_4} [Monoid R] [Monoid S] [AddCommMonoid A] [DistribMulAction R A] [DistribMulAction S A] [SMulCommClass R S A] :
Equations
instance AddMonoid.End.isScalarTower {R : Type u_1} {S : Type u_2} {A : Type u_4} [Monoid R] [Monoid S] [AddCommMonoid A] [DistribMulAction R A] [DistribMulAction S A] [SMul R S] [IsScalarTower R S A] :
Equations
instance AddMonoid.End.instModule {R : Type u_1} {A : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] :
Equations
  • AddMonoid.End.instModule = AddMonoidHom.instModule

The tautological action by AddMonoid.End α on α.

This generalizes AddMonoid.End.applyDistribMulAction.

Equations

Miscelaneous morphisms #

@[simp]
theorem AddMonoidHom.smulLeft_apply {M : Type u_3} {A : Type u_4} [Monoid M] [AddMonoid A] [DistribMulAction M A] (c : M) :
(AddMonoidHom.smulLeft c) = fun (x : A) => c x
def AddMonoidHom.smulLeft {M : Type u_3} {A : Type u_4} [Monoid M] [AddMonoid A] [DistribMulAction M A] (c : M) :
A →+ A

Scalar multiplication on the left as an additive monoid homomorphism.

Equations
Instances For
    def AddMonoidHom.smul {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
    R →+ M →+ M

    Scalar multiplication as a biadditive monoid homomorphism. We need M to be commutative to have addition on M →+ M.

    Equations
    Instances For
      @[simp]
      theorem AddMonoidHom.coe_smul' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
      AddMonoidHom.smul = AddMonoidHom.smulLeft