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) [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 LinearMap.instOneEnd {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : One (Module.End 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] : Mul (Module.End R M)

Equations

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

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] : Nontrivial (Module.End R M)

Equations

• ⋯ = ⋯

instance Module.End.monoid {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : Monoid (Module.End R M)

Equations

• Module.End.monoid = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

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

Equations

• Module.End.semiring = 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) : (OfNat.ofNat n) m = OfNat.ofNat n • 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 = 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] : IsScalarTower S (Module.End R M) (Module.End 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] : SMulCommClass S (Module.End R M) (Module.End 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] : SMulCommClass (Module.End R M) S (Module.End 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 : ℕ) : 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 : ℕ) : 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 : ℕ) : 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)) : Function.Injective ⇑f'

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

Action by a module endomorphism.

instance LinearMap.applyModule {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : Module (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

• LinearMap.applyModule = Module.mk ⋯ ⋯

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

LinearMap.applyModule is faithful.

Equations

• ⋯ = ⋯

instance LinearMap.apply_smulCommClass {R : Type u_1} {S : Type u_4} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [SMul S M] [IsScalarTower S R M] : SMulCommClass S (Module.End R M) M

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance LinearMap.apply_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] : IsScalarTower S (Module.End R M) 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) : 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.toModuleEnd_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) : (DistribMulAction.toModuleEnd R M) s = DistribMulAction.toLinearMap R M s

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] : 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 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) : (Module.toModuleEnd R M) s = DistribMulAction.toLinearMap R M 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] : S →+* Module.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.moduleEndSelf_apply (R : Type u_1) [Semiring R] (s : Rᵐᵒᵖ) : (Module.moduleEndSelf R) s = DistribMulAction.toLinearMap R R s

@[simp]

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

def Module.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

• Module.moduleEndSelf R = { toFun := DistribMulAction.toLinearMap R R, invFun := fun (f : Module.End R R) => MulOpposite.op (f 1), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

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

@[simp]

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

def Module.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

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

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' := ⋯ }

@[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) : LinearMap.smulRight 0 x = 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} [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' := ⋯ }

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 := fun (g : M →ₗ[R] M₂) => f ∘ₗ g, map_add' := ⋯, map_smul' := ⋯ }

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

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' := ⋯ }

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