HepLean Documentation

Mathlib.Algebra.Module.Hom

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 #

source
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
source
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
source
@[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
source
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
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
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
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 = Module.mk ⋯ ⋯

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)
Equations
  • ⋯ = ⋯
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)
Equations
  • ⋯ = ⋯
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)
Equations
  • ⋯ = ⋯
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

Miscellaneous morphisms #

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.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
Instances For
    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
    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