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.

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)

Equations

• ZeroHom.instModule = { toMulAction := ZeroHom.instMulActionWithZero.toMulAction, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

Instances for AddMonoidHom

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

• AddMonoidHom.instModule = { toDistribMulAction := AddMonoidHom.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

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₂)

Equations

• AddMonoidHom.instDomMulActModule = { toDistribMulAction := DomMulAct.instDistribMulActionAddMonoidHom, add_smul := ⋯, zero_smul := ⋯ }

Instances for AddMonoid.End

These are direct copies of the instances above.

instance AddMonoid.End.instDistribSMul {M : Type u_3} {A : Type u_4} [AddCommMonoid A] [DistribSMul M A] : DistribSMul M (AddMonoid.End A)

Equations

• AddMonoid.End.instDistribSMul = AddMonoidHom.instDistribSMul

instance AddMonoid.End.instDistribMulAction {R : Type u_1} {A : Type u_4} [Monoid R] [AddCommMonoid A] [DistribMulAction R A] : DistribMulAction R (AddMonoid.End A)

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] : SMulCommClass R S (AddMonoid.End A)

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)

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)

instance AddMonoid.End.instModule {R : Type u_1} {A : Type u_4} [Semiring R] [AddCommMonoid A] [Module R A] : Module R (AddMonoid.End A)

Equations

• AddMonoid.End.instModule = AddMonoidHom.instModule

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.

Equations

• AddMonoid.End.applyModule = { toDistribMulAction := AddMonoid.End.applyDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

Miscellaneous morphisms

@[deprecated DistribSMul.toAddMonoidHom (since := "2026-01-07")]

def AddMonoidHom.smulLeft {M : Type u_3} {A : Type u_4} [AddMonoid A] [DistribSMul M A] (c : M) : A →+ A

Scalar multiplication on the left as an additive monoid homomorphism.

See also the linear map version of this Module.End.smulLeft.

Equations

• AddMonoidHom.smulLeft c = DistribSMul.toAddMonoidHom A c

@[simp]

theorem AddMonoidHom.smulLeft_apply {M : Type u_3} {A : Type u_4} [AddMonoid A] [DistribSMul M A] (c : M) : ⇑(AddMonoidHom.smulLeft c) = fun (x : A) => c • x

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

• AddMonoidHom.smul = (Module.toAddMonoidEnd R M).toAddMonoidHom

@[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