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.

Instances for AddMonoidHom

instance AddMonoidHom.instDistribSMul {M : Type u_3} {A : Type u_4} {B : Type u_5} [AddZeroClass A] [AddCommMonoid B] [DistribSMul M B] : DistribSMul M (A →+ B)

Equations

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

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

Equations

• AddMonoidHom.instDistribMulAction = 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_4} {B : Type u_5} [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_4} {B : Type u_5} [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_4} {B : Type u_5} [Monoid R] [Monoid S] [AddMonoid A] [AddCommMonoid B] [DistribMulAction R B] [DistribMulAction S B] [SMulCommClass R S B] : SMulCommClass R S (A →+ B)

Equations

• (_ : SMulCommClass R S (A →+ B)) = (_ : SMulCommClass R S (A →+ B))

instance AddMonoidHom.isScalarTower {R : Type u_1} {S : Type u_2} {A : Type u_4} {B : Type u_5} [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

• (_ : IsScalarTower R S (A →+ B)) = (_ : IsScalarTower R S (A →+ B))

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

Equations

• (_ : IsCentralScalar R (A →+ B)) = (_ : IsCentralScalar R (A →+ B))

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

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)

Equations

• (_ : SMulCommClass R S (AddMonoid.End A)) = (_ : SMulCommClass R S (A →+ 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)

Equations

• (_ : IsScalarTower R S (AddMonoid.End A)) = (_ : IsScalarTower R S (A →+ 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)

Equations

• (_ : IsCentralScalar R (AddMonoid.End A)) = (_ : IsCentralScalar R (A →+ 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 = Module.mk (_ : ∀ (x x_1 : AddMonoid.End A) (x_2 : A), (x + x_1) • x_2 = (x + x_1) • x_2) (_ : ∀ (x : A), 0 • x = 0 • x)

Miscelaneous morphisms

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

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

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 = RingHom.toAddMonoidHom (Module.toAddMonoidEnd R M)

@[simp]

theorem AddMonoidHom.coe_smul' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : ⇑AddMonoidHom.smul = AddMonoidHom.smulLeft