Documentation

Mathlib.Algebra.Module.Hom

Bundled Hom instances for module and multiplicative actions #

This file defines instances for Module on bundled Hom types.

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

We also define a bundled versions of (· • ·) as AddMonoidHom.smul.

source
@[instance_reducible]
instance ZeroHom.instModule {R : Type u_1} {A : Type u_4} {B : Type u_5} [Semiring R] [AddMonoid A] [AddCommMonoid B] [Module R B] :
Module R (ZeroHom A B)

Instances for AddMonoidHom #

source
@[instance_reducible]
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)
source
@[instance_reducible]
instance AddMonoidHom.instDomMulActModule {S : Type u_6} {M : Type u_7} {M₂ : Type u_8} [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module S M] :
Module Sᵈᵐᵃ (M →+ M₂)

Instances for AddMonoid.End #

These are direct copies of the instances above.

source
@[instance_reducible]
instance AddMonoid.End.instDistribSMul {M : Type u_3} {A : Type u_4} [AddCommMonoid A] [DistribSMul M A] :
DistribSMul M (AddMonoid.End A)
source
@[instance_reducible]
instance AddMonoid.End.instDistribMulAction {R : Type u_1} {A : Type u_4} [Monoid R] [AddCommMonoid A] [DistribMulAction R A] :
DistribMulAction R (AddMonoid.End A)
source
@[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
source
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
source
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] :
SMulCommClass R S (AddMonoid.End A)
source
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] :
IsScalarTower R S (AddMonoid.End A)
source
instance AddMonoid.End.isCentralScalar {R : Type u_1} {A : Type u_4} [Monoid R] [AddCommMonoid A] [DistribMulAction R A] [DistribMulAction Rᵐᵒᵖ A] [IsCentralScalar R A] :
IsCentralScalar R (AddMonoid.End A)
source
@[instance_reducible]
instance AddMonoid.End.instModule {R : Type u_1} {A : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] :
Module R (AddMonoid.End A)
source
@[instance_reducible]
instance AddMonoid.End.applyModule {A : Type u_4} [AddCommMonoid A] :
Module (AddMonoid.End A) A

The tautological action by AddMonoid.End α on α.

This generalizes AddMonoid.End.applyDistribMulAction.

Miscellaneous morphisms #

source
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.

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