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.

instance AddMonoidHom.distribSMul {A : Type u_3} {B : Type u_4} {M : Type u_5} [AddZeroClass A] [AddCommMonoid B] [DistribSMul M B] :
instance AddMonoidHom.distribMulAction {R : Type u_1} {A : Type u_3} {B : Type u_4} [Monoid R] [AddMonoid A] [AddCommMonoid B] [DistribMulAction R B] :
@[simp]
theorem AddMonoidHom.coe_smul {R : Type u_1} {A : Type u_3} {B : Type u_4} [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_3} {B : Type u_4} [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_3} {B : Type u_4} [Monoid R] [Monoid S] [AddMonoid A] [AddCommMonoid B] [DistribMulAction R B] [DistribMulAction S B] [SMulCommClass R S B] :
instance AddMonoidHom.isScalarTower {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [Monoid S] [AddMonoid A] [AddCommMonoid B] [DistribMulAction R B] [DistribMulAction S B] [SMul R S] [IsScalarTower R S B] :
@[simp]
theorem AddMonoidHom.smulLeft_apply {A : Type u_3} {M : Type u_5} [Monoid M] [AddMonoid A] [DistribMulAction M A] (c : M) :
↑(AddMonoidHom.smulLeft c) = fun x => c x
def AddMonoidHom.smulLeft {A : Type u_3} {M : Type u_5} [Monoid M] [AddMonoid A] [DistribMulAction M A] (c : M) :
A →+ A

Scalar multiplication on the left as an additive monoid homomorphism.

Instances For
    def AddMonoidHom.smul {R : Type u_1} {M : Type u_5} [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.

    Instances For
      @[simp]
      theorem AddMonoidHom.coe_smul' {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
      AddMonoidHom.smul = AddMonoidHom.smulLeft
      instance AddMonoidHom.module {R : Type u_1} {A : Type u_3} {B : Type u_4} [Semiring R] [AddMonoid A] [AddCommMonoid B] [Module R B] :
      Module R (A →+ B)