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

• Module.End.semiring and Module.End.ring: the (semi)ring of endomorphisms formed by taking the additive structure above with composition as multiplication.
@[reducible, inline]
abbrev Module.End (R : Type u) (M : Type v) [] [] [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} [] [] [Module R M] :
One ()
Equations
• LinearMap.instOneEnd = { one := LinearMap.id }
instance LinearMap.instMulEnd {R : Type u_1} {M : Type u_5} [] [] [Module R M] :
Mul ()
Equations
• LinearMap.instMulEnd = { mul := LinearMap.comp }
theorem LinearMap.one_eq_id {R : Type u_1} {M : Type u_5} [] [] [Module R M] :
1 = LinearMap.id
theorem LinearMap.mul_eq_comp {R : Type u_1} {M : Type u_5} [] [] [Module R M] (f : ) (g : ) :
f * g = f ∘ₗ g
@[simp]
theorem LinearMap.one_apply {R : Type u_1} {M : Type u_5} [] [] [Module R M] (x : M) :
1 x = x
@[simp]
theorem LinearMap.mul_apply {R : Type u_1} {M : Type u_5} [] [] [Module R M] (f : ) (g : ) (x : M) :
(f * g) x = f (g x)
theorem LinearMap.coe_one {R : Type u_1} {M : Type u_5} [] [] [Module R M] :
1 = id
theorem LinearMap.coe_mul {R : Type u_1} {M : Type u_5} [] [] [Module R M] (f : ) (g : ) :
(f * g) = f g
instance Module.End.instNontrivial {R : Type u_1} {M : Type u_5} [] [] [Module R M] [] :
Equations
• =
instance Module.End.monoid {R : Type u_1} {M : Type u_5} [] [] [Module R M] :
Equations
• Module.End.monoid = Monoid.mk npowRec
instance Module.End.semiring {R : Type u_1} {M : Type u_5} [] [] [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} [] [] [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} [] [] [Module R M] (n : ) [n.AtLeastTwo] (m : M) :
() m = m
instance Module.End.ring {R : Type u_1} {N₁ : Type u_10} [] [] [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} [] [] [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} [] [] [Module R M] [] [] [] :
Equations
• =
instance Module.End.smulCommClass {R : Type u_1} {S : Type u_4} {M : Type u_5} [] [] [Module R M] [] [] [] [SMul S R] [] :
Equations
• =
instance Module.End.smulCommClass' {R : Type u_1} {S : Type u_4} {M : Type u_5} [] [] [Module R M] [] [] [] [SMul S R] [] :
Equations
• =
theorem Module.End_isUnit_apply_inv_apply_of_isUnit {R : Type u_1} {M : Type u_5} [] [] [Module R M] {f : } (h : ) (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} [] [] [Module R M] {f : } (h : ) (x : M) :
h.unit.inv (f x) = x
theorem LinearMap.coe_pow {R : Type u_1} {M : Type u_5} [] [] [Module R M] (f : M →ₗ[R] M) (n : ) :
(f ^ n) = (f)^[n]
theorem LinearMap.pow_apply {R : Type u_1} {M : Type u_5} [] [] [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} [] [] [Module R M] {f : } {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} [] [] [Module R M] [Semiring R₂] [] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} {g : } {g₂ : Module.End R₂ M₂} (h : = 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} [] [] [Module R M] (n : ) :
LinearMap.id ^ n = LinearMap.id
theorem LinearMap.iterate_succ {R : Type u_1} {M : Type u_5} [] [] [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} [] [] [Module R M] {f' : M →ₗ[R] M} (h : ) (n : ) :
theorem LinearMap.iterate_injective {R : Type u_1} {M : Type u_5} [] [] [Module R M] {f' : M →ₗ[R] M} (h : ) (n : ) :
theorem LinearMap.iterate_bijective {R : Type u_1} {M : Type u_5} [] [] [Module R M] {f' : M →ₗ[R] M} (h : ) (n : ) :
theorem LinearMap.injective_of_iterate_injective {R : Type u_1} {M : Type u_5} [] [] [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} [] [] [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} [] [] [Module R M] :
Module () M

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

This generalizes Function.End.applyMulAction.

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

LinearMap.applyModule is faithful.

Equations
• =
instance LinearMap.apply_smulCommClass {R : Type u_1} {M : Type u_5} [] [] [Module R M] :
Equations
• =
instance LinearMap.apply_smulCommClass' {R : Type u_1} {M : Type u_5} [] [] [Module R M] :
Equations
• =
instance LinearMap.apply_isScalarTower {R : Type u_12} {M : Type u_13} [] [] [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) [] [] [Module R M] [] [] [] (s : S) :
∀ (a : M), () a = s a
def DistribMulAction.toLinearMap (R : Type u_1) {S : Type u_4} (M : Type u_5) [] [] [Module R M] [] [] [] (s : S) :

Each element of the monoid defines a linear map.

This is a stronger version of DistribMulAction.toAddMonoidHom.

Equations
• = { toFun := , map_add' := , map_smul' := }
Instances For
@[simp]
theorem DistribMulAction.toModuleEnd_apply (R : Type u_1) {S : Type u_4} (M : Type u_5) [] [] [Module R M] [] [] [] (s : S) :
def DistribMulAction.toModuleEnd (R : Type u_1) {S : Type u_4} (M : Type u_5) [] [] [Module R M] [] [] [] :
S →*

Each element of the monoid defines a module endomorphism.

This is a stronger version of DistribMulAction.toAddMonoidEnd.

Equations
• = { toFun := , map_one' := , map_mul' := }
Instances For
@[simp]
theorem Module.toModuleEnd_apply (R : Type u_1) {S : Type u_4} (M : Type u_5) [] [] [Module R M] [] [Module S M] [] (s : S) :
() s =
def Module.toModuleEnd (R : Type u_1) {S : Type u_4} (M : Type u_5) [] [] [Module R M] [] [Module S M] [] :

Each element of the semiring defines a module endomorphism.

This is a stronger version of DistribMulAction.toModuleEnd.

Equations
• = let __src := ; { toFun := , map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem Module.moduleEndSelf_apply (R : Type u_1) [] (s : Rᵐᵒᵖ) :
@[simp]
theorem Module.moduleEndSelf_symm_apply (R : Type u_1) [] (f : ) :
.symm f = MulOpposite.op (f 1)

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
@[simp]
theorem Module.moduleEndSelfOp_apply (R : Type u_1) [] (s : R) :
@[simp]
theorem Module.moduleEndSelfOp_symm_apply (R : Type u_1) [] (f : ) :
.symm f = f 1
def Module.moduleEndSelfOp (R : Type u_1) [] :

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} [] (n : ) [] [Module R N₁] :
n = () n
theorem Module.End.intCast_def (R : Type u_1) {N₁ : Type u_10} [] (z : ) [] [Module R N₁] :
z = () z
def LinearMap.smulRight {R : Type u_1} {S : Type u_4} {M : Type u_5} {M₁ : Type u_6} [] [] [] [Module R M] [Module R M₁] [] [Module R S] [Module 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} [] [] [] [Module R M] [Module R M₁] [] [Module R S] [Module 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} [] [] [] [Module R M] [Module R M₁] [] [Module R S] [Module 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} [] [] [] [Module R M] [Module R M₁] [] [Module R S] [Module 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} [] [] [] [Module R M] [Module R M₁] [] [Module R S] [Module S M] [] (x : M) :
= 0
@[simp]
theorem LinearMap.smulRight_apply_eq_zero_iff {R : Type u_1} {S : Type u_4} {M : Type u_5} {M₁ : Type u_6} [] [] [] [Module R M] [Module R M₁] [] [Module R S] [Module S M] [] {f : M₁ →ₗ[R] S} {x : 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} [] [] [] [] [Module R M] [Module R M₂] [Module S M₂] [SMulCommClass R S M₂] (v : M) (f : M →ₗ[R] M₂) :
( v) f = f v
def LinearMap.applyₗ' {R : Type u_1} (S : Type u_4) {M : Type u_5} {M₂ : Type u_7} [] [] [] [] [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
• = { 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} [] [] [] [] [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} [] [] [] [] [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} [] [] [] [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} [] [] [] [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} [] [] [] [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} [] [] [] [Module R M] [Module R M₂] (f : M₂ →ₗ[R] R) (x : M) (c : M₂) :
((LinearMap.smulRightₗ f) x) c = f c x