# 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 bundled versions of `(c • ·)` and `(· • ·)` as `AddMonoidHom.smulLeft` and `AddMonoidHom.smul`, respectively.

source
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` #

source
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 := ⋯ }

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

source
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

source
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

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

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

source
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

- AddMonoidHom.smulLeft c = DistribMulAction.toAddMonoidHom A c

Instances For

source
@[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
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`.

Equations

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

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 = AddMonoidHom.smulLeft