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] : DistribSMul M (A →+ B)

Equations

• AddMonoidHom.distribSMul = DistribSMul.mk (_ : ∀ (x : M) (x_1 x_2 : A →+ B), x • (x_1 + x_2) = x • x_1 + x • x_2)

instance AddMonoidHom.distribMulAction {R : Type u_1} {A : Type u_3} {B : Type u_4} [Monoid R] [AddMonoid A] [AddCommMonoid B] [DistribMulAction R B] : DistribMulAction R (A →+ B)

Equations

• AddMonoidHom.distribMulAction = DistribMulAction.mk (_ : ∀ (a : R), a • 0 = 0) (_ : ∀ (a : R) (b₁ b₂ : A →+ B), a • (b₁ + b₂) = a • b₁ + a • 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] : SMulCommClass R S (A →+ B)

Equations

• @AddMonoidHom.smulCommClass = @AddMonoidHom.smulCommClass.proof_1

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] : IsScalarTower R S (A →+ B)

Equations

• @AddMonoidHom.isScalarTower = @AddMonoidHom.isScalarTower.proof_1

instance AddMonoidHom.isCentralScalar {R : Type u_1} {A : Type u_3} {B : Type u_4} [Monoid R] [AddMonoid A] [AddCommMonoid B] [DistribMulAction R B] [DistribMulAction Rᵐᵒᵖ B] [IsCentralScalar R B] : IsCentralScalar R (A →+ B)

Equations

• @AddMonoidHom.isCentralScalar = @AddMonoidHom.isCentralScalar.proof_1

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

Equations

• AddMonoidHom.smulLeft c = { toZeroHom := { toFun := fun x => c • x, map_zero' := (_ : c • 0 = 0) }, map_add' := (_ : ∀ (b₁ b₂ : A), c • (b₁ + b₂) = c • b₁ + c • b₂) }

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• AddMonoidHom.module = Module.mk (_ : ∀ (x x_1 : R) (x_2 : A →+ B), (x + x_1) • x_2 = x • x_2 + x_1 • x_2) (_ : ∀ (x : A →+ B), 0 • x = 0)