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 Module.End.instOne {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :
      One (End R M)
      Equations
        instance Module.End.instMul {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :
        Mul (End R M)
        Equations
          theorem Module.End.one_eq_id {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :
          theorem Module.End.mul_eq_comp {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (f g : End R M) :
          f * g = f ∘ₗ g
          @[simp]
          theorem Module.End.one_apply {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
          1 x = x
          @[simp]
          theorem Module.End.mul_apply {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (f g : End R M) (x : M) :
          (f * g) x = f (g x)
          theorem Module.End.coe_one {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :
          1 = id
          theorem Module.End.coe_mul {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (f g : End R M) :
          ⇑(f * g) = f g
          instance Module.End.instNontrivial {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] :
          instance Module.End.instMonoid {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :
          Monoid (End R M)
          Equations
            instance Module.End.instSemiring {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :
            Equations
              @[simp]
              theorem Module.End.natCast_apply {R : Type u_1} {M : Type u_4} [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_4} [Semiring R] [AddCommMonoid M] [Module R M] (n : ) [n.AtLeastTwo] (m : M) :
              instance Module.End.instRing {R : Type u_1} {N₁ : Type u_8} [Semiring R] [AddCommGroup N₁] [Module R N₁] :
              Ring (End R N₁)
              Equations
                @[simp]
                theorem Module.End.intCast_apply {R : Type u_1} {N₁ : Type u_8} [Semiring R] [AddCommGroup N₁] [Module R N₁] (z : ) (m : N₁) :
                z m = z m

                See also Module.End.intCast_def.

                instance Module.End.instIsScalarTower {R : Type u_1} {S : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] :
                IsScalarTower S (End R M) (End R M)
                instance Module.End.instSMulCommClass {R : Type u_1} {S : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMul S R] [IsScalarTower S R M] :
                SMulCommClass S (End R M) (End R M)
                instance Module.End.instSMulCommClass' {R : Type u_1} {S : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMul S R] [IsScalarTower S R M] :
                SMulCommClass (End R M) S (End R M)
                theorem Module.End.isUnit_apply_inv_apply_of_isUnit {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {f : End R M} (h : IsUnit f) (x : M) :
                f (h.unit.inv x) = x
                @[deprecated Module.End.isUnit_apply_inv_apply_of_isUnit (since := "2025-04-28")]
                theorem Module.End_isUnit_apply_inv_apply_of_isUnit {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {f : End R M} (h : IsUnit f) (x : M) :
                f (h.unit.inv x) = x

                Alias of Module.End.isUnit_apply_inv_apply_of_isUnit.

                theorem Module.End.isUnit_inv_apply_apply_of_isUnit {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {f : End R M} (h : IsUnit f) (x : M) :
                h.unit.inv (f x) = x
                @[deprecated Module.End.isUnit_inv_apply_apply_of_isUnit (since := "2025-04-28")]
                theorem Module.End_isUnit_inv_apply_apply_of_isUnit {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {f : End R M} (h : IsUnit f) (x : M) :
                h.unit.inv (f x) = x

                Alias of Module.End.isUnit_inv_apply_apply_of_isUnit.

                theorem Module.End.coe_pow {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (f : End R M) (n : ) :
                ⇑(f ^ n) = (⇑f)^[n]
                theorem Module.End.pow_apply {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (f : End R M) (n : ) (m : M) :
                (f ^ n) m = (⇑f)^[n] m
                theorem Module.End.pow_map_zero_of_le {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {f : End R M} {m : M} {k l : } (hk : k l) (hm : (f ^ k) m = 0) :
                (f ^ l) m = 0
                theorem Module.End.commute_pow_left_of_commute {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} {g : End R M} {g₂ : End R₂ M₂} (h : g₂ ∘ₛₗ f = f ∘ₛₗ g) (k : ) :
                (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
                @[simp]
                theorem Module.End.id_pow {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (n : ) :
                theorem Module.End.iterate_succ {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {f' : End R M} (n : ) :
                f' ^ (n + 1) = (f' ^ n) ∘ₗ f'
                theorem Module.End.iterate_surjective {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {f' : End R M} (h : Function.Surjective f') (n : ) :
                theorem Module.End.iterate_injective {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {f' : End R M} (h : Function.Injective f') (n : ) :
                theorem Module.End.iterate_bijective {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {f' : End R M} (h : Function.Bijective f') (n : ) :
                theorem Module.End.injective_of_iterate_injective {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {f' : End R M} {n : } (hn : n 0) (h : Function.Injective ⇑(f' ^ n)) :
                theorem Module.End.surjective_of_iterate_surjective {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {f' : End R M} {n : } (hn : n 0) (h : Function.Surjective ⇑(f' ^ n)) :

                Action by a module endomorphism. #

                instance Module.End.applyModule {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :
                Module (End R M) M

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

                This generalizes Function.End.applyMulAction.

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

                  LinearMap.applyModule is faithful.

                  instance Module.End.apply_smulCommClass {R : Type u_1} {S : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [SMul S M] [IsScalarTower S R M] :
                  SMulCommClass S (End R M) M
                  instance Module.End.apply_smulCommClass' {R : Type u_1} {S : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [SMul S M] [IsScalarTower S R M] :
                  SMulCommClass (End R M) S M
                  instance Module.End.apply_isScalarTower {R : Type u_1} {S : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] :
                  IsScalarTower S (End R M) M

                  Actions as module endomorphisms #

                  def DistribMulAction.toLinearMap (R : Type u_1) {S : Type u_3} (M : Type u_4) [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
                      @[simp]
                      theorem DistribMulAction.toLinearMap_apply (R : Type u_1) {S : Type u_3} (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) (a✝ : M) :
                      (toLinearMap R M s) a✝ = s a✝
                      def DistribMulAction.toModuleEnd (R : Type u_1) {S : Type u_3} (M : Type u_4) [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 DistribMulAction.toModuleEnd_apply (R : Type u_1) {S : Type u_3} (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) :
                          (toModuleEnd R M) s = toLinearMap R M s
                          def Module.toModuleEnd (R : Type u_1) {S : Type u_3} (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [Module S M] [SMulCommClass S R M] :
                          S →+* End R M

                          Each element of the semiring defines a module endomorphism.

                          This is a stronger version of DistribMulAction.toModuleEnd.

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

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

                              Equations
                                Instances For

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

                                  Equations
                                    Instances For
                                      @[deprecated RingEquiv.moduleEndSelf (since := "2025-04-13")]

                                      Alias of RingEquiv.moduleEndSelf.


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

                                      Equations
                                        Instances For
                                          @[deprecated RingEquiv.moduleEndSelfOp (since := "2025-04-13")]

                                          Alias of RingEquiv.moduleEndSelfOp.


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

                                          Equations
                                            Instances For
                                              theorem Module.End.natCast_def (R : Type u_1) {N₁ : Type u_8} [Semiring R] (n : ) [AddCommMonoid N₁] [Module R N₁] :
                                              n = (toModuleEnd R N₁) n
                                              theorem Module.End.intCast_def (R : Type u_1) {N₁ : Type u_8} [Semiring R] (z : ) [AddCommGroup N₁] [Module R N₁] :
                                              z = (toModuleEnd R N₁) z
                                              def LinearMap.smulRight {R : Type u_1} {S : Type u_3} {M : Type u_4} {M₁ : Type u_5} [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
                                                Instances For
                                                  @[simp]
                                                  theorem LinearMap.coe_smulRight {R : Type u_1} {S : Type u_3} {M : Type u_4} {M₁ : Type u_5} [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_3} {M : Type u_4} {M₁ : Type u_5} [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_3} {M : Type u_4} {M₁ : Type u_5} [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_3} {M : Type u_4} {M₁ : Type u_5} [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) :
                                                  smulRight 0 x = 0
                                                  @[simp]
                                                  theorem LinearMap.smulRight_apply_eq_zero_iff {R : Type u_1} {S : Type u_3} {M : Type u_4} {M₁ : Type u_5} [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
                                                  def LinearMap.applyₗ' {R : Type u_1} (S : Type u_3) {M : Type u_4} {M₂ : Type u_6} [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
                                                    Instances For
                                                      @[simp]
                                                      theorem LinearMap.applyₗ'_apply_apply {R : Type u_1} (S : Type u_3) {M : Type u_4} {M₂ : Type u_6} [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₂) :
                                                      ((applyₗ' S) v) f = f v
                                                      def LinearMap.compRight {R : Type u_1} {M : Type u_4} {M₂ : Type u_6} {M₃ : Type u_7} [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
                                                        Instances For
                                                          @[simp]
                                                          theorem LinearMap.compRight_apply {R : Type u_1} {M : Type u_4} {M₂ : Type u_6} {M₃ : Type u_7} [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₂) :
                                                          def LinearMap.applyₗ {R : Type u_1} {M : Type u_4} {M₂ : Type u_6} [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
                                                            Instances For
                                                              @[simp]
                                                              theorem LinearMap.applyₗ_apply_apply {R : Type u_1} {M : Type u_4} {M₂ : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (v : M) (f : M →ₗ[R] M₂) :
                                                              (applyₗ v) f = f v
                                                              def LinearMap.smulRightₗ {R : Type u_1} {M : Type u_4} {M₂ : Type u_6} [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
                                                                Instances For
                                                                  @[simp]
                                                                  theorem LinearMap.smulRightₗ_apply {R : Type u_1} {M : Type u_4} {M₂ : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M₂ →ₗ[R] R) (x : M) (c : M₂) :
                                                                  ((smulRightₗ f) x) c = f c x
                                                                  theorem Module.End.commute_id_left {R : Type u_9} {M : Type u_10} [Ring R] [AddCommGroup M] [Module R M] (f : End R M) :
                                                                  theorem Module.End.commute_id_right {R : Type u_9} {M : Type u_10} [Ring R] [AddCommGroup M] [Module R M] (f : End R M) :