Mathlib.Algebra.Module.LinearMap.End

Module.End abbrev

(R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M]

Full source

/-- Linear endomorphisms of a module, with associated ring structure
`Module.End.semiring` and algebra structure `Module.End.algebra`. -/
abbrev Module.End (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] :=
  M →ₗ[R] M

Ring of Linear Endomorphisms of an $R$-Module

Informal description

Given a semiring $R$ and an $R$-module $M$ (where $M$ is an additive commutative monoid equipped with a scalar multiplication operation satisfying the module axioms), the type $\text{End}_R(M)$ denotes the collection of all $R$-linear endomorphisms of $M$. These are linear maps $f \colon M \to M$ that preserve both the additive structure and scalar multiplication, i.e., for all $x, y \in M$ and $r \in R$, we have: 1. $f(x + y) = f(x) + f(y)$ 2. $f(r \cdot x) = r \cdot f(x)$ This type forms a ring under pointwise addition and composition of maps, with the additive identity being the zero map and the multiplicative identity being the identity map on $M$.

Module.End.instOne instance

: One (Module.End R M)

Full source

instance : One (Module.End R M) := ⟨LinearMap.id⟩

Identity Endomorphism as the One Element in the Endomorphism Ring

Informal description

For any semiring $R$ and $R$-module $M$, the ring of linear endomorphisms $\text{End}_R(M)$ has a multiplicative identity given by the identity linear map $\text{id}: M \to M$.

Module.End.instMul instance

: Mul (Module.End R M)

Full source

instance : Mul (Module.End R M) := ⟨fun f g => LinearMap.comp f g⟩

Multiplication in the Ring of Linear Endomorphisms via Composition

Informal description

For any semiring $R$ and $R$-module $M$, the ring of linear endomorphisms $\text{End}_R(M)$ is equipped with a multiplication operation given by composition of linear maps. Specifically, for any two endomorphisms $f, g \in \text{End}_R(M)$, their product $f * g$ is defined as the composition $f \circ g$.

Module.End.one_eq_id theorem

: (1 : Module.End R M) = .id

Full source

theorem one_eq_id : (1 : Module.End R M) = .id := rfl

Identity Endomorphism as Multiplicative Identity in Endomorphism Ring

Informal description

In the ring of linear endomorphisms $\text{End}_R(M)$ of an $R$-module $M$, the multiplicative identity element $1$ is equal to the identity linear map $\text{id} \colon M \to M$.

Module.End.mul_eq_comp theorem

(f g : Module.End R M) : f * g = f.comp g

Full source

theorem mul_eq_comp (f g : Module.End R M) : f * g = f.comp g := rfl

Composition as Multiplication in the Endomorphism Ring

Informal description

For any two linear endomorphisms $f$ and $g$ of an $R$-module $M$, the product $f * g$ in the endomorphism ring $\text{End}_R(M)$ is equal to the composition $f \circ g$ of the linear maps.

Module.End.one_apply theorem

(x : M) : (1 : Module.End R M) x = x

Full source

@[simp]
theorem one_apply (x : M) : (1 : Module.End R M) x = x := rfl

Identity Endomorphism Acts as Identity Function

Informal description

For any element $x$ in an $R$-module $M$, the identity endomorphism $1$ acts on $x$ as the identity function, i.e., $1(x) = x$.

Module.End.mul_apply theorem

(f g : Module.End R M) (x : M) : (f * g) x = f (g x)

Full source

@[simp]
theorem mul_apply (f g : Module.End R M) (x : M) : (f * g) x = f (g x) := rfl

Composition of Linear Endomorphisms via Multiplication

Informal description

For any two linear endomorphisms $f, g$ of an $R$-module $M$ and any element $x \in M$, the action of the product endomorphism $f * g$ on $x$ is equal to the composition of $f$ and $g$ applied to $x$, i.e., $(f * g)(x) = f(g(x))$.

Module.End.coe_one theorem

: ⇑(1 : Module.End R M) = _root_.id

Full source

theorem coe_one : ⇑(1 : Module.End R M) = _root_.id := rfl

Identity Endomorphism Acts as Identity Function

Informal description

The identity endomorphism $1 \in \text{End}_R(M)$ acts as the identity function on the module $M$, i.e., for any $x \in M$, we have $1(x) = x$.

Module.End.coe_mul theorem

(f g : Module.End R M) : ⇑(f * g) = f ∘ g

Full source

theorem coe_mul (f g : Module.End R M) : ⇑(f * g) = f ∘ g := rfl

Composition of Linear Endomorphisms Corresponds to Ring Multiplication

Informal description

For any two linear endomorphisms $f, g$ of an $R$-module $M$, the underlying function of their product $f * g$ in the endomorphism ring is equal to the composition $f \circ g$ of the underlying functions.

Module.End.instNontrivial instance

[Nontrivial M] : Nontrivial (Module.End R M)

Full source

instance instNontrivial [Nontrivial M] : Nontrivial (Module.End R M) := by
  obtain ⟨m, ne⟩ := exists_ne (0 : M)
  exact nontrivial_of_ne 1 0 fun p => ne (LinearMap.congr_fun p m)

Nontriviality of the Endomorphism Ring of a Nontrivial Module

Informal description

For any semiring $R$ and nontrivial $R$-module $M$, the ring of linear endomorphisms $\text{End}_R(M)$ is nontrivial.

Module.End.instMonoid instance

: Monoid (Module.End R M)

Full source

instance instMonoid : Monoid (Module.End R M) where
  mul_assoc _ _ _ := LinearMap.ext fun _ ↦ rfl
  mul_one := comp_id
  one_mul := id_comp

Monoid Structure of Module Endomorphisms under Composition

Informal description

The set of linear endomorphisms $\text{End}_R(M)$ of an $R$-module $M$ forms a monoid under composition of maps, with the identity map as the multiplicative identity.

Module.End.instSemiring instance

: Semiring (Module.End R M)

Full source

instance instSemiring : Semiring (Module.End R M) where
  __ := AddMonoidWithOne.unary
  __ := instMonoid
  __ := addCommMonoid
  mul_zero := comp_zero
  zero_mul := zero_comp
  left_distrib := fun _ _ _ ↦ comp_add _ _ _
  right_distrib := fun _ _ _ ↦ add_comp _ _ _
  natCast := fun n ↦ n • (1 : M →ₗ[R] M)
  natCast_zero := zero_smul ℕ (1 : M →ₗ[R] M)
  natCast_succ := fun n ↦ AddMonoid.nsmul_succ n (1 : M →ₗ[R] M)

Semiring Structure on Module Endomorphisms

Informal description

The set of linear endomorphisms $\text{End}_R(M)$ of an $R$-module $M$ forms a semiring under pointwise addition and composition of maps, with the zero map as the additive identity and the identity map as the multiplicative identity.

Module.End.natCast_apply theorem

(n : ℕ) (m : M) : (↑n : Module.End R M) m = n • m

Full source

/-- See also `Module.End.natCast_def`. -/
@[simp]
theorem natCast_apply (n : ℕ) (m : M) : (↑n : Module.End R M) m = n • m := rfl

Natural Number Action as Module Endomorphism: $n \cdot m = n \bullet m$

Informal description

For any natural number $n$ and any element $m$ in an $R$-module $M$, the action of the endomorphism $\text{End}_R(M)$ corresponding to $n$ (via the natural coercion from $\mathbb{N}$) on $m$ is equal to the scalar multiplication of $n$ on $m$, i.e., $n \cdot m$.

Module.End.ofNat_apply theorem

(n : ℕ) [n.AtLeastTwo] (m : M) : (ofNat(n) : Module.End R M) m = ofNat(n) • m

Full source

@[simp]
theorem ofNat_apply (n : ℕ) [n.AtLeastTwo] (m : M) :
    (ofNat(n) : Module.End R M) m = ofNat(n) • m := rfl

Action of Numeric Endomorphism Equals Scalar Multiplication for $n \geq 2$

Informal description

For any natural number $n \geq 2$ and any element $m$ of an $R$-module $M$, the action of the endomorphism corresponding to $n$ (via the `OfNat` instance) on $m$ equals the scalar multiplication of $n$ on $m$, i.e., $n(m) = n \bullet m$.

Module.End.instRing instance

: Ring (Module.End R N₁)

Full source

instance instRing : Ring (Module.End R N₁) where
  intCast z := z • (1 : N₁ →ₗ[R] N₁)
  intCast_ofNat := natCast_zsmul _
  intCast_negSucc := negSucc_zsmul _

Ring Structure on Module Endomorphisms

Informal description

The set of linear endomorphisms $\text{End}_R(N₁)$ of an $R$-module $N₁$ forms a ring under pointwise addition and composition of maps, with the zero map as the additive identity and the identity map as the multiplicative identity.

Module.End.intCast_apply theorem

(z : ℤ) (m : N₁) : (z : Module.End R N₁) m = z • m

Full source

/-- See also `Module.End.intCast_def`. -/
@[simp]
theorem intCast_apply (z : ℤ) (m : N₁) : (z : Module.End R N₁) m = z • m :=
  rfl

Integer Endomorphism Action Equals Integer Scalar Multiplication

Informal description

For any integer $z$ and any element $m$ of an $R$-module $N₁$, the action of the endomorphism corresponding to $z$ (via the integer casting) on $m$ equals the scalar multiplication of $z$ on $m$, i.e., $z(m) = z \bullet m$.

Module.End.instIsScalarTower instance

: IsScalarTower S (Module.End R M) (Module.End R M)

Full source

instance instIsScalarTower :
    IsScalarTower S (Module.End R M) (Module.End R M) :=
  ⟨smul_comp⟩

Scalar Multiplication Tower Property for Module Endomorphisms

Informal description

For any semiring $S$ and $R$-module $M$, the scalar multiplication by $S$ on the endomorphism ring $\text{End}_R(M)$ satisfies the tower property. That is, for any $s \in S$, $f \in \text{End}_R(M)$, and $g \in \text{End}_R(M)$, we have $(s \cdot f) \circ g = s \cdot (f \circ g)$.

Module.End.instSMulCommClass instance

[SMul S R] [IsScalarTower S R M] : SMulCommClass S (Module.End R M) (Module.End R M)

Full source

instance instSMulCommClass [SMul S R] [IsScalarTower S R M] :
    SMulCommClass S (Module.End R M) (Module.End R M) :=
  ⟨fun s _ _ ↦ (comp_smul _ s _).symm⟩

Commutativity of Scalar Multiplication with Module Endomorphisms under Scalar Tower Condition

Informal description

For any semiring $R$ and $R$-module $M$, and given a scalar multiplication action of $S$ on $R$ with the scalar tower property (i.e., $s \cdot (r \cdot m) = (s \cdot r) \cdot m$ for all $s \in S$, $r \in R$, $m \in M$), the scalar multiplications by $S$ and by endomorphisms in $\text{End}_R(M)$ commute with each other. That is, for any $s \in S$, $f \in \text{End}_R(M)$, and $m \in M$, we have $s \cdot (f \cdot m) = f \cdot (s \cdot m)$.

Module.End.instSMulCommClass' instance

[SMul S R] [IsScalarTower S R M] : SMulCommClass (Module.End R M) S (Module.End R M)

Full source

instance instSMulCommClass' [SMul S R] [IsScalarTower S R M] :
    SMulCommClass (Module.End R M) S (Module.End R M) :=
  SMulCommClass.symm _ _ _

Commutativity of Module Endomorphisms with Scalar Multiplication under Scalar Tower Condition

Informal description

For any semiring $R$ and $R$-module $M$, given a scalar multiplication action of $S$ on $R$ with the scalar tower property (i.e., $s \cdot (r \cdot m) = (s \cdot r) \cdot m$ for all $s \in S$, $r \in R$, $m \in M$), the scalar multiplications by endomorphisms in $\text{End}_R(M)$ and by $S$ commute with each other. That is, for any $f \in \text{End}_R(M)$, $s \in S$, and $g \in \text{End}_R(M)$, we have $f \circ (s \cdot g) = s \cdot (f \circ g)$.

Module.End.isUnit_apply_inv_apply_of_isUnit theorem

{f : End R M} (h : IsUnit f) (x : M) : f (h.unit.inv x) = x

Full source

theorem isUnit_apply_inv_apply_of_isUnit {f : End R M} (h : IsUnit f) (x : M) :
    f (h.unit.inv x) = x :=
  show (f * h.unit.inv) x = x by simp

Invertible Endomorphism Property: $f(f^{-1}(x)) = x$

Informal description

Let $M$ be a module over a semiring $R$, and let $f \in \text{End}_R(M)$ be an invertible endomorphism (i.e., $f$ is a unit in the ring of endomorphisms). Then for any $x \in M$, applying $f$ to the inverse of $f$ evaluated at $x$ yields $x$ itself, i.e., $f(f^{-1}(x)) = x$.

Module.End.isUnit_inv_apply_apply_of_isUnit theorem

{f : End R M} (h : IsUnit f) (x : M) : h.unit.inv (f x) = x

Full source

theorem isUnit_inv_apply_apply_of_isUnit {f : End R M} (h : IsUnit f) (x : M) :
    h.unit.inv (f x) = x :=
  (by simp : (h.unit.inv * f) x = x)

Inverse of Invertible Linear Endomorphism Acts as Left Inverse

Informal description

For any linear endomorphism $f$ of an $R$-module $M$, if $f$ is invertible (i.e., $f$ is a unit in the ring of endomorphisms), then applying the inverse of $f$ to $f(x)$ yields $x$ for any $x \in M$. In other words, $f^{-1}(f(x)) = x$.

Module.End.coe_pow theorem

(f : End R M) (n : ℕ) : ⇑(f ^ n) = f^[n]

Full source

theorem coe_pow (f : End R M) (n : ℕ) : ⇑(f ^ n) = f^[n] := hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _

Power of Endomorphism Equals Iteration: $f^n = f^[n]$

Informal description

For any linear endomorphism $f$ of an $R$-module $M$ and any natural number $n$, the $n$-th power of $f$ (under composition) is equal to the $n$-th iterate of $f$ as a function, i.e., $(f^n)(x) = f^[n](x)$ for all $x \in M$.

Module.End.pow_apply theorem

(f : End R M) (n : ℕ) (m : M) : (f ^ n) m = f^[n] m

Full source

theorem pow_apply (f : End R M) (n : ℕ) (m : M) : (f ^ n) m = f^[n] m := congr_fun (coe_pow f n) m

Power of Endomorphism Equals Iterated Application: $f^n(m) = f^[n](m)$

Informal description

For any linear endomorphism $f$ of an $R$-module $M$, any natural number $n$, and any element $m \in M$, the application of the $n$-th power of $f$ to $m$ equals the $n$-th iterate of $f$ applied to $m$, i.e., $(f^n)(m) = f^[n](m)$.

Module.End.pow_map_zero_of_le theorem

{f : End R M} {m : M} {k l : ℕ} (hk : k ≤ l) (hm : (f ^ k) m = 0) : (f ^ l) m = 0

Full source

theorem pow_map_zero_of_le {f : End R M} {m : M} {k l : ℕ} (hk : k ≤ l)
    (hm : (f ^ k) m = 0) : (f ^ l) m = 0 := by
  rw [← Nat.sub_add_cancel hk, pow_add, mul_apply, hm, map_zero]

Vanishing Property of Iterated Endomorphisms: $f^k(m) = 0 \Rightarrow f^l(m) = 0$ for $k \leq l$

Informal description

Let $M$ be a module over a semiring $R$, and let $f \colon M \to M$ be a linear endomorphism. For any element $m \in M$ and natural numbers $k, l$ such that $k \leq l$, if $f^k(m) = 0$, then $f^l(m) = 0$.

Module.End.commute_pow_left_of_commute theorem

 [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} {g : Module.End R M}
  {g₂ : Module.End R₂ M₂} (h : g₂.comp f = f.comp g) (k : ℕ) : (g₂ ^ k).comp f = f.comp (g ^ k)

Full source

theorem commute_pow_left_of_commute
    [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂}
    {f : M →ₛₗ[σ₁₂] M₂} {g : Module.End R M} {g₂ : Module.End R₂ M₂}
    (h : g₂.comp f = f.comp g) (k : ℕ) : (g₂ ^ k).comp f = f.comp (g ^ k) := by
  induction k with
  | zero => simp [one_eq_id]
  | succ k ih => rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]

Commutation of Semilinear Maps with Powers of Endomorphisms

Informal description

Let $R$ and $R_2$ be semirings, $M$ and $M_2$ be additive commutative monoids with module structures over $R$ and $R_2$ respectively, and $\sigma_{12} \colon R \to R_2$ be a ring homomorphism. Given a semilinear map $f \colon M \to_{\sigma_{12}} M_2$ and linear endomorphisms $g \in \text{End}_R(M)$, $g_2 \in \text{End}_{R_2}(M_2)$ such that $g_2 \circ f = f \circ g$, then for any natural number $k$, the $k$-th power of $g_2$ composed with $f$ equals $f$ composed with the $k$-th power of $g$, i.e., $$(g_2^k) \circ f = f \circ (g^k).$$

Module.End.id_pow theorem

(n : ℕ) : (id : End R M) ^ n = .id

Full source

@[simp]
theorem id_pow (n : ℕ) : (id : End R M) ^ n = .id :=
  one_pow n

Identity Endomorphism Power Law: $\text{id}^n = \text{id}$

Informal description

For any natural number $n$, the $n$-th power of the identity endomorphism $\text{id} \colon M \to M$ on an $R$-module $M$ equals the identity endomorphism, i.e., $\text{id}^n = \text{id}$.

Module.End.iterate_succ theorem

(n : ℕ) : f' ^ (n + 1) = .comp (f' ^ n) f'

Full source

theorem iterate_succ (n : ℕ) : f' ^ (n + 1) = .comp (f' ^ n) f' := by rw [pow_succ, mul_eq_comp]

Recursive formula for iterates of a linear endomorphism: $f'^{n+1} = f'^n \circ f'$

Informal description

For any linear endomorphism $f'$ of an $R$-module $M$ and any natural number $n$, the $(n+1)$-th iterate of $f'$ is equal to the composition of the $n$-th iterate of $f'$ with $f'$ itself, i.e., $f'^{n+1} = f'^n \circ f'$.

Module.End.iterate_surjective theorem

(h : Surjective f') : ∀ n : ℕ, Surjective (f' ^ n)

Full source

theorem iterate_surjective (h : Surjective f') : ∀ n : ℕ, Surjective (f' ^ n)
  | 0 => surjective_id
  | n + 1 => by
    rw [iterate_succ]
    exact (iterate_surjective h n).comp h

Surjectivity of Iterates of a Surjective Linear Endomorphism

Informal description

Let $M$ be a module over a semiring $R$ and let $f' \colon M \to M$ be a surjective linear endomorphism. Then for every natural number $n$, the $n$-th iterate $f'^n$ is also surjective.

Module.End.iterate_injective theorem

(h : Injective f') : ∀ n : ℕ, Injective (f' ^ n)

Full source

theorem iterate_injective (h : Injective f') : ∀ n : ℕ, Injective (f' ^ n)
  | 0 => injective_id
  | n + 1 => by
    rw [iterate_succ]
    exact (iterate_injective h n).comp h

Injectivity of Iterates of an Injective Linear Endomorphism

Informal description

Let $f'$ be an injective linear endomorphism of an $R$-module $M$. Then for every natural number $n$, the $n$-th iterate $f'^n$ is also injective.

Module.End.iterate_bijective theorem

(h : Bijective f') : ∀ n : ℕ, Bijective (f' ^ n)

Full source

theorem iterate_bijective (h : Bijective f') : ∀ n : ℕ, Bijective (f' ^ n)
  | 0 => bijective_id
  | n + 1 => by
    rw [iterate_succ]
    exact (iterate_bijective h n).comp h

Bijectivity of Iterates of a Bijective Linear Endomorphism

Informal description

Let $M$ be a module over a semiring $R$, and let $f \colon M \to M$ be a bijective linear endomorphism. Then for every natural number $n$, the $n$-th iterate $f^n$ of $f$ is also bijective.

Module.End.injective_of_iterate_injective theorem

{n : ℕ} (hn : n ≠ 0) (h : Injective (f' ^ n)) : Injective f'

Full source

theorem injective_of_iterate_injective {n : ℕ} (hn : n ≠ 0) (h : Injective (f' ^ n)) :
    Injective f' := by
  rw [← Nat.succ_pred_eq_of_pos (show 0 < n by omega), iterate_succ, coe_comp] at h
  exact h.of_comp

Injectivity of a Linear Endomorphism via Iterates

Informal description

Let $M$ be a module over a semiring $R$, and let $f \colon M \to M$ be a linear endomorphism. If for some nonzero natural number $n$, the $n$-th iterate $f^n$ is injective, then $f$ itself is injective.

Module.End.surjective_of_iterate_surjective theorem

{n : ℕ} (hn : n ≠ 0) (h : Surjective (f' ^ n)) : Surjective f'

Full source

theorem surjective_of_iterate_surjective {n : ℕ} (hn : n ≠ 0) (h : Surjective (f' ^ n)) :
    Surjective f' := by
  rw [← Nat.succ_pred_eq_of_pos (Nat.pos_iff_ne_zero.mpr hn), pow_succ', coe_mul] at h
  exact Surjective.of_comp h

Surjectivity of a Linear Endomorphism via Iterates

Informal description

Let $M$ be a module over a semiring $R$, and let $f \colon M \to M$ be a linear endomorphism. If for some nonzero natural number $n$, the $n$-th iterate $f^n$ is surjective, then $f$ itself is surjective.

Module.End.applyModule instance

: Module (Module.End R M) M

Full source

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

This generalizes `Function.End.applyMulAction`. -/
instance applyModule : Module (Module.End R M) M where
  smul := (· <| ·)
  smul_zero := LinearMap.map_zero
  smul_add := LinearMap.map_add
  add_smul := LinearMap.add_apply
  zero_smul := (LinearMap.zero_apply : ∀ m, (0 : M →ₗ[R] M) m = 0)
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

Module Structure on $M$ via Endomorphism Action

Informal description

The set of linear endomorphisms $\text{End}_R(M)$ of an $R$-module $M$ acts on $M$ via the natural action $f \cdot a = f(a)$. This action makes $M$ into a module over the semiring $\text{End}_R(M)$.

Module.End.smul_def theorem

(f : Module.End R M) (a : M) : f • a = f a

Full source

@[simp]
protected theorem smul_def (f : Module.End R M) (a : M) : f • a = f a :=
  rfl

Scalar Multiplication of Module Endomorphism Equals Function Application

Informal description

For any linear endomorphism $f$ of an $R$-module $M$ and any element $a \in M$, the scalar multiplication of $f$ on $a$ is equal to the application of $f$ to $a$, i.e., $f \bullet a = f(a)$.

Module.End.apply_faithfulSMul instance

: FaithfulSMul (Module.End R M) M

Full source

/-- `LinearMap.applyModule` is faithful. -/
instance apply_faithfulSMul : FaithfulSMul (Module.End R M) M :=
  ⟨LinearMap.ext⟩

Faithfulness of the Endomorphism Action on a Module

Informal description

The natural action of the semiring of linear endomorphisms $\text{End}_R(M)$ on an $R$-module $M$ is faithful. That is, for any two endomorphisms $f, g \in \text{End}_R(M)$, if $f(a) = g(a)$ for all $a \in M$, then $f = g$.

Module.End.apply_smulCommClass instance

[SMul S R] [SMul S M] [IsScalarTower S R M] : SMulCommClass S (Module.End R M) M

Full source

instance apply_smulCommClass [SMul S R] [SMul S M] [IsScalarTower S R M] :
    SMulCommClass S (Module.End R M) M where
  smul_comm r e m := (e.map_smul_of_tower r m).symm

Commutation of Scalar and Endomorphism Actions in Module Towers

Informal description

Let $R$ be a semiring and $M$ be an $R$-module. Suppose $S$ is a type with scalar multiplication actions on both $R$ and $M$, such that the scalar multiplications form a tower (i.e., for $s \in S$, $r \in R$, $x \in M$ we have $s \cdot (r \cdot x) = (s \cdot r) \cdot x$). Then the scalar multiplication by $S$ commutes with the action of the endomorphism ring $\text{End}_R(M)$ on $M$. That is, for any $s \in S$, $f \in \text{End}_R(M)$, and $x \in M$, we have $s \cdot (f \cdot x) = f \cdot (s \cdot x)$.

Module.End.apply_smulCommClass' instance

[SMul S R] [SMul S M] [IsScalarTower S R M] : SMulCommClass (Module.End R M) S M

Full source

instance apply_smulCommClass' [SMul S R] [SMul S M] [IsScalarTower S R M] :
    SMulCommClass (Module.End R M) S M :=
  SMulCommClass.symm _ _ _

Commutation of Endomorphism and Scalar Actions in Module Towers

Informal description

For any semiring $R$ and $R$-module $M$, and given a type $S$ with scalar multiplication actions on both $R$ and $M$ forming a scalar tower (i.e., $s \cdot (r \cdot x) = (s \cdot r) \cdot x$ for all $s \in S$, $r \in R$, $x \in M$), the action of the endomorphism ring $\text{End}_R(M)$ on $M$ commutes with the scalar multiplication by $S$. That is, for any $f \in \text{End}_R(M)$, $s \in S$, and $x \in M$, we have $f(s \cdot x) = s \cdot f(x)$.

Module.End.apply_isScalarTower instance

[Monoid S] [DistribMulAction S M] [SMulCommClass R S M] : IsScalarTower S (Module.End R M) M

Full source

instance apply_isScalarTower [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] :
    IsScalarTower S (Module.End R M) M :=
  ⟨fun _ _ _ ↦ rfl⟩

Compatibility of Scalar and Endomorphism Actions on a Module

Informal description

Given a monoid $S$ with a distributive action on an $R$-module $M$ such that the scalar multiplications by $R$ and $S$ commute, the scalar multiplication by $S$ on $M$ is compatible with the action of the endomorphism ring $\text{End}_R(M)$. That is, for any $s \in S$, $f \in \text{End}_R(M)$, and $x \in M$, we have $s \cdot (f \cdot x) = (s \cdot f) \cdot x$.

DistribMulAction.toLinearMap definition

(s : S) : M →ₗ[R] M

Full source

/-- Each element of the monoid defines a linear map.

This is a stronger version of `DistribMulAction.toAddMonoidHom`. -/
@[simps]
def toLinearMap (s : S) : M →ₗ[R] M where
  toFun := HSMul.hSMul s
  map_add' := smul_add s
  map_smul' _ _ := smul_comm _ _ _

Linear map induced by distributive monoid action

Informal description

For each element $s$ in a monoid $S$ acting distributively on an $R$-module $M$, the scalar multiplication by $s$ defines a linear map from $M$ to itself. This map satisfies: 1. Additivity: $s \cdot (x + y) = s \cdot x + s \cdot y$ for all $x, y \in M$ 2. Compatibility with scalar multiplication: $s \cdot (r \cdot x) = r \cdot (s \cdot x)$ for all $r \in R$ and $x \in M$

DistribMulAction.toModuleEnd definition

: S →* Module.End R M

Full source

/-- Each element of the monoid defines a module endomorphism.

This is a stronger version of `DistribMulAction.toAddMonoidEnd`. -/
@[simps]
def toModuleEnd : S →* Module.End R M where
  toFun := toLinearMap R M
  map_one' := LinearMap.ext <| one_smul _
  map_mul' _ _ := LinearMap.ext <| mul_smul _ _

Monoid action as module endomorphisms

Informal description

Given a monoid $S$ acting distributively on an $R$-module $M$, the function maps each element $s \in S$ to the corresponding $R$-linear endomorphism of $M$ defined by scalar multiplication by $s$. This mapping preserves the monoid structure, sending the identity element of $S$ to the identity endomorphism and respecting the multiplication operation in $S$.

Module.toModuleEnd definition

: S →+* Module.End R M

Full source

/-- Each element of the semiring defines a module endomorphism.

This is a stronger version of `DistribMulAction.toModuleEnd`. -/
@[simps]
def Module.toModuleEnd : S →+* Module.End R M :=
  { DistribMulAction.toModuleEnd R M with
    toFun := DistribMulAction.toLinearMap R M
    map_zero' := LinearMap.ext <| zero_smul S
    map_add' := fun _ _ ↦ LinearMap.ext <| add_smul _ _ }

Semiring action as module endomorphisms

Informal description

Given a semiring $S$ acting on an $R$-module $M$, the function maps each element $s \in S$ to the corresponding $R$-linear endomorphism of $M$ defined by scalar multiplication by $s$. This mapping is a semiring homomorphism, preserving both the additive and multiplicative structures, where: 1. The zero element of $S$ maps to the zero endomorphism 2. Addition in $S$ corresponds to pointwise addition of endomorphisms This extends the monoid homomorphism version (`DistribMulAction.toModuleEnd`) to a semiring homomorphism.

RingEquiv.moduleEndSelf definition

: Rᵐᵒᵖ ≃+* Module.End R R

Full source

/-- The canonical (semi)ring isomorphism from `Rᵐᵒᵖ` to `Module.End R R` induced by the right
multiplication. -/
@[simps]
def RingEquiv.moduleEndSelf : RᵐᵒᵖRᵐᵒᵖ ≃+* Module.End R R :=
  { Module.toModuleEnd R R with
    toFun := DistribMulAction.toLinearMap R R
    invFun := fun f ↦ MulOpposite.op (f 1)
    left_inv := mul_one
    right_inv := fun _ ↦ LinearMap.ext_ring <| one_mul _ }

Ring isomorphism between opposite ring and endomorphism ring

Informal description

The canonical ring isomorphism between the multiplicative opposite ring $R^\text{op}$ and the ring of linear endomorphisms $\text{End}_R(R)$ of $R$ as a module over itself. This isomorphism maps each element $r \in R^\text{op}$ to the endomorphism given by right multiplication by $r$, and its inverse maps an endomorphism $f$ to $f(1)$ (considered as an element of $R^\text{op}$).

RingEquiv.moduleEndSelfOp definition

: R ≃+* Module.End Rᵐᵒᵖ R

Full source

/-- The canonical (semi)ring isomorphism from `R` to `Module.End Rᵐᵒᵖ R` induced by the left
multiplication. -/
@[simps]
def RingEquiv.moduleEndSelfOp : R ≃+* Module.End Rᵐᵒᵖ R :=
  { Module.toModuleEnd _ _ with
    toFun := DistribMulAction.toLinearMap _ _
    invFun := fun f ↦ f 1
    left_inv := mul_one
    right_inv := fun _ ↦ LinearMap.ext_ring_op <| mul_one _ }

Ring isomorphism between a semiring and its opposite module endomorphisms

Informal description

The canonical ring isomorphism from a semiring $R$ to the ring of linear endomorphisms of the multiplicative opposite $R^\text{op}$ as an $R$-module. This isomorphism maps each element $r \in R$ to the linear endomorphism given by left multiplication by $r$ on $R^\text{op}$, and its inverse maps each endomorphism $f$ to $f(1)$.

Module.End.natCast_def theorem

(n : ℕ) [AddCommMonoid N₁] [Module R N₁] : (↑n : Module.End R N₁) = Module.toModuleEnd R N₁ n

Full source

theorem Module.End.natCast_def (n : ℕ) [AddCommMonoid N₁] [Module R N₁] :
    (↑n : Module.End R N₁) = Module.toModuleEnd R N₁ n :=
  rfl

Natural Number Action as Scalar Multiplication in Module Endomorphisms

Informal description

For any natural number $n$ and any $R$-module $N_1$ (where $N_1$ is an additive commutative monoid with a scalar multiplication satisfying the module axioms), the canonical embedding of $n$ into the ring of $R$-linear endomorphisms $\text{End}_R(N_1)$ is equal to the endomorphism given by scalar multiplication by $n$. That is, the natural number $n$ acts on $N_1$ via $x \mapsto n \cdot x$.

Module.End.intCast_def theorem

(z : ℤ) [AddCommGroup N₁] [Module R N₁] : (z : Module.End R N₁) = Module.toModuleEnd R N₁ z

Full source

theorem Module.End.intCast_def (z : ℤ) [AddCommGroup N₁] [Module R N₁] :
    (z : Module.End R N₁) = Module.toModuleEnd R N₁ z :=
  rfl

Integer Scalar Multiplication as Module Endomorphism

Informal description

For any integer $z \in \mathbb{Z}$ and any $R$-module $N₁$ where $N₁$ is an additive commutative group, the endomorphism corresponding to $z$ in the ring of $R$-linear endomorphisms $\text{End}_R(N₁)$ is equal to the endomorphism defined by scalar multiplication by $z$.

LinearMap.smulRight definition

(f : M₁ →ₗ[R] S) (x : M) : M₁ →ₗ[R] M

Full source

/-- When `f` is an `R`-linear map taking values in `S`, then `fun b ↦ f b • x` is an `R`-linear
map. -/
def smulRight (f : M₁ →ₗ[R] S) (x : M) : M₁ →ₗ[R] M where
  toFun b := f b • x
  map_add' x y := by rw [f.map_add, add_smul]
  map_smul' b y := by rw [RingHom.id_apply, map_smul, smul_assoc]

Linear map defined by scalar multiplication via a linear functional

Informal description

Given an $R$-linear map $f \colon M_1 \to S$ and an element $x \in M$, the function $b \mapsto f(b) \bullet x$ defines an $R$-linear map from $M_1$ to $M$, where $\bullet$ denotes the scalar multiplication in $M$.

LinearMap.coe_smulRight theorem

(f : M₁ →ₗ[R] S) (x : M) : (smulRight f x : M₁ → M) = fun c => f c • x

Full source

@[simp]
theorem coe_smulRight (f : M₁ →ₗ[R] S) (x : M) : (smulRight f x : M₁ → M) = fun c => f c • x :=
  rfl

Explicit form of the linear map $\mathrm{smulRight}\, f\, x$

Informal description

For any $R$-linear map $f \colon M_1 \to S$ and any element $x \in M$, the linear map $\mathrm{smulRight}\, f\, x \colon M_1 \to M$ is given by the function $c \mapsto f(c) \cdot x$ for all $c \in M_1$.

LinearMap.smulRight_apply theorem

(f : M₁ →ₗ[R] S) (x : M) (c : M₁) : smulRight f x c = f c • x

Full source

theorem smulRight_apply (f : M₁ →ₗ[R] S) (x : M) (c : M₁) : smulRight f x c = f c • x :=
  rfl

Evaluation of the Linear Map $\mathrm{smulRight}(f, x)$

Informal description

Let $R$ be a semiring, $M$ be an $R$-module, and $S$ be another semiring such that $M$ has a compatible $S$-action. Given an $R$-linear map $f \colon M_1 \to S$ and an element $x \in M$, the linear map $\mathrm{smulRight}(f, x) \colon M_1 \to M$ satisfies $\mathrm{smulRight}(f, x)(c) = f(c) \cdot x$ for all $c \in M_1$, where $\cdot$ denotes the scalar multiplication in $M$.

LinearMap.smulRight_zero theorem

(f : M₁ →ₗ[R] S) : f.smulRight (0 : M) = 0

Full source

@[simp]
lemma smulRight_zero (f : M₁ →ₗ[R] S) : f.smulRight (0 : M) = 0 := by ext; simp

Zero vector scalar multiplication yields zero map

Informal description

For any $R$-linear map $f \colon M_1 \to S$, the linear map defined by scalar multiplication via $f$ with the zero vector in $M$ is equal to the zero map, i.e., $f \cdot 0 = 0$.

LinearMap.zero_smulRight theorem

(x : M) : (0 : M₁ →ₗ[R] S).smulRight x = 0

Full source

@[simp]
lemma zero_smulRight (x : M) : (0 : M₁ →ₗ[R] S).smulRight x = 0 := by ext; simp

Zero Functional Yields Zero Map under Scalar Multiplication

Informal description

For any element $x$ in an $R$-module $M$, the linear map obtained by scalar multiplication via the zero linear functional $0 \colon M_1 \to S$ is the zero map, i.e., $(0 \colon M_1 \to S).\text{smulRight}(x) = 0$.

LinearMap.smulRight_apply_eq_zero_iff theorem

{f : M₁ →ₗ[R] S} {x : M} [NoZeroSMulDivisors S M] : f.smulRight x = 0 ↔ f = 0 ∨ x = 0

Full source

@[simp]
lemma smulRight_apply_eq_zero_iff {f : M₁ →ₗ[R] S} {x : M} [NoZeroSMulDivisors S M] :
    f.smulRight x = 0 ↔ f = 0 ∨ x = 0 := by
  rcases eq_or_ne x 0 with rfl | hx
  · simp
  refine ⟨fun h ↦ Or.inl ?_, fun h ↦ by simp [h.resolve_right hx]⟩
  ext v
  replace h : f v • x = 0 := by simpa only [LinearMap.zero_apply] using LinearMap.congr_fun h v
  rw [smul_eq_zero] at h
  tauto

Zero Criterion for Scalar Multiplication via Linear Functional: $f \cdot x = 0 \leftrightarrow f = 0 \lor x = 0$

Informal description

Let $M$ be a module over a semiring $R$, $S$ another semiring, and $M_1$ an $R$-module. Given an $R$-linear map $f \colon M_1 \to S$ and an element $x \in M$, the linear map $f \cdot x \colon M_1 \to M$ defined by $(f \cdot x)(b) = f(b) \cdot x$ is the zero map if and only if either $f$ is the zero map or $x$ is the zero vector in $M$, provided that $S$ and $M$ have no zero scalar divisors (i.e., $a \cdot v = 0$ implies $a = 0$ or $v = 0$ for $a \in S$ and $v \in M$).

LinearMap.applyₗ' definition

: M →+ (M →ₗ[R] M₂) →ₗ[S] M₂

Full source

/-- 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`. -/
@[simps]
def applyₗ' : M →+ (M →ₗ[R] M₂) →ₗ[S] M₂ where
  toFun v :=
    { toFun := fun f => f v
      map_add' := fun f g => f.add_apply g v
      map_smul' := fun x f => f.smul_apply x v }
  map_zero' := LinearMap.ext fun f => f.map_zero
  map_add' _ _ := LinearMap.ext fun f => f.map_add _ _

Evaluation of linear maps at a fixed vector

Informal description

For a fixed element $v$ in an $R$-module $M$, the function $\text{applyₗ'}$ evaluates linear maps $f \colon M \to_{R} M₂$ at $v$, producing an element $f(v) \in M₂$. This evaluation is an $S$-linear map from the space of $R$-linear maps $\text{Hom}_R(M, M₂)$ to $M₂$, and it is also an additive homomorphism. More precisely, $\text{applyₗ'}$ is the map that takes $v \in M$ and returns the evaluation-at-$v$ functional, which is both $S$-linear and additive in $v$.

LinearMap.compRight definition

(f : M₂ →ₗ[R] M₃) : (M →ₗ[R] M₂) →ₗ[R] M →ₗ[R] M₃

Full source

/-- 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₃`. -/
def compRight (f : M₂ →ₗ[R] M₃) : (M →ₗ[R] M₂) →ₗ[R] M →ₗ[R] M₃ where
  toFun g := f.comp g
  map_add' _ _ := LinearMap.ext fun _ => map_add f _ _
  map_smul' _ _ := LinearMap.ext fun _ => map_smul f _ _

Right composition with a linear map

Informal description

Given a linear map $f \colon M_2 \to M_3$ between $R$-modules, the function $\text{compRight}(f)$ maps a linear map $g \colon M \to M_2$ to the composition $f \circ g \colon M \to M_3$. This operation is itself a linear map from the space of linear maps $M \to M_2$ to the space of linear maps $M \to M_3$.

LinearMap.compRight_apply theorem

(f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂) : compRight f g = f.comp g

Full source

@[simp]
theorem compRight_apply (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂) : compRight f g = f.comp g :=
  rfl

Composition of Linear Maps via Right Application

Informal description

Given a linear map $f \colon M_2 \to M_3$ between $R$-modules and a linear map $g \colon M \to M_2$, the composition $\text{compRight}(f)(g)$ equals the composition $f \circ g \colon M \to M_3$.

LinearMap.applyₗ definition

: M →ₗ[R] (M →ₗ[R] M₂) →ₗ[R] M₂

Full source

/-- 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`. -/
@[simps]
def applyₗ : M →ₗ[R] (M →ₗ[R] M₂) →ₗ[R] M₂ :=
  { applyₗ' R with
    toFun := fun v => { applyₗ' R v with toFun := fun f => f v }
    map_smul' := fun _ _ => LinearMap.ext fun f => map_smul f _ _ }

Linear evaluation map at a fixed vector

Informal description

For a fixed element $v$ in an $R$-module $M$, the function $\text{applyₗ}$ evaluates linear maps $f \colon M \to_{R} M₂$ at $v$, producing an element $f(v) \in M₂$. This evaluation is itself an $R$-linear map from the space of $R$-linear maps $\text{Hom}_R(M, M₂)$ to $M₂$. More precisely, $\text{applyₗ}$ is the $R$-linear map that takes $v \in M$ and returns the evaluation-at-$v$ functional, which is $R$-linear in $v$.

LinearMap.smulRightₗ definition

: (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M

Full source

/--
The family of linear maps `M₂ → M` parameterised by `f ∈ M₂ → R`, `x ∈ M`, is linear in `f`, `x`.
-/
def smulRightₗ : (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M where
  toFun f :=
    { toFun := LinearMap.smulRight f
      map_add' := fun m m' => by
        ext
        apply smul_add
      map_smul' := fun c m => by
        ext
        apply smul_comm }
  map_add' f f' := by
    ext
    apply add_smul
  map_smul' c f := by
    ext
    apply mul_smul

Linear map induced by scalar multiplication via a linear functional

Informal description

The linear map that takes a linear functional $f \colon M_2 \to R$ and an element $x \in M$ to the linear map $M_2 \to M$ defined by $c \mapsto f(c) \cdot x$, where $\cdot$ denotes the scalar multiplication in $M$. This construction is itself linear in both $f$ and $x$.

LinearMap.smulRightₗ_apply theorem

 (f : M₂ →ₗ[R] R) (x : M) (c : M₂) : (smulRightₗ : (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M) f x c = f c • x

Full source

@[simp]
theorem smulRightₗ_apply (f : M₂ →ₗ[R] R) (x : M) (c : M₂) :
    (smulRightₗ : (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M) f x c = f c • x :=
  rfl

Evaluation of the Linear Map $\text{smulRight}_\ell$

Informal description

For any linear functional $f \colon M_2 \to R$, any element $x \in M$, and any $c \in M_2$, the evaluation of the linear map $\text{smulRight}_\ell(f, x)$ at $c$ is equal to the scalar multiplication of $f(c)$ with $x$, i.e., \[ \text{smulRight}_\ell(f, x)(c) = f(c) \cdot x. \]

Module.End.commute_id_left theorem

: Commute LinearMap.id f

Full source

lemma commute_id_left : Commute LinearMap.id f := by ext; simp

Identity Map Commutes with All Endomorphisms

Informal description

For any linear endomorphism $f$ of an $R$-module $M$, the identity map $\text{id}_M$ commutes with $f$ under composition, i.e., $\text{id}_M \circ f = f \circ \text{id}_M$.

Module.End.commute_id_right theorem

: Commute f LinearMap.id

Full source

lemma commute_id_right : Commute f LinearMap.id := by ext; simp

Right Commutation of Endomorphisms with Identity

Informal description

For any linear endomorphism $f$ of an $R$-module $M$, the identity map $\text{id}_M$ commutes with $f$ under composition, i.e., $f \circ \text{id}_M = \text{id}_M \circ f$.

Main results