Mathlib.Algebra.Module.Submodule.LinearMap

SMulMemClass.subtype definition

: S' →ₗ[R] M

Full source

/-- The natural `R`-linear map from a submodule of an `R`-module `M` to `M`. -/
protected def subtype : S' →ₗ[R] M where
  toFun := Subtype.val
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

Canonical linear embedding of a scalar-multiplication-closed subset

Informal description

Given a module $M$ over a semiring $R$ and a subset $S'$ of $M$ that is closed under scalar multiplication (i.e., $S'$ is an instance of `SMulMemClass`), the function `SMulMemClass.subtype` is the canonical $R$-linear embedding of $S'$ into $M$. More precisely, it is the linear map that sends each element $x \in S'$ to itself (viewed as an element of $M$), preserving both addition and scalar multiplication: - For any $x, y \in S'$, we have $\text{subtype}(x + y) = \text{subtype}(x) + \text{subtype}(y)$ - For any $r \in R$ and $x \in S'$, we have $\text{subtype}(r \bullet x) = r \bullet \text{subtype}(x)$

SMulMemClass.subtype_apply theorem

(x : S') : SMulMemClass.subtype S' x = x

Full source

@[simp]
lemma subtype_apply (x : S') :
    SMulMemClass.subtype S' x = x := rfl

Canonical Linear Embedding Acts as Identity on Elements

Informal description

For any element $x$ in a subset $S'$ of a module $M$ that is closed under scalar multiplication, the canonical linear embedding $\text{subtype}$ of $S'$ into $M$ satisfies $\text{subtype}(x) = x$.

SMulMemClass.subtype_injective theorem

: Function.Injective (SMulMemClass.subtype S')

Full source

lemma subtype_injective :
    Function.Injective (SMulMemClass.subtype S') :=
  Subtype.coe_injective

Injectivity of the Submodule Inclusion Map

Informal description

The canonical linear embedding $\text{subtype} : S' \to M$ of a scalar-multiplication-closed subset $S'$ of a module $M$ over a semiring $R$ is injective. That is, for any $x, y \in S'$, if $\text{subtype}(x) = \text{subtype}(y)$ in $M$, then $x = y$ in $S'$.

SMulMemClass.coe_subtype theorem

: (SMulMemClass.subtype S' : S' → M) = Subtype.val

Full source

@[simp]
protected theorem coe_subtype : (SMulMemClass.subtype S' : S' → M) = Subtype.val :=
  rfl

Coercion Equals Subtype Embedding for Scalar-Multiplication-Closed Subsets

Informal description

The canonical linear embedding `SMulMemClass.subtype` from a scalar-multiplication-closed subset $S'$ into the ambient module $M$ coincides with the coercion function `Subtype.val`, i.e., for any $x \in S'$, we have $\text{subtype}(x) = x$ as elements of $M$.

Submodule.subtype definition

: p →ₗ[R] M

Full source

/-- Embedding of a submodule `p` to the ambient space `M`. -/
protected def subtype : p →ₗ[R] M where
  toFun := Subtype.val
  map_add' := by simp [coe_smul]
  map_smul' := by simp [coe_smul]

Submodule inclusion map

Informal description

The linear map that embeds a submodule $p$ into its ambient module $M$ by sending each element $x \in p$ to itself (viewed as an element of $M$). This is the canonical inclusion map $p \hookrightarrow M$ that preserves the module structure.

Submodule.subtype_apply theorem

(x : p) : p.subtype x = x

Full source

@[simp]
theorem subtype_apply (x : p) : p.subtype x = x :=
  rfl

Inclusion Map Acts as Identity on Submodule Elements

Informal description

For any element $x$ in a submodule $p$ of a module $M$ over a semiring $R$, the image of $x$ under the inclusion map $p \hookrightarrow M$ is equal to $x$ itself, i.e., $p.\text{subtype}(x) = x$.

Submodule.subtype_injective theorem

: Function.Injective p.subtype

Full source

lemma subtype_injective :
    Function.Injective p.subtype :=
  Subtype.coe_injective

Injectivity of Submodule Inclusion Map

Informal description

The canonical inclusion map from a submodule $p$ to its ambient module $M$ is injective. That is, for any $x, y \in p$, if $x = y$ in $M$, then $x = y$ in $p$.

Submodule.coe_subtype theorem

: (Submodule.subtype p : p → M) = Subtype.val

Full source

@[simp]
theorem coe_subtype : (Submodule.subtype p : p → M) = Subtype.val :=
  rfl

Submodule Inclusion Map as Coercion

Informal description

The underlying function of the submodule inclusion map `p.subtype` from a submodule $p$ to its ambient module $M$ is equal to the canonical coercion function `Subtype.val` that extracts the underlying element from a term of the subtype $p$.

Submodule.injective_subtype theorem

: Injective p.subtype

Full source

theorem injective_subtype : Injective p.subtype :=
  Subtype.coe_injective

Injectivity of Submodule Inclusion Map

Informal description

The canonical inclusion map from a submodule $p$ to its ambient module $M$ is injective. That is, for any $x, y \in p$, if $x = y$ as elements of $M$, then $x = y$ in $p$.

Submodule.coe_sum theorem

(x : ι → p) (s : Finset ι) : ↑(∑ i ∈ s, x i) = ∑ i ∈ s, (x i : M)

Full source

/-- Note the `AddSubmonoid` version of this lemma is called `AddSubmonoid.coe_finset_sum`. -/
theorem coe_sum (x : ι → p) (s : Finset ι) : ↑(∑ i ∈ s, x i) = ∑ i ∈ s, (x i : M) :=
  map_sum p.subtype _ _

Inclusion Map Preserves Finite Sums in Submodules

Informal description

For any family of elements $x : \iota \to p$ in a submodule $p$ of a module $M$ over a semiring $R$, and for any finite set $s \subseteq \iota$, the image under the inclusion map of the sum $\sum_{i \in s} x_i$ in $p$ is equal to the sum $\sum_{i \in s} x_i$ computed in the ambient module $M$.

Submodule.instAddActionSubtypeMem instance

[AddAction M α] : AddAction p α

Full source

/-- The action by a submodule is the action by the underlying module. -/
instance [AddAction M α] : AddAction p α :=
  AddAction.compHom _ p.subtype.toAddMonoidHom

Additive Action Inherited by Submodules

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, and any type $\alpha$ with an additive action by $M$, the submodule $p$ inherits an additive action on $\alpha$ through the inclusion map $p \hookrightarrow M$.

LinearMap.domRestrict definition

(f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) : p →ₛₗ[σ₁₂] M₂

Full source

/-- The restriction of a linear map `f : M → M₂` to a submodule `p ⊆ M` gives a linear map
`p → M₂`. -/
def domRestrict (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) : p →ₛₗ[σ₁₂] M₂ :=
  f.comp p.subtype

Domain restriction of a semilinear map to a submodule

Informal description

Given a semilinear map $f \colon M \to M₂$ and a submodule $p \subseteq M$, the domain restriction of $f$ to $p$ is the semilinear map obtained by composing $f$ with the inclusion map $p \hookrightarrow M$. More precisely, for any $x \in p$, the restricted map sends $x$ to $f(x) \in M₂$.

LinearMap.domRestrict_apply theorem

(f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) (x : p) : f.domRestrict p x = f x

Full source

@[simp]
theorem domRestrict_apply (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) (x : p) :
    f.domRestrict p x = f x :=
  rfl

Evaluation of Domain-Restricted Semilinear Map on Submodule Elements: $f|_{p}(x) = f(x)$

Informal description

Let $R$ and $R₂$ be semirings, $M$ be an $R$-module, $M₂$ be an $R₂$-module, and $\sigma₁₂ \colon R \to R₂$ be a ring homomorphism. Given a $\sigma₁₂$-semilinear map $f \colon M \to M₂$ and a submodule $p \subseteq M$, for any element $x \in p$, the domain-restricted map $f|_{p}$ satisfies $f|_{p}(x) = f(x)$.

LinearMap.codRestrict definition

(p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) (h : ∀ c, f c ∈ p) : M →ₛₗ[σ₁₂] p

Full source

/-- A linear map `f : M₂ → M` whose values lie in a submodule `p ⊆ M` can be restricted to a
linear map M₂ → p.

See also `LinearMap.codLift`. -/
def codRestrict (p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) (h : ∀ c, f c ∈ p) : M →ₛₗ[σ₁₂] p where
  toFun c := ⟨f c, h c⟩
  map_add' _ _ := by simp
  map_smul' _ _ := by simp

Codomain restriction of a semilinear map to a submodule

Informal description

Given a submodule $p$ of $M₂$ and a semilinear map $f : M → M₂$ such that $f(c) \in p$ for all $c \in M$, the function restricts $f$ to a semilinear map from $M$ to $p$. More precisely, for any $c \in M$, the restricted map sends $c$ to $\langle f(c), h(c) \rangle \in p$, where $h$ is the proof that $f(c) \in p$.

LinearMap.codRestrict_apply theorem

(p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) {h} (x : M) : (codRestrict p f h x : M₂) = f x

Full source

@[simp]
theorem codRestrict_apply (p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) {h} (x : M) :
    (codRestrict p f h x : M₂) = f x :=
  rfl

Codomain restriction preserves evaluation: $(\text{codRestrict}\, p\, f\, h\, x) = f(x)$

Informal description

Let $p$ be a submodule of $M₂$, $f : M \to M₂$ a semilinear map, and $h$ a proof that $f(c) \in p$ for all $c \in M$. Then for any $x \in M$, the underlying element of $M₂$ corresponding to $\text{codRestrict}\, p\, f\, h\, x$ is equal to $f(x)$. In other words, the codomain-restricted map $\text{codRestrict}\, p\, f\, h : M \to p$ satisfies $(\text{codRestrict}\, p\, f\, h\, x) = f(x)$ when viewed as an element of $M₂$.

LinearMap.comp_codRestrict theorem

 (p : Submodule R₃ M₃) (h : ∀ b, g b ∈ p) :
  ((codRestrict p g h).comp f : M →ₛₗ[σ₁₃] p) = codRestrict p (g.comp f) fun _ => h _

Full source

@[simp]
theorem comp_codRestrict (p : Submodule R₃ M₃) (h : ∀ b, g b ∈ p) :
    ((codRestrict p g h).comp f : M →ₛₗ[σ₁₃] p) = codRestrict p (g.comp f) fun _ => h _ :=
  ext fun _ => rfl

Composition of Codomain-Restricted Semilinear Maps

Informal description

Let $R₁$, $R₂$, and $R₃$ be semirings, and let $M$, $M₂$, and $M₃$ be modules over $R₁$, $R₂$, and $R₃$ respectively. Let $\sigma₁₂ : R₁ \to R₂$ and $\sigma₂₃ : R₂ \to R₃$ be ring homomorphisms, and let $\sigma₁₃ = \sigma₂₃ \circ \sigma₁₂$. Given a submodule $p$ of $M₃$, a semilinear map $g : M₂ \to M₃$ such that $g(b) \in p$ for all $b \in M₂$, and a semilinear map $f : M \to M₂$, the composition of the codomain-restricted map $\text{codRestrict}\, p\, g\, h$ with $f$ is equal to the codomain restriction of $g \circ f$ to $p$. That is, $$(\text{codRestrict}\, p\, g\, h) \circ f = \text{codRestrict}\, p\, (g \circ f)\, (\lambda x, h (f x)).$$

LinearMap.subtype_comp_codRestrict theorem

(p : Submodule R₂ M₂) (h : ∀ b, f b ∈ p) : p.subtype.comp (codRestrict p f h) = f

Full source

@[simp]
theorem subtype_comp_codRestrict (p : Submodule R₂ M₂) (h : ∀ b, f b ∈ p) :
    p.subtype.comp (codRestrict p f h) = f :=
  ext fun _ => rfl

Composition of Inclusion with Codomain Restriction Equals Original Map

Informal description

Let $p$ be a submodule of $M₂$ over a semiring $R₂$, and let $f : M \to M₂$ be a linear map such that $f(b) \in p$ for all $b \in M$. Then the composition of the inclusion map $p \hookrightarrow M₂$ with the codomain restriction of $f$ to $p$ equals $f$ itself. In symbols, if $\iota : p \hookrightarrow M₂$ denotes the inclusion map and $f|_p : M \to p$ is the codomain restriction of $f$, then $\iota \circ f|_p = f$.

LinearMap.codLift definition

: M →ₛₗ[σ₁₂] M₂'

Full source

/-- A linear map `f : M → M₂` whose values lie in the image of an injective linear map
`p : M₂' → M₂` admits a unique lift to a linear map `M → M₂'`. -/
noncomputable def codLift :
    M →ₛₗ[σ₁₂] M₂' where
  toFun c := (h c).choose
  map_add' b c := by apply hp; simp_rw [map_add, (h _).choose_spec, ← map_add, (h _).choose_spec]
  map_smul' r c := by apply hp; simp_rw [map_smul, (h _).choose_spec, LinearMap.map_smulₛₗ]

Lift of a linear map through an injective codomain map

Informal description

Given a linear map $ f : M \to M₂ $ whose values lie in the image of an injective linear map $ p : M₂' \to M₂ $, there exists a unique lift of $ f $ to a linear map $ M \to M₂' $. This lift is constructed by choosing for each $ x \in M $ a preimage of $ f(x) $ under $ p $, and using the injectivity of $ p $ to ensure the linearity of the resulting map.

LinearMap.codLift_apply theorem

(x : M) : (f.codLift p hp h x) = (h x).choose

Full source

@[simp] theorem codLift_apply (x : M) :
    (f.codLift p hp h x) = (h x).choose :=
  rfl

Evaluation of Linear Map Lift Through Injective Codomain Map

Informal description

Let $f : M \to M₂$ be a linear map, $p : M₂' \to M₂$ be an injective linear map, and $h : \forall x \in M, f(x) \in \text{range}(p)$. For any $x \in M$, the lift of $f$ through $p$ evaluated at $x$ equals a chosen preimage of $f(x)$ under $p$, i.e., $(f.\text{codLift}\ p\ hp\ h)(x) = (h\ x).\text{choose}$.

LinearMap.comp_codLift theorem

: p.comp (f.codLift p hp h) = f

Full source

@[simp]
theorem comp_codLift :
    p.comp (f.codLift p hp h) = f := by
  ext x
  rw [comp_apply, codLift_apply, (h x).choose_spec]

Composition of Linear Map with Its Lift Through Injective Codomain Map Equals Original Map

Informal description

Let $f : M \to M₂$ be a linear map, $p : M₂' \to M₂$ be an injective linear map, and $h : \forall x \in M, f(x) \in \text{range}(p)$. Then the composition of $p$ with the lift of $f$ through $p$ equals $f$, i.e., $p \circ (f.\text{codLift}\ p\ hp\ h) = f$.

LinearMap.restrict definition

(f : M →ₗ[R] M₁) {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) : p →ₗ[R] q

Full source

/-- Restrict domain and codomain of a linear map. -/
def restrict (f : M →ₗ[R] M₁) {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) :
    p →ₗ[R] q :=
  (f.domRestrict p).codRestrict q <| SetLike.forall.2 hf

Restriction of a linear map to submodules

Informal description

Given a linear map $f \colon M \to M₁$ over a semiring $R$, and submodules $p \subseteq M$ and $q \subseteq M₁$ such that $f(x) \in q$ for all $x \in p$, the restriction of $f$ to $p$ and $q$ is the linear map obtained by first restricting the domain of $f$ to $p$ and then restricting the codomain to $q$. More precisely, for any $x \in p$, the restricted map sends $x$ to $\langle f(x), hf(x) \rangle \in q$, where $hf$ is the proof that $f(x) \in q$.

LinearMap.restrict_coe_apply theorem

 (f : M →ₗ[R] M₁) {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) (x : p) : ↑(f.restrict hf x) = f x

Full source

@[simp]
theorem restrict_coe_apply (f : M →ₗ[R] M₁) {p : Submodule R M} {q : Submodule R M₁}
    (hf : ∀ x ∈ p, f x ∈ q) (x : p) : ↑(f.restrict hf x) = f x :=
  rfl

Coefficient of Restricted Linear Map Equals Original Map

Informal description

Let $R$ be a semiring, $M$ and $M₁$ be $R$-modules, and $f \colon M \to M₁$ be a linear map. For any submodules $p \subseteq M$ and $q \subseteq M₁$ such that $f(x) \in q$ for all $x \in p$, and for any $x \in p$, the image of $x$ under the restricted linear map $f|_{p,q}$ (considered as an element of $M₁$) equals $f(x)$. In symbols: if $f|_{p,q} \colon p \to q$ is the restriction of $f$ to $p$ and $q$, then for any $x \in p$, we have $f|_{p,q}(x) = f(x)$ in $M₁$.

LinearMap.restrict_apply theorem

 {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) (x : p) :
  f.restrict hf x = ⟨f x, hf x.1 x.2⟩

Full source

theorem restrict_apply {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁}
    (hf : ∀ x ∈ p, f x ∈ q) (x : p) : f.restrict hf x = ⟨f x, hf x.1 x.2⟩ :=
  rfl

Evaluation of Restricted Linear Map on Submodules

Informal description

Let $R$ be a semiring, $M$ and $M₁$ be $R$-modules, and $f \colon M \to M₁$ be a linear map. Given submodules $p \subseteq M$ and $q \subseteq M₁$ such that $f(x) \in q$ for all $x \in p$, the restricted linear map $f_{\text{restrict}} \colon p \to q$ satisfies $f_{\text{restrict}}(x) = \langle f(x), hf(x) \rangle$ for any $x \in p$, where $hf$ is the proof that $f(x) \in q$.

LinearMap.restrict_commute theorem

 {f g : M →ₗ[R] M} (h : Commute f g) {p : Submodule R M} (hf : MapsTo f p p) (hg : MapsTo g p p) :
  Commute (f.restrict hf) (g.restrict hg)

Full source

lemma restrict_commute {f g : M →ₗ[R] M} (h : Commute f g) {p : Submodule R M}
    (hf : MapsTo f p p) (hg : MapsTo g p p) :
    Commute (f.restrict hf) (g.restrict hg) := by
  change (f ∘ₗ g).restrict (hf.comp hg) = (g ∘ₗ f).restrict (hg.comp hf)
  congr 1

Restriction of Commuting Linear Maps Preserves Commutation

Informal description

Let $M$ be a module over a semiring $R$, and let $f, g \colon M \to M$ be commuting linear maps (i.e., $f \circ g = g \circ f$). For any submodule $p \subseteq M$ such that $f$ and $g$ both map $p$ into itself (i.e., $f(x) \in p$ and $g(x) \in p$ for all $x \in p$), the restricted maps $f|_p \colon p \to p$ and $g|_p \colon p \to p$ also commute.

LinearMap.subtype_comp_restrict theorem

 {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) :
  q.subtype.comp (f.restrict hf) = f.domRestrict p

Full source

theorem subtype_comp_restrict {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁}
    (hf : ∀ x ∈ p, f x ∈ q) : q.subtype.comp (f.restrict hf) = f.domRestrict p :=
  rfl

Composition of Submodule Inclusion with Restricted Linear Map Equals Domain Restriction

Informal description

Let $R$ be a semiring, $M$ and $M₁$ be $R$-modules, $p \subseteq M$ and $q \subseteq M₁$ be submodules, and $f \colon M \to M₁$ be a linear map such that $f(x) \in q$ for all $x \in p$. Then the composition of the inclusion map $q \hookrightarrow M₁$ with the restriction of $f$ to $p$ and $q$ equals the domain restriction of $f$ to $p$. In symbols: $$ \iota_q \circ f\big|_p^q = f\big|_p $$ where $\iota_q \colon q \hookrightarrow M₁$ is the inclusion map and $f\big|_p^q \colon p \to q$ is the restriction of $f$ to $p$ and $q$.

LinearMap.restrict_eq_codRestrict_domRestrict theorem

 {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) :
  f.restrict hf = (f.domRestrict p).codRestrict q fun x => hf x.1 x.2

Full source

theorem restrict_eq_codRestrict_domRestrict {f : M →ₗ[R] M₁} {p : Submodule R M}
    {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) :
    f.restrict hf = (f.domRestrict p).codRestrict q fun x => hf x.1 x.2 :=
  rfl

Equality of Restricted Linear Map as Composition of Domain and Codomain Restrictions

Informal description

Let $R$ be a semiring, $M$ and $M₁$ be $R$-modules, and $p \subseteq M$, $q \subseteq M₁$ be submodules. Given a linear map $f \colon M \to M₁$ such that $f(x) \in q$ for all $x \in p$, the restriction of $f$ to $p$ and $q$ is equal to the composition of the domain restriction of $f$ to $p$ followed by the codomain restriction to $q$. More precisely, we have: $$ f|_{p,q} = (f|_p)|^q $$ where: - $f|_{p,q}$ denotes the restriction of $f$ to $p$ and $q$, - $f|_p$ denotes the domain restriction of $f$ to $p$, - $(\cdot)|^q$ denotes the codomain restriction to $q$.

LinearMap.restrict_eq_domRestrict_codRestrict theorem

 {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x, f x ∈ q) :
  (f.restrict fun x _ => hf x) = (f.codRestrict q hf).domRestrict p

Full source

theorem restrict_eq_domRestrict_codRestrict {f : M →ₗ[R] M₁} {p : Submodule R M}
    {q : Submodule R M₁} (hf : ∀ x, f x ∈ q) :
    (f.restrict fun x _ => hf x) = (f.codRestrict q hf).domRestrict p :=
  rfl

Equality of Restricted Linear Map and Composed Domain-Codomain Restrictions

Informal description

Let $f \colon M \to M₁$ be a linear map over a semiring $R$, and let $p \subseteq M$ and $q \subseteq M₁$ be submodules such that $f(x) \in q$ for all $x \in M$. Then the restriction of $f$ to $p$ and $q$ is equal to the composition of the codomain restriction of $f$ to $q$ followed by the domain restriction to $p$. That is, \[ f_{\text{restrict}} = (f_{\text{codRestrict } q})_{\text{domRestrict } p}. \]

LinearMap.sum_apply theorem

(t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) (b : M) : (∑ d ∈ t, f d) b = ∑ d ∈ t, f d b

Full source

theorem sum_apply (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) (b : M) :
    (∑ d ∈ t, f d) b = ∑ d ∈ t, f d b :=
  _root_.map_sum ((AddMonoidHom.eval b).comp toAddMonoidHom') f _

Sum of Linear Maps Equals Sum of Evaluations

Informal description

For any finite set $t$ of indices and any family of linear maps $f_i \colon M \to M₂$ indexed by $i \in t$, the evaluation of the sum of these linear maps at a point $b \in M$ is equal to the sum of the evaluations of each individual linear map at $b$. That is, \[ \left(\sum_{i \in t} f_i\right)(b) = \sum_{i \in t} f_i(b). \]

LinearMap.coeFn_sum theorem

 {ι : Type*} (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) : ⇑(∑ i ∈ t, f i) = ∑ i ∈ t, (f i : M → M₂)

Full source

@[simp, norm_cast]
theorem coeFn_sum {ι : Type*} (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) :
    ⇑(∑ i ∈ t, f i) = ∑ i ∈ t, (f i : M → M₂) :=
  _root_.map_sum
    (show AddMonoidHom (M →ₛₗ[σ₁₂] M₂) (M → M₂)
      from { toFun := DFunLike.coe,
             map_zero' := rfl
             map_add' := fun _ _ => rfl }) _ _

Sum of Linear Maps Equals Sum of Evaluations

Informal description

For any finite set $t$ of indices and any family of linear maps $f_i : M \to M₂$ indexed by $i \in t$, the evaluation of the sum of these linear maps at a point $b \in M$ is equal to the sum of the evaluations of each individual linear map at $b$. That is, \[ \left(\sum_{i \in t} f_i\right)(b) = \sum_{i \in t} f_i(b). \]

Module.End.submodule_pow_eq_zero_of_pow_eq_zero theorem

 {N : Submodule R M} {g : Module.End R N} {G : Module.End R M} (h : G.comp N.subtype = N.subtype.comp g) {k : ℕ}
  (hG : G ^ k = 0) : g ^ k = 0

Full source

theorem _root_.Module.End.submodule_pow_eq_zero_of_pow_eq_zero {N : Submodule R M}
    {g : Module.End R N} {G : Module.End R M} (h : G.comp N.subtype = N.subtype.comp g) {k : ℕ}
    (hG : G ^ k = 0) : g ^ k = 0 := by
  ext m
  have hg : N.subtype.comp (g ^ k) m = 0 := by
    rw [← Module.End.commute_pow_left_of_commute h, hG, zero_comp, zero_apply]
  simpa using hg

Nilpotency of Submodule Endomorphism via Nilpotency of Ambient Endomorphism

Informal description

Let $M$ be a module over a semiring $R$, and let $N$ be a submodule of $M$. Given two endomorphisms $g \colon N \to N$ and $G \colon M \to M$ such that $G \circ \iota = \iota \circ g$, where $\iota \colon N \hookrightarrow M$ is the inclusion map, if $G^k = 0$ for some natural number $k$, then $g^k = 0$.

Module.End.pow_apply_mem_of_forall_mem theorem

{p : Submodule R M} (n : ℕ) (h : ∀ x ∈ p, f' x ∈ p) (x : M) (hx : x ∈ p) : (f' ^ n) x ∈ p

Full source

theorem _root_.Module.End.pow_apply_mem_of_forall_mem {p : Submodule R M} (n : ℕ)
    (h : ∀ x ∈ p, f' x ∈ p) (x : M) (hx : x ∈ p) : (f' ^ n) x ∈ p := by
  induction n generalizing x with
  | zero => simpa
  | succ n ih =>
    simpa only [iterate_succ, coe_comp, Function.comp_apply, restrict_apply] using ih _ (h _ hx)

Iterated Linear Map Preserves Submodule: $f'^n(x) \in p$ for $x \in p$

Informal description

Let $R$ be a semiring, $M$ be an $R$-module, and $p$ be a submodule of $M$. For any linear endomorphism $f'$ of $M$ that preserves $p$ (i.e., $f'(x) \in p$ for all $x \in p$), any natural number $n \in \mathbb{N}$, and any element $x \in p$, the $n$-th iterate $f'^n(x)$ belongs to $p$.

LinearMap.domRestrict' definition

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

Full source

/-- Alternative version of `domRestrict` as a linear map. -/
def domRestrict' (p : Submodule R M) : (M →ₗ[R] M₂) →ₗ[R] p →ₗ[R] M₂ where
  toFun φ := φ.domRestrict p
  map_add' := by simp [LinearMap.ext_iff]
  map_smul' := by simp [LinearMap.ext_iff]

Linear map of domain restriction to a submodule

Informal description

The linear map that takes a linear map $f \colon M \to M₂$ and returns its restriction to the submodule $p \subseteq M$, viewed as a linear map $p \to M₂$. More precisely, for any linear map $f \colon M \to M₂$ and any $x \in p$, the restricted map sends $x$ to $f(x) \in M₂$.

LinearMap.domRestrict'_apply theorem

(f : M →ₗ[R] M₂) (p : Submodule R M) (x : p) : domRestrict' p f x = f x

Full source

@[simp]
theorem domRestrict'_apply (f : M →ₗ[R] M₂) (p : Submodule R M) (x : p) :
    domRestrict' p f x = f x :=
  rfl

Restriction of Linear Map to Submodule Preserves Values: $\text{domRestrict'}_p(f)(x) = f(x)$

Informal description

Let $R$ be a semiring, $M$ and $M₂$ be $R$-modules, and $p$ be a submodule of $M$. For any linear map $f \colon M \to M₂$ and any element $x \in p$, the restriction of $f$ to $p$ evaluated at $x$ equals $f(x)$, i.e., $\text{domRestrict'}_p(f)(x) = f(x)$.

Submodule.inclusion definition

(h : p ≤ p') : p →ₗ[R] p'

Full source

/-- If two submodules `p` and `p'` satisfy `p ⊆ p'`, then `inclusion p p'` is the linear map version
of this inclusion. -/
def inclusion (h : p ≤ p') : p →ₗ[R] p' :=
  p.subtype.codRestrict p' fun ⟨_, hx⟩ => h hx

Inclusion map of submodules

Informal description

Given two submodules $p$ and $p'$ of an $R$-module $M$ with $p \subseteq p'$, the inclusion map $\text{inclusion} \colon p \to p'$ is the linear map that embeds $p$ into $p'$ by sending each element $x \in p$ to itself (viewed as an element of $p'$). More precisely, for any $x \in p$, the inclusion map sends $x$ to $\langle x, h(x.2) \rangle \in p'$, where $h$ is the proof that $p \subseteq p'$ and $x.2$ is the proof that $x \in p$.

Submodule.coe_inclusion theorem

(h : p ≤ p') (x : p) : (inclusion h x : M) = x

Full source

@[simp]
theorem coe_inclusion (h : p ≤ p') (x : p) : (inclusion h x : M) = x :=
  rfl

Inclusion Map Preserves Elements: $\text{inclusion}(x) = x$

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $p, p'$ submodules of $M$ with $p \subseteq p'$. For any element $x \in p$, the image of $x$ under the inclusion map $\text{inclusion} \colon p \to p'$ (viewed as an element of $M$) equals $x$ itself, i.e., $\text{inclusion}(x) = x$ in $M$.

Submodule.inclusion_apply theorem

(h : p ≤ p') (x : p) : inclusion h x = ⟨x, h x.2⟩

Full source

theorem inclusion_apply (h : p ≤ p') (x : p) : inclusion h x = ⟨x, h x.2⟩ :=
  rfl

Application of Submodule Inclusion Map

Informal description

Let $M$ be a module over a semiring $R$, and let $p$ and $p'$ be submodules of $M$ such that $p \subseteq p'$. For any element $x \in p$, the inclusion map $\text{inclusion} \colon p \to p'$ satisfies $\text{inclusion}(x) = \langle x, h(x.2) \rangle$, where $h$ is the proof that $p \subseteq p'$ and $x.2$ is the proof that $x \in p$.

Submodule.inclusion_injective theorem

(h : p ≤ p') : Function.Injective (inclusion h)

Full source

theorem inclusion_injective (h : p ≤ p') : Function.Injective (inclusion h) := fun _ _ h =>
  Subtype.val_injective (Subtype.mk.inj h)

Injectivity of Submodule Inclusion Map

Informal description

For any submodules $p$ and $p'$ of an $R$-module $M$ such that $p \subseteq p'$, the inclusion map $\text{inclusion} \colon p \to p'$ is injective. That is, for any $x, y \in p$, if $\text{inclusion}(x) = \text{inclusion}(y)$, then $x = y$.

Submodule.subtype_comp_inclusion theorem

(p q : Submodule R M) (h : p ≤ q) : q.subtype.comp (inclusion h) = p.subtype

Full source

theorem subtype_comp_inclusion (p q : Submodule R M) (h : p ≤ q) :
    q.subtype.comp (inclusion h) = p.subtype := by
  ext ⟨b, hb⟩
  rfl

Compatibility of Submodule Inclusions with Canonical Embeddings

Informal description

Let $M$ be a module over a semiring $R$, and let $p$ and $q$ be submodules of $M$ with $p \subseteq q$. Then the composition of the inclusion map $\text{inclusion} \colon p \to q$ with the canonical embedding $q \hookrightarrow M$ equals the canonical embedding $p \hookrightarrow M$. In other words, the following diagram commutes: $$\begin{array}{ccc} p & \xrightarrow{\text{inclusion}} & q \\ & \searrow & \downarrow \\ && M \end{array}$$ where the downward maps are the canonical submodule embeddings.

Mathlib.Algebra.Module.Submodule.LinearMap

Main declarations

Tags