Documentation

Mathlib.Algebra.Module.LinearMap.End

Endomorphisms of a module #

In this file we define the type of linear endomorphisms of a module over a ring (Module.End). We set up the basic theory, including the action of Module.End on the module we are considering endomorphisms of.

Main results #

@[reducible, inline]
abbrev Module.End (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] :

Linear endomorphisms of a module, with associated ring structure Module.End.semiring and algebra structure Module.End.algebra.

Equations
Instances For

    Monoid structure of endomorphisms #

    instance LinearMap.instOneEnd {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
    Equations
    • LinearMap.instOneEnd = { one := LinearMap.id }
    instance LinearMap.instMulEnd {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
    Equations
    • LinearMap.instMulEnd = { mul := LinearMap.comp }
    theorem LinearMap.one_eq_id {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
    1 = LinearMap.id
    theorem LinearMap.mul_eq_comp {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) (g : Module.End R M) :
    f * g = f ∘ₗ g
    @[simp]
    theorem LinearMap.one_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
    1 x = x
    @[simp]
    theorem LinearMap.mul_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) (g : Module.End R M) (x : M) :
    (f * g) x = f (g x)
    theorem LinearMap.coe_one {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
    1 = id
    theorem LinearMap.coe_mul {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) (g : Module.End R M) :
    (f * g) = f g
    instance Module.End.instNontrivial {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] :
    Equations
    • =
    instance Module.End.monoid {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
    Equations
    • Module.End.monoid = Monoid.mk npowRec
    instance Module.End.semiring {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
    Equations
    • Module.End.semiring = let __src := AddMonoidWithOne.unary; let __src_1 := Module.End.monoid; let __src_2 := LinearMap.addCommMonoid; Semiring.mk Monoid.npow
    @[simp]
    theorem Module.End.natCast_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (n : ) (m : M) :
    n m = n m

    See also Module.End.natCast_def.

    @[simp]
    theorem Module.End.ofNat_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (n : ) [n.AtLeastTwo] (m : M) :
    instance Module.End.ring {R : Type u_1} {N₁ : Type u_10} [Semiring R] [AddCommGroup N₁] [Module R N₁] :
    Ring (Module.End R N₁)
    Equations
    • Module.End.ring = let __src := Module.End.semiring; let __src_1 := LinearMap.addCommGroup; Ring.mk SubNegMonoid.zsmul
    @[simp]
    theorem Module.End.intCast_apply {R : Type u_1} {N₁ : Type u_10} [Semiring R] [AddCommGroup N₁] [Module R N₁] (z : ) (m : N₁) :
    z m = z m

    See also Module.End.intCast_def.

    instance Module.End.isScalarTower {R : Type u_1} {S : Type u_4} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] :
    Equations
    • =
    instance Module.End.smulCommClass {R : Type u_1} {S : Type u_4} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMul S R] [IsScalarTower S R M] :
    Equations
    • =
    instance Module.End.smulCommClass' {R : Type u_1} {S : Type u_4} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMul S R] [IsScalarTower S R M] :
    Equations
    • =
    theorem Module.End_isUnit_apply_inv_apply_of_isUnit {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f : Module.End R M} (h : IsUnit f) (x : M) :
    f (h.unit.inv x) = x
    theorem Module.End_isUnit_inv_apply_apply_of_isUnit {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f : Module.End R M} (h : IsUnit f) (x : M) :
    h.unit.inv (f x) = x
    theorem LinearMap.coe_pow {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) (n : ) :
    (f ^ n) = (f)^[n]
    theorem LinearMap.pow_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) (n : ) (m : M) :
    (f ^ n) m = (f)^[n] m
    theorem LinearMap.pow_map_zero_of_le {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f : Module.End R M} {m : M} {k : } {l : } (hk : k l) (hm : (f ^ k) m = 0) :
    (f ^ l) m = 0
    theorem LinearMap.commute_pow_left_of_commute {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} {g : Module.End R M} {g₂ : Module.End R₂ M₂} (h : LinearMap.comp g₂ f = f.comp g) (k : ) :
    LinearMap.comp (g₂ ^ k) f = f.comp (g ^ k)
    @[simp]
    theorem LinearMap.id_pow {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (n : ) :
    LinearMap.id ^ n = LinearMap.id
    theorem LinearMap.iterate_succ {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} (n : ) :
    f' ^ (n + 1) = (f' ^ n) ∘ₗ f'
    theorem LinearMap.iterate_surjective {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} (h : Function.Surjective f') (n : ) :
    theorem LinearMap.iterate_injective {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} (h : Function.Injective f') (n : ) :
    theorem LinearMap.iterate_bijective {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} (h : Function.Bijective f') (n : ) :
    theorem LinearMap.injective_of_iterate_injective {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} {n : } (hn : n 0) (h : Function.Injective (f' ^ n)) :
    theorem LinearMap.surjective_of_iterate_surjective {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} {n : } (hn : n 0) (h : Function.Surjective (f' ^ n)) :

    Action by a module endomorphism. #

    instance LinearMap.applyModule {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :

    The tautological action by Module.End R M (aka M →ₗ[R] M) on M.

    This generalizes Function.End.applyMulAction.

    Equations
    @[simp]
    theorem LinearMap.smul_def {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) (a : M) :
    f a = f a
    instance LinearMap.apply_faithfulSMul {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :

    LinearMap.applyModule is faithful.

    Equations
    • =
    instance LinearMap.apply_smulCommClass {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
    Equations
    • =
    instance LinearMap.apply_smulCommClass' {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
    Equations
    • =
    instance LinearMap.apply_isScalarTower {R : Type u_12} {M : Type u_13} [CommSemiring R] [AddCommMonoid M] [Module R M] :
    Equations
    • =

    Actions as module endomorphisms #

    @[simp]
    theorem DistribMulAction.toLinearMap_apply (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) :
    ∀ (a : M), (DistribMulAction.toLinearMap R M s) a = s a
    def DistribMulAction.toLinearMap (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) :

    Each element of the monoid defines a linear map.

    This is a stronger version of DistribMulAction.toAddMonoidHom.

    Equations
    Instances For
      def DistribMulAction.toModuleEnd (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] :

      Each element of the monoid defines a module endomorphism.

      This is a stronger version of DistribMulAction.toAddMonoidEnd.

      Equations
      Instances For
        @[simp]
        theorem Module.toModuleEnd_apply (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [Module S M] [SMulCommClass S R M] (s : S) :
        def Module.toModuleEnd (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [Module S M] [SMulCommClass S R M] :

        Each element of the semiring defines a module endomorphism.

        This is a stronger version of DistribMulAction.toModuleEnd.

        Equations
        Instances For
          @[simp]

          The canonical (semi)ring isomorphism from Rᵐᵒᵖ to Module.End R R induced by the right multiplication.

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

            The canonical (semi)ring isomorphism from R to Module.End Rᵐᵒᵖ R induced by the left multiplication.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem Module.End.natCast_def (R : Type u_1) {N₁ : Type u_10} [Semiring R] (n : ) [AddCommMonoid N₁] [Module R N₁] :
              n = (Module.toModuleEnd R N₁) n
              theorem Module.End.intCast_def (R : Type u_1) {N₁ : Type u_10} [Semiring R] (z : ) [AddCommGroup N₁] [Module R N₁] :
              z = (Module.toModuleEnd R N₁) z
              def LinearMap.smulRight {R : Type u_1} {S : Type u_4} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M] (f : M₁ →ₗ[R] S) (x : M) :
              M₁ →ₗ[R] M

              When f is an R-linear map taking values in S, then fun b ↦ f b • x is an R-linear map.

              Equations
              • f.smulRight x = { toFun := fun (b : M₁) => f b x, map_add' := , map_smul' := }
              Instances For
                @[simp]
                theorem LinearMap.coe_smulRight {R : Type u_1} {S : Type u_4} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M] (f : M₁ →ₗ[R] S) (x : M) :
                (f.smulRight x) = fun (c : M₁) => f c x
                theorem LinearMap.smulRight_apply {R : Type u_1} {S : Type u_4} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M] (f : M₁ →ₗ[R] S) (x : M) (c : M₁) :
                (f.smulRight x) c = f c x
                @[simp]
                theorem LinearMap.smulRight_zero {R : Type u_1} {S : Type u_4} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M] (f : M₁ →ₗ[R] S) :
                f.smulRight 0 = 0
                @[simp]
                theorem LinearMap.zero_smulRight {R : Type u_1} {S : Type u_4} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M] (x : M) :
                @[simp]
                theorem LinearMap.smulRight_apply_eq_zero_iff {R : Type u_1} {S : Type u_4} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M] {f : M₁ →ₗ[R] S} {x : M} [NoZeroSMulDivisors S M] :
                f.smulRight x = 0 f = 0 x = 0
                @[simp]
                theorem LinearMap.applyₗ'_apply_apply {R : Type u_1} (S : Type u_4) {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M₂] [SMulCommClass R S M₂] (v : M) (f : M →ₗ[R] M₂) :
                ((LinearMap.applyₗ' S) v) f = f v
                def LinearMap.applyₗ' {R : Type u_1} (S : Type u_4) {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M₂] [SMulCommClass R S M₂] :
                M →+ (M →ₗ[R] M₂) →ₗ[S] M₂

                Applying a linear map at v : M, seen as S-linear map from M →ₗ[R] M₂ to M₂.

                See LinearMap.applyₗ for a version where S = R.

                Equations
                • LinearMap.applyₗ' S = { toFun := fun (v : M) => { toFun := fun (f : M →ₗ[R] M₂) => f v, map_add' := , map_smul' := }, map_zero' := , map_add' := }
                Instances For
                  def LinearMap.compRight {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M₂ →ₗ[R] M₃) :
                  (M →ₗ[R] M₂) →ₗ[R] M →ₗ[R] M₃

                  Composition by f : M₂ → M₃ is a linear map from the space of linear maps M → M₂ to the space of linear maps M → M₃.

                  Equations
                  • f.compRight = { toFun := f.comp, map_add' := , map_smul' := }
                  Instances For
                    @[simp]
                    theorem LinearMap.compRight_apply {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂) :
                    f.compRight g = f ∘ₗ g
                    @[simp]
                    theorem LinearMap.applyₗ_apply_apply {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (v : M) (f : M →ₗ[R] M₂) :
                    (LinearMap.applyₗ v) f = f v
                    def LinearMap.applyₗ {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                    M →ₗ[R] (M →ₗ[R] M₂) →ₗ[R] M₂

                    Applying a linear map at v : M, seen as a linear map from M →ₗ[R] M₂ to M₂. See also LinearMap.applyₗ' for a version that works with two different semirings.

                    This is the LinearMap version of toAddMonoidHom.eval.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def LinearMap.smulRightₗ {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :
                      (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M

                      The family of linear maps M₂ → M parameterised by f ∈ M₂ → R, x ∈ M, is linear in f, x.

                      Equations
                      • LinearMap.smulRightₗ = { toFun := fun (f : M₂ →ₗ[R] R) => { toFun := f.smulRight, map_add' := , map_smul' := }, map_add' := , map_smul' := }
                      Instances For
                        @[simp]
                        theorem LinearMap.smulRightₗ_apply {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M₂ →ₗ[R] R) (x : M) (c : M₂) :
                        ((LinearMap.smulRightₗ f) x) c = f c x