Documentation

Mathlib.Algebra.Module.Hom

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.

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

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

        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
          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
            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
              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
                @[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
                  Instances For
                    source
                    @[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
                    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 = DistribSMul.toAddMonoidHom M