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.instSemiring and Module.End.instRing: 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) [Semiring R] [AddCommMonoid M] [Module R M] : Type v

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

Equations

• Module.End R M = (M →ₗ[R] M)

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

• Module.End.instOne = { one := LinearMap.id }

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

Equations

• Module.End.instMul = { mul := fun (f g : Module.End R M) => f ∘ₗ g }

theorem Module.End.one_eq_id {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] : 1 = LinearMap.id

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] : Nontrivial (End R 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

• Module.End.instMonoid = { toMul := Module.End.instMul, mul_assoc := ⋯, toOne := Module.End.instOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }

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

Equations

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

@[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) : (OfNat.ofNat n) m = OfNat.ofNat n • 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

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

@[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 : ℕ) : LinearMap.id ^ n = LinearMap.id

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 : ℕ) : 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 : ℕ) : 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 : ℕ) : 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)) : Function.Injective ⇑f'

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)) : Function.Surjective ⇑f'

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

• Module.End.applyModule = { smul := fun (x1 : Module.End R M) (x2 : M) => x1 x2, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[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] : FaithfulSMul (End R M) 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) : M →ₗ[R] M

Each element of the monoid defines a linear map.

This is a stronger version of DistribMulAction.toAddMonoidHom.

Equations

• DistribMulAction.toLinearMap R M s = { toFun := HSMul.hSMul s, map_add' := ⋯, map_smul' := ⋯ }

@[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] : S →* Module.End R M

Each element of the monoid defines a module endomorphism.

This is a stronger version of DistribMulAction.toAddMonoidEnd.

Equations

• DistribMulAction.toModuleEnd R M = { toFun := DistribMulAction.toLinearMap R M, map_one' := ⋯, map_mul' := ⋯ }

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

• Module.toModuleEnd R M = { toFun := DistribMulAction.toLinearMap R M, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[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) : (toModuleEnd R M) s = DistribMulAction.toLinearMap R M s

def RingEquiv.moduleEndSelf (R : Type u_1) [Semiring R] : Rᵐᵒᵖ ≃+* Module.End R R

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.

@[simp]

theorem RingEquiv.moduleEndSelf_apply (R : Type u_1) [Semiring R] (s : Rᵐᵒᵖ) : (moduleEndSelf R) s = DistribMulAction.toLinearMap R R s

@[simp]

theorem RingEquiv.moduleEndSelf_symm_apply (R : Type u_1) [Semiring R] (f : Module.End R R) : (moduleEndSelf R).symm f = MulOpposite.op (f 1)

def RingEquiv.moduleEndSelfOp (R : Type u_1) [Semiring R] : R ≃+* Module.End Rᵐᵒᵖ R

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

Equations

• RingEquiv.moduleEndSelfOp R = { toFun := DistribMulAction.toLinearMap Rᵐᵒᵖ R, invFun := fun (f : Module.End Rᵐᵒᵖ R) => f 1, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingEquiv.moduleEndSelfOp_symm_apply (R : Type u_1) [Semiring R] (f : Module.End Rᵐᵒᵖ R) : (moduleEndSelfOp R).symm f = f 1

@[simp]

theorem RingEquiv.moduleEndSelfOp_apply (R : Type u_1) [Semiring R] (s : R) : (moduleEndSelfOp R) s = DistribMulAction.toLinearMap Rᵐᵒᵖ R s

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

def Module.moduleEndSelf (R : Type u_1) [Semiring R] : Rᵐᵒᵖ ≃+* End R R

Alias of RingEquiv.moduleEndSelf.

---

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

Equations

• Module.moduleEndSelf = RingEquiv.moduleEndSelf

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

def Module.moduleEndSelfOp (R : Type u_1) [Semiring R] : R ≃+* End Rᵐᵒᵖ R

Alias of RingEquiv.moduleEndSelfOp.

---

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

Equations

• Module.moduleEndSelfOp = RingEquiv.moduleEndSelfOp

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

• f.smulRight x = { toFun := fun (b : M₁) => f b • x, map_add' := ⋯, map_smul' := ⋯ }

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

• LinearMap.applyₗ' S = { toFun := fun (v : M) => { toFun := fun (f : M →ₗ[R] M₂) => f v, map_add' := ⋯, map_smul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

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

• f.compRight = { toFun := fun (g : M →ₗ[R] M₂) => f ∘ₗ g, map_add' := ⋯, map_smul' := ⋯ }

@[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₂) : f.compRight g = f ∘ₗ g

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

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

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

• LinearMap.smulRightₗ = { toFun := fun (f : M₂ →ₗ[R] R) => { toFun := f.smulRight, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

@[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) : Commute LinearMap.id f

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) : Commute f LinearMap.id