Mathlib.LinearAlgebra.Finsupp.LinearCombination

Finsupp.linearCombination definition

: (α →₀ R) →ₗ[R] M

Full source

/-- Interprets (l : α →₀ R) as a linear combination of the elements in the family (v : α → M) and
    evaluates this linear combination. -/
def linearCombination : (α →₀ R) →ₗ[R] M :=
  Finsupp.lsum ℕ fun i => LinearMap.id.smulRight (v i)

Linear combination of a family of module elements

Informal description

Given a semiring $R$, an additive commutative monoid $M$ with a module structure over $R$, and a family of elements $(v_i)_{i \in \alpha}$ in $M$, the linear combination function maps any finitely supported function $l : \alpha \to_{\text{f}} R$ to the element $\sum_{i \in \alpha} l(i) \cdot v_i$ in $M$. This is a linear map from the module of finitely supported functions $\alpha \to_{\text{f}} R$ to $M$.

Finsupp.linearCombination_apply theorem

(l : α →₀ R) : linearCombination R v l = l.sum fun i a => a • v i

Full source

theorem linearCombination_apply (l : α →₀ R) : linearCombination R v l = l.sum fun i a => a • v i :=
  rfl

Linear Combination Formula for Finitely Supported Functions

Informal description

Given a semiring $R$, an $R$-module $M$, and a family of elements $(v_i)_{i \in \alpha}$ in $M$, the linear combination of these elements with coefficients given by a finitely supported function $l : \alpha \to_{\text{f}} R$ is equal to the sum $\sum_{i \in \alpha} l(i) \cdot v_i$.

Finsupp.linearCombination_apply_of_mem_supported theorem

 {l : α →₀ R} {s : Finset α} (hs : l ∈ supported R R (↑s : Set α)) : linearCombination R v l = s.sum fun i => l i • v i

Full source

theorem linearCombination_apply_of_mem_supported {l : α →₀ R} {s : Finset α}
    (hs : l ∈ supported R R (↑s : Set α)) : linearCombination R v l = s.sum fun i => l i • v i :=
  Finset.sum_subset hs fun x _ hxg =>
    show l x • v x = 0 by rw [not_mem_support_iff.1 hxg, zero_smul]

Linear Combination over Finite Support

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $v \colon \alpha \to M$ a family of elements in $M$. For any finitely supported function $l \colon \alpha \to_{\text{f}} R$ whose support is contained in a finite set $s \subseteq \alpha$, the linear combination $\sum_{i \in \alpha} l(i) \cdot v_i$ equals the finite sum $\sum_{i \in s} l(i) \cdot v_i$.

Finsupp.linearCombination_single theorem

(c : R) (a : α) : linearCombination R v (single a c) = c • v a

Full source

@[simp]
theorem linearCombination_single (c : R) (a : α) :
    linearCombination R v (single a c) = c • v a := by
  simp [linearCombination_apply, sum_single_index]

Linear Combination of a Single Element: $(\text{single } a c) \cdot v = c \cdot v(a)$

Informal description

For any scalar $c$ in a semiring $R$ and any element $a$ in a type $\alpha$, the linear combination of a family of module elements $v : \alpha \to M$ evaluated at the finitely supported function `single a c` (which is $c$ at $a$ and zero elsewhere) equals the scalar multiple $c \cdot v(a)$.

Finsupp.linearCombination_zero_apply theorem

(x : α →₀ R) : (linearCombination R (0 : α → M)) x = 0

Full source

theorem linearCombination_zero_apply (x : α →₀ R) : (linearCombination R (0 : α → M)) x = 0 := by
  simp [linearCombination_apply]

Linear Combination of Zero Family Yields Zero

Informal description

For any finitely supported function $x : \alpha \to_{\text{f}} R$, the linear combination of the zero family $(0 : \alpha \to M)$ evaluated at $x$ is equal to the zero element in $M$, i.e., $\sum_{i \in \alpha} x(i) \cdot 0 = 0$.

Finsupp.linearCombination_zero theorem

: linearCombination R (0 : α → M) = 0

Full source

@[simp]
theorem linearCombination_zero : linearCombination R (0 : α → M) = 0 :=
  LinearMap.ext (linearCombination_zero_apply R)

Linear Combination of Zero Family is Zero Map

Informal description

The linear combination of the zero family $(0 : \alpha \to M)$ is the zero linear map, i.e., $\text{linearCombination}_R (0) = 0$.

Finsupp.linearCombination_single_index theorem

(c : M) (a : α) (f : α →₀ R) [DecidableEq α] : linearCombination R (Pi.single a c) f = f a • c

Full source

@[simp]
theorem linearCombination_single_index (c : M) (a : α) (f : α →₀ R) [DecidableEq α] :
    linearCombination R (Pi.single a c) f = f a • c := by
  rw [linearCombination_apply, sum_eq_single a, Pi.single_eq_same]
  · exact fun i _ hi ↦ by rw [Pi.single_eq_of_ne hi, smul_zero]
  · exact fun _ ↦ by simp only [single_eq_same, zero_smul]

Linear Combination of a Single Element Family

Informal description

Let $R$ be a semiring, $M$ an $R$-module, $\alpha$ a type, and $c \in M$. For any finitely supported function $f : \alpha \to_{\text{f}} R$ and any $a \in \alpha$, the linear combination of the family $\text{Pi.single}(a, c) : \alpha \to M$ evaluated at $f$ equals the scalar multiple $f(a) \cdot c$. That is, $$\sum_{i \in \alpha} f(i) \cdot \text{Pi.single}(a, c)(i) = f(a) \cdot c.$$

Finsupp.linearCombination_linear_comp theorem

(f : M →ₗ[R] M') : linearCombination R (f ∘ v) = f ∘ₗ linearCombination R v

Full source

theorem linearCombination_linear_comp (f : M →ₗ[R] M') :
    linearCombination R (f ∘ v) = f ∘ₗ linearCombination R v := by
  ext
  simp [linearCombination_apply]

Linear Combination Commutes with Linear Maps

Informal description

Let $R$ be a semiring, $M$ and $M'$ be $R$-modules, and $v : \alpha \to M$ be a family of elements in $M$. For any linear map $f : M \to M'$, the linear combination of the family $(f \circ v) : \alpha \to M'$ equals the composition of $f$ with the linear combination of $v$. That is, the following diagram commutes: $$\text{linearCombination}_R (f \circ v) = f \circ \text{linearCombination}_R v$$

Finsupp.apply_linearCombination theorem

(f : M →ₗ[R] M') (v) (l : α →₀ R) : f (linearCombination R v l) = linearCombination R (f ∘ v) l

Full source

theorem apply_linearCombination (f : M →ₗ[R] M') (v) (l : α →₀ R) :
    f (linearCombination R v l) = linearCombination R (f ∘ v) l :=
  congr($(linearCombination_linear_comp R f) l).symm

Linear Map Commutes with Linear Combination

Informal description

Let $R$ be a semiring, $M$ and $M'$ be $R$-modules, and $v : \alpha \to M$ be a family of elements in $M$. For any linear map $f : M \to M'$ and any finitely supported function $l : \alpha \to_{\text{f}} R$, we have $$ f\left(\sum_{i \in \alpha} l(i) \cdot v(i)\right) = \sum_{i \in \alpha} l(i) \cdot f(v(i)). $$

Finsupp.apply_linearCombination_id theorem

(f : M →ₗ[R] M') (l : M →₀ R) : f (linearCombination R _root_.id l) = linearCombination R f l

Full source

theorem apply_linearCombination_id (f : M →ₗ[R] M') (l : M →₀ R) :
    f (linearCombination R _root_.id l) = linearCombination R f l :=
  apply_linearCombination ..

Linear Map Commutes with Linear Combination of Identity Family

Informal description

Let $R$ be a semiring, $M$ and $M'$ be $R$-modules, and $f : M \to M'$ be a linear map. For any finitely supported function $l : M \to_{\text{f}} R$, we have $$ f\left(\sum_{x \in M} l(x) \cdot x\right) = \sum_{x \in M} l(x) \cdot f(x). $$

Finsupp.linearCombination_unique theorem

[Unique α] (l : α →₀ R) (v : α → M) : linearCombination R v l = l default • v default

Full source

theorem linearCombination_unique [Unique α] (l : α →₀ R) (v : α → M) :
    linearCombination R v l = l default • v default := by
  rw [← linearCombination_single, ← unique_single l]

Linear Combination over a Unique Index Type: $\sum_{i \in \alpha} l(i) \cdot v(i) = l(\text{default}) \cdot v(\text{default})$

Informal description

Let $\alpha$ be a type with a unique element, $R$ a semiring, and $M$ an $R$-module. For any finitely supported function $l \colon \alpha \to_{\text{f}} R$ and any family of elements $v \colon \alpha \to M$, the linear combination $\sum_{i \in \alpha} l(i) \cdot v(i)$ equals $l(\text{default}) \cdot v(\text{default})$, where $\text{default}$ is the unique element of $\alpha$.

Finsupp.linearCombination_surjective theorem

(h : Function.Surjective v) : Function.Surjective (linearCombination R v)

Full source

theorem linearCombination_surjective (h : Function.Surjective v) :
    Function.Surjective (linearCombination R v) := by
  intro x
  obtain ⟨y, hy⟩ := h x
  exact ⟨single y 1, by simp [hy]⟩

Surjectivity of Linear Combination Map for Surjective Families

Informal description

Let $R$ be a semiring, $M$ be an $R$-module, and $\alpha$ be a type. Given a surjective function $v : \alpha \to M$, the linear combination map $\text{linearCombination}_R v : (\alpha \to_{\text{f}} R) \to M$ is also surjective. Here, $\text{linearCombination}_R v$ sends a finitely supported function $l : \alpha \to_{\text{f}} R$ to the sum $\sum_{i \in \alpha} l(i) \cdot v(i)$.

Finsupp.linearCombination_range theorem

(h : Function.Surjective v) : LinearMap.range (linearCombination R v) = ⊤

Full source

theorem linearCombination_range (h : Function.Surjective v) :
    LinearMap.range (linearCombination R v) = ⊤ :=
  range_eq_top.2 <| linearCombination_surjective R h

Range of Linear Combination Map is Entire Module for Surjective Families

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $\alpha$ a type. Given a surjective function $v : \alpha \to M$, the range of the linear combination map $\text{linearCombination}_R\, v : (\alpha \to_{\text{f}} R) \to M$ is equal to the entire module $M$. In other words, the linear combination map is surjective when $v$ is surjective.

Finsupp.linearCombination_id_surjective theorem

(M) [AddCommMonoid M] [Module R M] : Function.Surjective (linearCombination R (id : M → M))

Full source

/-- Any module is a quotient of a free module. This is stated as surjectivity of
`Finsupp.linearCombination R id : (M →₀ R) →ₗ[R] M`. -/
theorem linearCombination_id_surjective (M) [AddCommMonoid M] [Module R M] :
    Function.Surjective (linearCombination R (id : M → M)) :=
  linearCombination_surjective R Function.surjective_id

Surjectivity of the Canonical Linear Combination Map for Free Modules

Informal description

For any semiring $R$ and any $R$-module $M$, the linear combination map $\text{linearCombination}_R\, \mathrm{id} \colon (M \to_{\text{f}} R) \to M$ is surjective. Here, $\text{linearCombination}_R\, \mathrm{id}$ sends a finitely supported function $l \colon M \to_{\text{f}} R$ to the sum $\sum_{x \in M} l(x) \cdot x$.

Finsupp.range_linearCombination theorem

: LinearMap.range (linearCombination R v) = span R (range v)

Full source

theorem range_linearCombination : LinearMap.range (linearCombination R v) = span R (range v) := by
  ext x
  constructor
  · intro hx
    rw [LinearMap.mem_range] at hx
    rcases hx with ⟨l, hl⟩
    rw [← hl]
    rw [linearCombination_apply]
    exact sum_mem fun i _ => Submodule.smul_mem _ _ (subset_span (mem_range_self i))
  · apply span_le.2
    intro x hx
    rcases hx with ⟨i, hi⟩
    rw [SetLike.mem_coe, LinearMap.mem_range]
    use single i 1
    simp [hi]

Range of Linear Combination Equals Span of Vector Family

Informal description

For a semiring $R$, an $R$-module $M$, and a family of vectors $(v_i)_{i \in \alpha}$ in $M$, the range of the linear combination map $\text{linearCombination}_R\, v$ is equal to the $R$-linear span of the range of $v$. That is: \[ \text{range}\, (\text{linearCombination}_R\, v) = \text{span}_R\, (\text{range}\, v) \]

Finsupp.lmapDomain_linearCombination theorem

 (f : α → α') (g : M →ₗ[R] M') (h : ∀ i, g (v i) = v' (f i)) :
  (linearCombination R v').comp (lmapDomain R R f) = g.comp (linearCombination R v)

Full source

theorem lmapDomain_linearCombination (f : α → α') (g : M →ₗ[R] M') (h : ∀ i, g (v i) = v' (f i)) :
    (linearCombination R v').comp (lmapDomain R R f) = g.comp (linearCombination R v) := by
  ext l
  simp [linearCombination_apply, Finsupp.sum_mapDomain_index, add_smul, h]

Naturality of Linear Combination under Domain Mapping and Linear Transformation

Informal description

Let $R$ be a semiring, $M$ and $M'$ be $R$-modules, and $\alpha$ and $\alpha'$ be types. Given a function $f \colon \alpha \to \alpha'$, an $R$-linear map $g \colon M \to M'$, and a family of vectors $(v_i)_{i \in \alpha}$ in $M$ and $(v'_{j})_{j \in \alpha'}$ in $M'$ such that $g(v_i) = v'_{f(i)}$ for all $i \in \alpha$, the following diagram commutes: \[ \begin{CD} \alpha \to_{\text{f}} R @>{\text{linearCombination}_R\, v}>> M \\ @V{\text{lmapDomain}_R\, R\, f}VV @VV{g}V \\ \alpha' \to_{\text{f}} R @>{\text{linearCombination}_R\, v'}>> M' \end{CD} \] That is, the composition of the linear combination map for $v'$ with the domain mapping by $f$ equals the composition of $g$ with the linear combination map for $v$.

Finsupp.linearCombination_comp_lmapDomain theorem

(f : α → α') : (linearCombination R v').comp (Finsupp.lmapDomain R R f) = linearCombination R (v' ∘ f)

Full source

theorem linearCombination_comp_lmapDomain (f : α → α') :
    (linearCombination R v').comp (Finsupp.lmapDomain R R f) = linearCombination R (v' ∘ f) := by
  ext
  simp

Composition of Linear Combination with Domain Mapping Equals Linear Combination of Composed Family

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $v' \colon \alpha' \to M$ a family of elements in $M$. For any function $f \colon \alpha \to \alpha'$, the composition of the linear combination map for $v'$ with the linear domain mapping by $f$ equals the linear combination map for the family $v' \circ f$. That is, $$ \text{linearCombination}_R\, v' \circ \text{lmapDomain}_R\, R\, f = \text{linearCombination}_R\, (v' \circ f). $$

Finsupp.linearCombination_embDomain theorem

(f : α ↪ α') (l : α →₀ R) : (linearCombination R v') (embDomain f l) = (linearCombination R (v' ∘ f)) l

Full source

@[simp]
theorem linearCombination_embDomain (f : α ↪ α') (l : α →₀ R) :
    (linearCombination R v') (embDomain f l) = (linearCombination R (v' ∘ f)) l := by
  simp [linearCombination_apply, Finsupp.sum, support_embDomain, embDomain_apply]

Equality of Linear Combinations under Embedding of Finitely Supported Functions

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $v' \colon \alpha' \to M$ a family of elements in $M$. For any injective function embedding $f \colon \alpha \hookrightarrow \alpha'$ and any finitely supported function $l \colon \alpha \to_{\text{f}} R$, the linear combination of $v'$ evaluated at the embedded function $\text{embDomain}\, f\, l$ is equal to the linear combination of $v' \circ f$ evaluated at $l$, i.e., $$ \text{linearCombination}_R\, v'\, (\text{embDomain}\, f\, l) = \text{linearCombination}_R\, (v' \circ f)\, l. $$

Finsupp.linearCombination_mapDomain theorem

(f : α → α') (l : α →₀ R) : (linearCombination R v') (mapDomain f l) = (linearCombination R (v' ∘ f)) l

Full source

@[simp]
theorem linearCombination_mapDomain (f : α → α') (l : α →₀ R) :
    (linearCombination R v') (mapDomain f l) = (linearCombination R (v' ∘ f)) l :=
  LinearMap.congr_fun (linearCombination_comp_lmapDomain _ _) l

Equality of Linear Combinations under Domain Mapping of Finitely Supported Functions

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $v' \colon \alpha' \to M$ a family of elements in $M$. For any function $f \colon \alpha \to \alpha'$ and any finitely supported function $l \colon \alpha \to_{\text{f}} R$, the linear combination of $v'$ evaluated at the mapped function $\text{mapDomain}\, f\, l$ is equal to the linear combination of $v' \circ f$ evaluated at $l$, i.e., $$ \text{linearCombination}_R\, v'\, (\text{mapDomain}\, f\, l) = \text{linearCombination}_R\, (v' \circ f)\, l. $$

Finsupp.linearCombination_equivMapDomain theorem

(f : α ≃ α') (l : α →₀ R) : (linearCombination R v') (equivMapDomain f l) = (linearCombination R (v' ∘ f)) l

Full source

@[simp]
theorem linearCombination_equivMapDomain (f : α ≃ α') (l : α →₀ R) :
    (linearCombination R v') (equivMapDomain f l) = (linearCombination R (v' ∘ f)) l := by
  rw [equivMapDomain_eq_mapDomain, linearCombination_mapDomain]

Equivariance of Linear Combination under Domain Equivalence

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $v' \colon \alpha' \to M$ a family of elements in $M$. For any equivalence $f \colon \alpha \simeq \alpha'$ and any finitely supported function $l \colon \alpha \to_{\text{f}} R$, the linear combination of $v'$ evaluated at the domain-remapped function $\text{equivMapDomain}\, f\, l$ is equal to the linear combination of $v' \circ f$ evaluated at $l$, i.e., $$ \text{linearCombination}_R\, v'\, (\text{equivMapDomain}\, f\, l) = \text{linearCombination}_R\, (v' \circ f)\, l. $$

Finsupp.span_eq_range_linearCombination theorem

(s : Set M) : span R s = LinearMap.range (linearCombination R ((↑) : s → M))

Full source

/-- A version of `Finsupp.range_linearCombination` which is useful for going in the other
direction -/
theorem span_eq_range_linearCombination (s : Set M) :
    span R s = LinearMap.range (linearCombination R ((↑) : s → M)) := by
  rw [range_linearCombination, Subtype.range_coe_subtype, Set.setOf_mem_eq]

Span Equals Range of Linear Combination Map for Subset Inclusion

Informal description

For any subset $s$ of an $R$-module $M$, the $R$-linear span of $s$ is equal to the range of the linear combination map associated with the inclusion function $\iota : s \hookrightarrow M$. That is: \[ \text{span}_R(s) = \text{range}\, (\text{linearCombination}_R\, \iota) \] where $\text{linearCombination}_R\, \iota$ maps a finitely supported function $l : s \to_{\text{f}} R$ to the linear combination $\sum_{x \in s} l(x) \cdot x$ in $M$.

Finsupp.mem_span_iff_linearCombination theorem

(s : Set M) (x : M) : x ∈ span R s ↔ ∃ l : s →₀ R, linearCombination R (↑) l = x

Full source

theorem mem_span_iff_linearCombination (s : Set M) (x : M) :
    x ∈ span R sx ∈ span R s ↔ ∃ l : s →₀ R, linearCombination R (↑) l = x :=
  (SetLike.ext_iff.1 <| span_eq_range_linearCombination _ _) x

Characterization of Span Membership via Finite Linear Combinations on Subsets

Informal description

For any subset $s$ of an $R$-module $M$ and any element $x \in M$, $x$ belongs to the $R$-linear span of $s$ if and only if there exists a finitely supported function $l : s \to_{\text{f}} R$ such that the linear combination $\sum_{y \in s} l(y) \cdot y$ equals $x$.

Finsupp.mem_span_range_iff_exists_finsupp theorem

{v : α → M} {x : M} : x ∈ span R (range v) ↔ ∃ c : α →₀ R, (c.sum fun i a => a • v i) = x

Full source

theorem mem_span_range_iff_exists_finsupp {v : α → M} {x : M} :
    x ∈ span R (range v)x ∈ span R (range v) ↔ ∃ c : α →₀ R, (c.sum fun i a => a • v i) = x := by
  simp only [← Finsupp.range_linearCombination, LinearMap.mem_range, linearCombination_apply]

Characterization of Span Membership via Finite Linear Combinations

Informal description

For any family of vectors $v : \alpha \to M$ in an $R$-module $M$ and any vector $x \in M$, the vector $x$ lies in the span of the range of $v$ if and only if there exists a finitely supported function $c : \alpha \to_{\text{f}} R$ such that the linear combination $\sum_{i \in \alpha} c(i) \cdot v_i$ equals $x$.

Finsupp.span_image_eq_map_linearCombination theorem

(s : Set α) : span R (v '' s) = Submodule.map (linearCombination R v) (supported R R s)

Full source

theorem span_image_eq_map_linearCombination (s : Set α) :
    span R (v '' s) = Submodule.map (linearCombination R v) (supported R R s) := by
  apply span_eq_of_le
  · intro x hx
    rw [Set.mem_image] at hx
    apply Exists.elim hx
    intro i hi
    exact ⟨_, Finsupp.single_mem_supported R 1 hi.1, by simp [hi.2]⟩
  · refine map_le_iff_le_comap.2 fun z hz => ?_
    have : ∀ i, z i • v i ∈ span R (v '' s) := by
      intro c
      haveI := Classical.decPred fun x => x ∈ s
      by_cases h : c ∈ s
      · exact smul_mem _ _ (subset_span (Set.mem_image_of_mem _ h))
      · simp [(Finsupp.mem_supported' R _).1 hz _ h]
    rw [mem_comap, linearCombination_apply]
    refine sum_mem ?_
    simp [this]

Span of Image Equals Image of Linear Combination on Supported Functions

Informal description

For any subset $s$ of a type $\alpha$ and a family of vectors $v : \alpha \to M$ in an $R$-module $M$, the span of the image $v(s)$ is equal to the image of the submodule of finitely supported functions supported on $s$ under the linear combination map $\text{linearCombination}_R v$. That is, \[ \operatorname{span}_R (v(s)) = (\text{linearCombination}_R v)(\text{supported}_R R s). \]

Finsupp.mem_span_image_iff_linearCombination theorem

{s : Set α} {x : M} : x ∈ span R (v '' s) ↔ ∃ l ∈ supported R R s, linearCombination R v l = x

Full source

theorem mem_span_image_iff_linearCombination {s : Set α} {x : M} :
    x ∈ span R (v '' s)x ∈ span R (v '' s) ↔ ∃ l ∈ supported R R s, linearCombination R v l = x := by
  rw [span_image_eq_map_linearCombination]
  simp

Characterization of Span Membership via Linear Combinations with Restricted Support

Informal description

For any subset $s$ of a type $\alpha$, a family of vectors $v : \alpha \to M$ in an $R$-module $M$, and a vector $x \in M$, the vector $x$ belongs to the span of the image $v(s)$ if and only if there exists a finitely supported function $l : \alpha \to_{\text{f}} R$ with support contained in $s$ such that the linear combination $\sum_{i \in \alpha} l(i) \cdot v_i$ equals $x$.

Finsupp.linearCombination_option theorem

 (v : Option α → M) (f : Option α →₀ R) :
  linearCombination R v f = f none • v none + linearCombination R (v ∘ Option.some) f.some

Full source

theorem linearCombination_option (v : Option α → M) (f : OptionOption α →₀ R) :
    linearCombination R v f =
      f none • v none + linearCombination R (v ∘ Option.some) f.some := by
  rw [linearCombination_apply, sum_option_index_smul, linearCombination_apply]; simp

Decomposition of Linear Combination over Option Type

Informal description

Let $R$ be a semiring, $M$ an $R$-module, $\alpha$ a type, and $v : \text{Option}\ \alpha \to M$ a family of elements in $M$. For any finitely supported function $f : \text{Option}\ \alpha \to_{\text{f}} R$, the linear combination of the $v_i$ with coefficients $f(i)$ can be decomposed as: \[ \text{linearCombination}_R v f = f(\text{none}) \cdot v(\text{none}) + \text{linearCombination}_R (v \circ \text{some}) f|_\alpha, \] where $f|_\alpha$ denotes the restriction of $f$ to $\alpha$ via the $\text{some}$ constructor.

Finsupp.linearCombination_linearCombination theorem

 {α β : Type*} (A : α → M) (B : β → α →₀ R) (f : β →₀ R) :
  linearCombination R A (linearCombination R B f) = linearCombination R (fun b => linearCombination R A (B b)) f

Full source

theorem linearCombination_linearCombination {α β : Type*} (A : α → M) (B : β → α →₀ R)
    (f : β →₀ R) : linearCombination R A (linearCombination R B f) =
      linearCombination R (fun b => linearCombination R A (B b)) f := by
  classical
  simp only [linearCombination_apply]
  induction f using induction_linear with
  | zero => simp only [sum_zero_index]
  | add f₁ f₂ h₁ h₂ => simp [sum_add_index, h₁, h₂, add_smul]
  | single => simp [sum_single_index, sum_smul_index, smul_sum, mul_smul]

Composition of Linear Combinations in Module Theory

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $\alpha, \beta$ types. Given a family of elements $(A_i)_{i \in \alpha}$ in $M$, a family of finitely supported functions $(B_b)_{b \in \beta}$ where each $B_b \colon \alpha \to_{\text{f}} R$, and a finitely supported function $f \colon \beta \to_{\text{f}} R$, we have: \[ \text{linearCombination}_R A \left(\text{linearCombination}_R B f\right) = \text{linearCombination}_R \left(\lambda b, \text{linearCombination}_R A (B_b)\right) f \] In other words, the linear combination of the linear combinations is equal to the linear combination of the pointwise linear combinations.

Finsupp.linearCombination_smul theorem

 [Module R S] [Module S M] [IsScalarTower R S M] {w : α' → S} :
  linearCombination R (fun i : α × α' ↦ w i.2 • v i.1) =
    (linearCombination S v).restrictScalars R ∘ₗ
      mapRange.linearMap (linearCombination R w) ∘ₗ (finsuppProdLEquiv R).toLinearMap

Full source

theorem linearCombination_smul [Module R S] [Module S M] [IsScalarTower R S M] {w : α' → S} :
    linearCombination R (fun i : α × α' ↦ w i.2 • v i.1) = (linearCombination S v).restrictScalars R
      ∘ₗ mapRange.linearMap (linearCombination R w) ∘ₗ (finsuppProdLEquiv R).toLinearMap := by
  ext; simp [finsuppProdLEquiv, finsuppProdEquiv, Finsupp.curry]

Decomposition of Bilinear Combination via Scalar Restriction and Tensor Product

Informal description

Let $R$ and $S$ be semirings, and let $M$ be a module over $S$ that is also a module over $R$ with compatible scalar multiplication (i.e., $[IsScalarTower R S M]$). Given families of vectors $v : \alpha \to M$ and scalars $w : \alpha' \to S$, the linear combination $\sum_{(i,j) \in \alpha \times \alpha'} w(j) \cdot v(i)$ can be expressed as the composition of three linear maps: 1. The linear equivalence $(finsuppProdLEquiv R)$ between $(\alpha \times \alpha') \to_{\text{f}} R$ and $\alpha \to_{\text{f}} (\alpha' \to_{\text{f}} R)$, 2. The linear map induced by applying $linearCombination R w$ pointwise to each $\alpha' \to_{\text{f}} R$, 3. The restriction of scalars of $linearCombination S v$ from $S$ to $R$. In other words, the following equality holds: \[ linearCombination_R \left(\lambda (i,j), w(j) \cdot v(i)\right) = (linearCombination_S v)_R \circ mapRange(linearCombination_R w) \circ finsuppProdLEquiv_R \] where $(-)_R$ denotes restriction of scalars from $S$ to $R$.

Finsupp.linearCombination_fin_zero theorem

(f : Fin 0 → M) : linearCombination R f = 0

Full source

@[simp]
theorem linearCombination_fin_zero (f : Fin 0 → M) : linearCombination R f = 0 := by
  ext i
  apply finZeroElim i

Linear Combination over Empty Finite Type is Zero

Informal description

For any module $M$ over a semiring $R$ and any function $f : \text{Fin } 0 \to M$, the linear combination of the elements in the image of $f$ is equal to the zero element of $M$, i.e., $\sum_{i \in \text{Fin } 0} f(i) = 0$.

Finsupp.linearCombinationOn definition

(s : Set α) : supported R R s →ₗ[R] span R (v '' s)

Full source

/-- `Finsupp.linearCombinationOn M v s` interprets `p : α →₀ R` as a linear combination of a
subset of the vectors in `v`, mapping it to the span of those vectors.

The subset is indicated by a set `s : Set α` of indices.
-/
def linearCombinationOn (s : Set α) : supportedsupported R R s →ₗ[R] span R (v '' s) :=
  LinearMap.codRestrict _ ((linearCombination _ v).comp (Submodule.subtype (supported R R s)))
    fun ⟨l, hl⟩ => (mem_span_image_iff_linearCombination _).2 ⟨l, hl, rfl⟩

Linear combination restricted to a subset of indices

Informal description

Given a semiring $R$, an $R$-module $M$, a family of vectors $v : \alpha \to M$, and a subset $s \subseteq \alpha$, the function `Finsupp.linearCombinationOn` maps any finitely supported function $l : \alpha \to_{\text{f}} R$ with support contained in $s$ to the linear combination $\sum_{i \in s} l(i) \cdot v(i)$, which lies in the $R$-submodule spanned by the vectors $\{v(i) \mid i \in s\}$.

Finsupp.linearCombinationOn_range theorem

(s : Set α) : LinearMap.range (linearCombinationOn α M R v s) = ⊤

Full source

theorem linearCombinationOn_range (s : Set α) :
    LinearMap.range (linearCombinationOn α M R v s) = ⊤ := by
  rw [linearCombinationOn, LinearMap.range_eq_map, LinearMap.map_codRestrict,
    ← LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top, LinearMap.range_comp,
    range_subtype]
  exact (span_image_eq_map_linearCombination _ _).le

Surjectivity of Restricted Linear Combination Map onto Span of Image

Informal description

For any subset $s$ of a type $\alpha$ and a family of vectors $v : \alpha \to M$ in an $R$-module $M$, the range of the restricted linear combination map $\text{linearCombinationOn}_{\alpha,M,R,v,s}$ is the entire submodule $\text{span}_R (v(s))$. That is, the map is surjective onto its codomain.

Finsupp.linearCombination_restrict theorem

 (s : Set α) :
  linearCombination R (s.restrict v) =
    Submodule.subtype _ ∘ₗ linearCombinationOn α M R v s ∘ₗ (supportedEquivFinsupp s).symm.toLinearMap

Full source

theorem linearCombination_restrict (s : Set α) :
    linearCombination R (s.restrict v) = Submodule.subtypeSubmodule.subtype _ ∘ₗ
      linearCombinationOn α M R v s ∘ₗ (supportedEquivFinsupp s).symm.toLinearMap := by
  classical ext; simp [linearCombinationOn]

Restriction of Linear Combination Equals Composition of Restricted Linear Combination with Support Equivalence

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $v \colon \alpha \to M$ a family of elements in $M$. For any subset $s \subseteq \alpha$, the linear combination map for the restricted family $v|_s$ is equal to the composition of the following three linear maps: 1. The inverse of the equivalence between finitely supported functions on $s$ and finitely supported functions on $\alpha$ with support contained in $s$, 2. The restricted linear combination map for $v$ on $s$ (which lands in the span of $v(s)$), 3. The inclusion map of the span of $v(s)$ into $M$. In symbols: \[ \text{linearCombination}_R (v|_s) = \iota \circ \text{linearCombinationOn}_{\alpha,M,R,v,s} \circ \phi^{-1} \] where $\phi$ is the supported equivalence and $\iota$ is the submodule inclusion.

Finsupp.linearCombination_comp theorem

(f : α' → α) : linearCombination R (v ∘ f) = (linearCombination R v).comp (lmapDomain R R f)

Full source

theorem linearCombination_comp (f : α' → α) :
    linearCombination R (v ∘ f) = (linearCombination R v).comp (lmapDomain R R f) := by
  ext
  simp [linearCombination_apply]

Composition of Linear Combination with Domain Mapping

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $v \colon \alpha \to M$ a family of elements in $M$. For any function $f \colon \alpha' \to \alpha$, the linear combination map for the composed family $v \circ f$ is equal to the composition of the linear combination map for $v$ with the linear map induced by $f$ on finitely supported functions. That is, \[ \text{linearCombination}_R (v \circ f) = (\text{linearCombination}_R v) \circ (\text{lmapDomain}_R R f). \]

Finsupp.linearCombination_comapDomain theorem

 (f : α → α') (l : α' →₀ R) (hf : Set.InjOn f (f ⁻¹' ↑l.support)) :
  linearCombination R v (Finsupp.comapDomain f l hf) = (l.support.preimage f hf).sum fun i => l (f i) • v i

Full source

theorem linearCombination_comapDomain (f : α → α') (l : α' →₀ R)
    (hf : Set.InjOn f (f ⁻¹' ↑l.support)) : linearCombination R v (Finsupp.comapDomain f l hf) =
      (l.support.preimage f hf).sum fun i => l (f i) • v i := by
  rw [linearCombination_apply]; rfl

Linear Combination of Preimage Composition Equals Finite Sum over Preimage Support

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $v \colon \alpha \to M$ a family of elements in $M$. Given a function $f \colon \alpha \to \alpha'$, a finitely supported function $l \colon \alpha' \to_{\text{f}} R$, and a proof that $f$ is injective on the preimage of the support of $l$, the linear combination of $v$ with coefficients given by the preimage composition $\text{comapDomain}_f l hf$ equals the finite sum $\sum_{i \in f^{-1}(\text{supp } l)} l(f(i)) \cdot v(i)$.

Finsupp.linearCombination_onFinset theorem

 {s : Finset α} {f : α → R} (g : α → M) (hf : ∀ a, f a ≠ 0 → a ∈ s) :
  linearCombination R g (Finsupp.onFinset s f hf) = Finset.sum s fun x : α => f x • g x

Full source

theorem linearCombination_onFinset {s : Finset α} {f : α → R} (g : α → M)
    (hf : ∀ a, f a ≠ 0 → a ∈ s) :
    linearCombination R g (Finsupp.onFinset s f hf) = Finset.sum s fun x : α => f x • g x := by
  classical
  simp only [linearCombination_apply, Finsupp.sum, Finsupp.onFinset_apply, Finsupp.support_onFinset]
  rw [Finset.sum_filter_of_ne]
  intro x _ h
  contrapose! h
  simp [h]

Linear Combination over Finite Support Equals Finite Sum

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $\alpha$ a type. Given a finite subset $s \subseteq \alpha$, a function $f \colon \alpha \to R$ such that $f(a) \neq 0$ implies $a \in s$, and a function $g \colon \alpha \to M$, the linear combination of $g$ with coefficients given by the finitely supported function $\text{onFinset } s f hf$ is equal to the finite sum $\sum_{x \in s} f(x) \cdot g(x)$.

Finsupp.bilinearCombination definition

: (α → M) →ₗ[S] (α →₀ R) →ₗ[R] M

Full source

/-- `Finsupp.bilinearCombination R S v f` is the linear combination of vectors in `v` with weights
in `f`, as a bilinear map of `v` and `f`.
In the absence of `SMulCommClass R S M`, use `Finsupp.linearCombination`.

See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.
-/
def bilinearCombination : (α → M) →ₗ[S] (α →₀ R) →ₗ[R] M where
  toFun v := linearCombination R v
  map_add' u v := by ext; simp [Finset.sum_add_distrib, Pi.add_apply, smul_add]
  map_smul' r v := by ext; simp [Finset.smul_sum, smul_comm]

Bilinear combination of a family of module elements

Informal description

Given a semiring $R$, a semiring $S$, and an $R$-module $M$ that is also an $S$-module with compatible scalar multiplication (i.e., $SMulCommClass R S M$ holds), the bilinear combination function maps a family of vectors $(v_i)_{i \in \alpha}$ in $M$ to a bilinear map. This bilinear map takes a finitely supported function $l : \alpha \to_{\text{f}} R$ and returns the linear combination $\sum_{i \in \alpha} l(i) \cdot v_i$ in $M$. The construction is bilinear in both $v$ and $l$.

Finsupp.bilinearCombination_apply theorem

: bilinearCombination R S v = linearCombination R v

Full source

@[simp]
theorem bilinearCombination_apply :
    bilinearCombination R S v = linearCombination R v :=
  rfl

Bilinear Combination Equals Linear Combination for Compatible Modules

Informal description

Given a semiring $R$, a semiring $S$, and an $R$-module $M$ that is also an $S$-module with compatible scalar multiplication (i.e., $SMulCommClass R S M$ holds), the bilinear combination map $\text{bilinearCombination}_{R,S} v$ of a family of vectors $(v_i)_{i \in \alpha}$ in $M$ equals the linear combination map $\text{linearCombination}_R v$ for the same family.

Fintype.linearCombination definition

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

Full source

/-- `Fintype.linearCombination R v f` is the linear combination of vectors in `v` with weights
in `f`. This variant of `Finsupp.linearCombination` is defined on fintype indexed vectors.

This map is linear in `v` if `R` is commutative, and always linear in `f`.
See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.
-/
protected def Fintype.linearCombination : (α → R) →ₗ[R] M where
  toFun f := ∑ i, f i • v i
  map_add' f g := by simp_rw [← Finset.sum_add_distrib, ← add_smul]; rfl
  map_smul' r f := by simp_rw [Finset.smul_sum, smul_smul]; rfl

Linear combination over a finite type

Informal description

Given a finite type $\alpha$, a commutative semiring $R$, and a function $v : \alpha \to M$ where $M$ is an $R$-module, the function `Fintype.linearCombination R v` maps a function $f : \alpha \to R$ to the linear combination $\sum_{i} f(i) \cdot v(i)$. This map is linear in $f$ and, when $R$ is commutative, also linear in $v$.

Fintype.linearCombination_apply theorem

(f) : Fintype.linearCombination R v f = ∑ i, f i • v i

Full source

theorem Fintype.linearCombination_apply (f) : Fintype.linearCombination R v f = ∑ i, f i • v i :=
  rfl

Evaluation of Linear Combination over Finite Type

Informal description

Let $R$ be a commutative semiring, $\alpha$ a finite type, and $M$ an $R$-module. Given a function $v : \alpha \to M$, the linear combination map $\text{Fintype.linearCombination}_R v$ satisfies \[ \text{Fintype.linearCombination}_R v (f) = \sum_{i \in \alpha} f(i) \cdot v(i) \] for any function $f : \alpha \to R$, where $\cdot$ denotes the scalar multiplication in $M$.

Fintype.linearCombination_apply_single theorem

[DecidableEq α] (i : α) (r : R) : Fintype.linearCombination R v (Pi.single i r) = r • v i

Full source

@[simp]
theorem Fintype.linearCombination_apply_single [DecidableEq α] (i : α) (r : R) :
    Fintype.linearCombination R v (Pi.single i r) = r • v i := by
  simp_rw [Fintype.linearCombination_apply, Pi.single_apply, ite_smul, zero_smul]
  rw [Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]

Linear Combination of Single Function: $r \cdot v(i)$

Informal description

For a finite type $\alpha$ with decidable equality, a commutative semiring $R$, and an $R$-module $M$ with a function $v : \alpha \to M$, the linear combination of $v$ evaluated at the single function $\text{Pi.single } i r$ (which is $r$ at $i$ and $0$ elsewhere) is equal to the scalar multiple $r \cdot v(i)$. That is, \[ \text{Fintype.linearCombination } R v (\text{Pi.single } i r) = r \cdot v(i). \]

Finsupp.linearCombination_eq_fintype_linearCombination_apply theorem

 (x : α → R) : linearCombination R v ((Finsupp.linearEquivFunOnFinite R R α).symm x) = Fintype.linearCombination R v x

Full source

theorem Finsupp.linearCombination_eq_fintype_linearCombination_apply (x : α → R) :
    linearCombination R v ((Finsupp.linearEquivFunOnFinite R R α).symm x) =
      Fintype.linearCombination R v x := by
  apply Finset.sum_subset
  · exact Finset.subset_univ _
  · intro x _ hx
    rw [Finsupp.not_mem_support_iff.mp hx]
    exact zero_smul _ _

Equality of Linear Combinations via Finitely Supported Functions and Finite Type Functions

Informal description

Let $R$ be a commutative semiring, $\alpha$ a finite type, and $M$ an $R$-module. Given a function $v : \alpha \to M$, for any function $x : \alpha \to R$, the linear combination of $v$ with coefficients given by the finitely supported function corresponding to $x$ is equal to the linear combination of $v$ with coefficients $x$ over the finite type $\alpha$. That is, \[ \text{linearCombination}_R v \left( (\text{linearEquivFunOnFinite}_R R \alpha)^{-1} x \right) = \text{Fintype.linearCombination}_R v (x). \]

Finsupp.linearCombination_eq_fintype_linearCombination theorem

: (linearCombination R v).comp (Finsupp.linearEquivFunOnFinite R R α).symm.toLinearMap = Fintype.linearCombination R v

Full source

theorem Finsupp.linearCombination_eq_fintype_linearCombination :
    (linearCombination R v).comp (Finsupp.linearEquivFunOnFinite R R α).symm.toLinearMap =
      Fintype.linearCombination R v :=
  LinearMap.ext <| linearCombination_eq_fintype_linearCombination_apply R v

Equality of Linear Combination Maps via Finitely Supported Functions and Finite Type Functions

Informal description

Let $R$ be a commutative semiring, $\alpha$ a finite type, and $M$ an $R$-module. Given a function $v : \alpha \to M$, the composition of the linear combination map $\text{linearCombination}_R v$ with the inverse of the linear equivalence between finitely supported functions and functions on $\alpha$ is equal to the linear combination map $\text{Fintype.linearCombination}_R v$. That is, \[ \text{linearCombination}_R v \circ (\text{linearEquivFunOnFinite}_R R \alpha)^{-1} = \text{Fintype.linearCombination}_R v. \]

Fintype.range_linearCombination theorem

: LinearMap.range (Fintype.linearCombination R v) = Submodule.span R (Set.range v)

Full source

@[simp]
theorem Fintype.range_linearCombination :
    LinearMap.range (Fintype.linearCombination R v) = Submodule.span R (Set.range v) := by
  rw [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearMap.range_comp,
      LinearEquiv.range, Submodule.map_top, Finsupp.range_linearCombination]

Range of Linear Combination Equals Span of Vector Family for Finite Types

Informal description

For a finite type $\alpha$, a commutative semiring $R$, and an $R$-module $M$ with a function $v : \alpha \to M$, the range of the linear combination map $\text{Fintype.linearCombination}_R\, v$ is equal to the $R$-linear span of the range of $v$. That is: \[ \text{range}\, (\text{Fintype.linearCombination}_R\, v) = \text{span}_R\, \{v(i) \mid i \in \alpha\}. \]

Fintype.bilinearCombination definition

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

Full source

/-- `Fintype.bilinearCombination R S v f` is the linear combination of vectors in `v` with weights
in `f`. This variant of `Finsupp.linearCombination` is defined on fintype indexed vectors.

This map is linear in `v` if `R` is commutative, and always linear in `f`.
See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.
-/
protected def Fintype.bilinearCombination : (α → M) →ₗ[S] (α → R) →ₗ[R] M where
  toFun v := Fintype.linearCombination R v
  map_add' u v := by ext; simp [Fintype.linearCombination,
    Finset.sum_add_distrib, Pi.add_apply, smul_add]
  map_smul' r v := by ext; simp [Fintype.linearCombination, Finset.smul_sum, smul_comm]

Bilinear combination over a finite type

Informal description

Given a finite type $\alpha$, a commutative semiring $R$, a semiring $S$, and an $R$-module $M$ that is also an $S$-module with compatible scalar multiplication (`SMulCommClass R S M`), the function `Fintype.bilinearCombination R S` maps a vector-valued function $v : \alpha \to M$ to a bilinear map that takes a coefficient function $f : \alpha \to R$ and returns the linear combination $\sum_{i} f(i) \cdot v(i)$. This map is linear in $v$ when $S$ is commutative and always linear in $f$.

Fintype.bilinearCombination_apply theorem

: Fintype.bilinearCombination R S v = Fintype.linearCombination R v

Full source

@[simp]
theorem Fintype.bilinearCombination_apply :
    Fintype.bilinearCombination R S v = Fintype.linearCombination R v :=
  rfl

Bilinear Combination Equals Linear Combination for Finite Types

Informal description

For a finite type $\alpha$, a commutative semiring $R$, a semiring $S$, and an $R$-module $M$ that is also an $S$-module with compatible scalar multiplication (`SMulCommClass R S M`), the bilinear combination map `Fintype.bilinearCombination R S v` applied to a vector-valued function $v : \alpha \to M$ is equal to the linear combination map `Fintype.linearCombination R v`.

Fintype.bilinearCombination_apply_single theorem

[DecidableEq α] (i : α) (r : R) : Fintype.bilinearCombination R S v (Pi.single i r) = r • v i

Full source

theorem Fintype.bilinearCombination_apply_single [DecidableEq α] (i : α) (r : R) :
    Fintype.bilinearCombination R S v (Pi.single i r) = r • v i := by
  simp [Fintype.bilinearCombination]

Bilinear Combination of Single Function: $r \cdot v(i)$

Informal description

For a finite type $\alpha$ with decidable equality, a commutative semiring $R$, a semiring $S$, and an $R$-module $M$ that is also an $S$-module with compatible scalar multiplication, the bilinear combination of a vector-valued function $v : \alpha \to M$ evaluated at the single function $\text{Pi.single } i r$ (which is $r$ at $i$ and $0$ elsewhere) is equal to the scalar multiple $r \cdot v(i)$. That is, \[ \text{Fintype.bilinearCombination } R S v (\text{Pi.single } i r) = r \cdot v(i). \]

Submodule.mem_span_range_iff_exists_fun theorem

: x ∈ span R (range v) ↔ ∃ c : α → R, ∑ i, c i • v i = x

Full source

/-- An element `x` lies in the span of `v` iff it can be written as sum `∑ cᵢ • vᵢ = x`.
-/
theorem Submodule.mem_span_range_iff_exists_fun :
    x ∈ span R (range v)x ∈ span R (range v) ↔ ∃ c : α → R, ∑ i, c i • v i = x := by
  rw [Finsupp.equivFunOnFinite.surjective.exists]
  simp only [Finsupp.mem_span_range_iff_exists_finsupp, Finsupp.equivFunOnFinite_apply]
  exact exists_congr fun c => Eq.congr_left <| Finsupp.sum_fintype _ _ fun i => zero_smul _ _

Characterization of Span Membership via Linear Combinations

Informal description

An element $x$ of an $R$-module $M$ lies in the span of the range of a function $v : \alpha \to M$ if and only if there exists a function $c : \alpha \to R$ such that $x$ can be expressed as a finite linear combination $\sum_{i} c(i) \cdot v(i)$.

Submodule.top_le_span_range_iff_forall_exists_fun theorem

: ⊤ ≤ span R (range v) ↔ ∀ x, ∃ c : α → R, ∑ i, c i • v i = x

Full source

/-- A family `v : α → V` is generating `V` iff every element `(x : V)`
can be written as sum `∑ cᵢ • vᵢ = x`.
-/
theorem Submodule.top_le_span_range_iff_forall_exists_fun :
    ⊤⊤ ≤ span R (range v) ↔ ∀ x, ∃ c : α → R, ∑ i, c i • v i = x := by
  simp_rw [← mem_span_range_iff_exists_fun]
  exact ⟨fun h x => h trivial, fun h x _ => h x⟩

Span of Range Equals Top iff Every Element is a Linear Combination

Informal description

The span of the range of a function $v : \alpha \to M$ is the entire module $M$ if and only if for every element $x \in M$, there exists a function $c : \alpha \to R$ such that $x$ can be expressed as a finite linear combination $\sum_{i} c(i) \cdot v(i)$.

Submodule.mem_span_image_iff_exists_fun theorem

{s : Set α} : x ∈ span R (v '' s) ↔ ∃ t : Finset α, ↑t ⊆ s ∧ ∃ c : t → R, ∑ i, c i • v i = x

Full source

theorem Submodule.mem_span_image_iff_exists_fun {s : Set α} :
    x ∈ span R (v '' s)x ∈ span R (v '' s) ↔ ∃ t : Finset α, ↑t ⊆ s ∧ ∃ c : t → R, ∑ i, c i • v i = x := by
  refine ⟨fun h ↦ ?_, fun ⟨t, ht, c, hx⟩ ↦ ?_⟩
  · obtain ⟨l, hl, hx⟩ := (Finsupp.mem_span_image_iff_linearCombination R).mp h
    refine ⟨l.support, hl, l ∘ (↑), ?_⟩
    rw [← hx]
    exact l.support.sum_coe_sort fun a ↦ l a • v a
  · rw [← hx]
    exact sum_smul_mem (span R (v '' s)) c fun a _ ↦ subset_span <| by aesop

Characterization of Span Membership via Finite Linear Combinations with Restricted Support

Informal description

Let $R$ be a ring, $M$ an $R$-module, $v : \alpha \to M$ a function, and $s \subseteq \alpha$ a subset. An element $x \in M$ lies in the span of the image $v(s)$ if and only if there exists a finite subset $t \subseteq s$ and a function $c : t \to R$ such that $x$ can be expressed as the finite linear combination $\sum_{i \in t} c(i) \cdot v(i)$.

Fintype.mem_span_image_iff_exists_fun theorem

{s : Set α} [Fintype s] : x ∈ span R (v '' s) ↔ ∃ c : s → R, ∑ i, c i • v i = x

Full source

theorem Fintype.mem_span_image_iff_exists_fun {s : Set α} [Fintype s] :
    x ∈ span R (v '' s)x ∈ span R (v '' s) ↔ ∃ c : s → R, ∑ i, c i • v i = x := by
  rw [← mem_span_range_iff_exists_fun, image_eq_range]

Characterization of Span Membership via Finite Linear Combinations

Informal description

Let $R$ be a ring, $M$ an $R$-module, $v : \alpha \to M$ a function, and $s \subseteq \alpha$ a finite set. An element $x \in M$ lies in the span of the image $v(s)$ if and only if there exists a function $c : s \to R$ such that $x$ can be expressed as the finite linear combination $\sum_{i \in s} c(i) \cdot v(i)$.

Span.repr definition

Full source

/-- Pick some representation of `x : span R w` as a linear combination in `w`,
  ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose
-/
irreducible_def Span.repr (w : Set M) (x : span R w) : w →₀ R :=
  ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose

Representation of an element in the span as a linear combination

Informal description

Given a subset $w$ of an $R$-module $M$ and an element $x$ in the span of $w$, the function `Span.repr` selects a representation of $x$ as a finite linear combination of elements in $w$. Specifically, it returns a finitely supported function from $w$ to $R$ whose linear combination with the inclusion map $w \hookrightarrow M$ equals $x$.

Span.repr_def theorem

: eta_helper Eq✝ @Span.repr.{} @(delta% @definition✝)

Full source

/-- Pick some representation of `x : span R w` as a linear combination in `w`,
  ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose
-/
irreducible_def Span.repr (w : Set M) (x : span R w) : w →₀ R :=
  ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose

Linear combination representation of elements in a span

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $w$ a subset of $M$. For any element $x$ in the span of $w$, the linear combination of the coefficients given by `Span.repr` with the inclusion map $w \hookrightarrow M$ equals $x$. That is, if $\varphi$ is the representation of $x$ as a finitely supported function from $w$ to $R$, then $\sum_{v \in w} \varphi(v) \cdot v = x$.

Span.finsupp_linearCombination_repr theorem

{w : Set M} (x : span R w) : Finsupp.linearCombination R ((↑) : w → M) (Span.repr R w x) = x

Full source

@[simp]
theorem Span.finsupp_linearCombination_repr {w : Set M} (x : span R w) :
    Finsupp.linearCombination R ((↑) : w → M) (Span.repr R w x) = x := by
  rw [Span.repr_def]
  exact ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose_spec

Linear combination representation of elements in a span equals the element itself

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $w$ a subset of $M$. For any element $x$ in the $R$-linear span of $w$, the linear combination of the coefficients given by the representation $\mathrm{Span.repr}_R(w)(x)$ with respect to the inclusion map $w \hookrightarrow M$ equals $x$. That is, $$\sum_{v \in w} (\mathrm{Span.repr}_R(w)(x))(v) \cdot v = x.$$

LinearMap.map_finsupp_linearCombination theorem

 (f : M →ₗ[R] N) {ι : Type*} {g : ι → M} (l : ι →₀ R) : f (linearCombination R g l) = linearCombination R (f ∘ g) l

Full source

theorem LinearMap.map_finsupp_linearCombination (f : M →ₗ[R] N) {ι : Type*} {g : ι → M}
    (l : ι →₀ R) : f (linearCombination R g l) = linearCombination R (f ∘ g) l :=
  apply_linearCombination _ _ _ _

Linear Map Commutes with Linear Combination

Informal description

Let $R$ be a semiring, $M$ and $N$ be $R$-modules, and $g : \iota \to M$ be a family of elements in $M$. For any linear map $f : M \to N$ and any finitely supported function $l : \iota \to_{\text{f}} R$, we have $$ f\left(\sum_{i \in \iota} l(i) \cdot g(i)\right) = \sum_{i \in \iota} l(i) \cdot f(g(i)). $$

Submodule.mem_span_iff_exists_finset_subset theorem

 {s : Set M} {x : M} : x ∈ span R s ↔ ∃ (f : M → R) (t : Finset M), ↑t ⊆ s ∧ f.support ⊆ t ∧ ∑ a ∈ t, f a • a = x

Full source

lemma Submodule.mem_span_iff_exists_finset_subset {s : Set M} {x : M} :
    x ∈ span R sx ∈ span R s ↔
      ∃ (f : M → R) (t : Finset M), ↑t ⊆ s ∧ f.support ⊆ t ∧ ∑ a ∈ t, f a • a = x where
  mp := by
    rw [← s.image_id, mem_span_image_iff_linearCombination]
    rintro ⟨l, hl, rfl⟩
    exact ⟨l, l.support, by simpa [linearCombination, Finsupp.sum] using hl⟩
  mpr := by
    rintro ⟨n, t, hts, -, rfl⟩; exact sum_mem fun x hx ↦ smul_mem _ _ <| subset_span <| hts hx

Characterization of Span Membership via Finite Linear Combinations

Informal description

For any subset $s$ of an $R$-module $M$ and any element $x \in M$, $x$ belongs to the span of $s$ if and only if there exists a function $f : M \to R$ and a finite subset $t \subseteq s$ such that the support of $f$ is contained in $t$ and the linear combination $\sum_{a \in t} f(a) \cdot a$ equals $x$.

Submodule.mem_span_finset theorem

{s : Finset M} {x : M} : x ∈ span R s ↔ ∃ f : M → R, f.support ⊆ s ∧ ∑ a ∈ s, f a • a = x

Full source

lemma Submodule.mem_span_finset {s : Finset M} {x : M} :
    x ∈ span R sx ∈ span R s ↔ ∃ f : M → R, f.support ⊆ s ∧ ∑ a ∈ s, f a • a = x where
  mp := by
    rw [mem_span_iff_exists_finset_subset]
    rintro ⟨f, t, hts, hf, rfl⟩
    refine ⟨f, hf.trans hts, .symm <| Finset.sum_subset hts ?_⟩
    simp +contextual [Function.support_subset_iff'.1 hf]
  mpr := by rintro ⟨f, -, rfl⟩; exact sum_mem fun x hx ↦ smul_mem _ _ <| subset_span <| hx

Characterization of Span Membership via Finite Linear Combinations for Finite Sets

Informal description

Let $M$ be an $R$-module and $s$ a finite subset of $M$. An element $x \in M$ belongs to the span of $s$ if and only if there exists a function $f : M \to R$ with support contained in $s$ such that the linear combination $\sum_{a \in s} f(a) \cdot a$ equals $x$.

Submodule.mem_span_set theorem

 {m : M} {s : Set M} : m ∈ Submodule.span R s ↔ ∃ c : M →₀ R, (c.support : Set M) ⊆ s ∧ (c.sum fun mi r => r • mi) = m

Full source

/-- An element `m ∈ M` is contained in the `R`-submodule spanned by a set `s ⊆ M`, if and only if
`m` can be written as a finite `R`-linear combination of elements of `s`.
The implementation uses `Finsupp.sum`. -/
theorem Submodule.mem_span_set {m : M} {s : Set M} :
    m ∈ Submodule.span R sm ∈ Submodule.span R s ↔
      ∃ c : M →₀ R, (c.support : Set M) ⊆ s ∧ (c.sum fun mi r => r • mi) = m := by
  conv_lhs => rw [← Set.image_id s]
  exact Finsupp.mem_span_image_iff_linearCombination R (v := _root_.id (α := M))

Characterization of Span Membership via Finitely Supported Linear Combinations

Informal description

Let $M$ be an $R$-module and $s \subseteq M$ a subset. An element $m \in M$ is contained in the $R$-submodule spanned by $s$ if and only if there exists a finitely supported function $c : M \to_{\text{f}} R$ such that: 1. The support of $c$ is contained in $s$, and 2. The finite linear combination $\sum_{x \in M} c(x) \cdot x$ equals $m$. In other words: \[ m \in \text{span}_R(s) \iff \exists c \in M \to_{\text{f}} R, \text{supp}(c) \subseteq s \text{ and } \sum_{x \in \text{supp}(c)} c(x) \cdot x = m \]

Submodule.mem_span_set' theorem

 {m : M} {s : Set M} : m ∈ Submodule.span R s ↔ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → s), ∑ i, f i • (g i : M) = m

Full source

/-- An element `m ∈ M` is contained in the `R`-submodule spanned by a set `s ⊆ M`, if and only if
`m` can be written as a finite `R`-linear combination of elements of `s`.
The implementation uses a sum indexed by `Fin n` for some `n`. -/
lemma Submodule.mem_span_set' {m : M} {s : Set M} :
    m ∈ Submodule.span R sm ∈ Submodule.span R s ↔ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → s),
      ∑ i, f i • (g i : M) = m := by
  refine ⟨fun h ↦ ?_, ?_⟩
  · rcases mem_span_set.1 h with ⟨c, cs, rfl⟩
    have A : c.support ≃ Fin c.support.card := Finset.equivFin _
    refine ⟨_, fun i ↦ c (A.symm i), fun i ↦ ⟨A.symm i, cs (A.symm i).2⟩, ?_⟩
    rw [Finsupp.sum, ← Finset.sum_coe_sort c.support]
    exact Fintype.sum_equiv A.symm _ (fun j ↦ c j • (j : M)) (fun i ↦ rfl)
  · rintro ⟨n, f, g, rfl⟩
    exact Submodule.sum_mem _ (fun i _ ↦ Submodule.smul_mem _ _ (Submodule.subset_span (g i).2))

Characterization of Span Membership via Finite Linear Combinations

Informal description

Let $M$ be an $R$-module and $s \subseteq M$ a subset. An element $m \in M$ is contained in the $R$-submodule spanned by $s$ if and only if there exist a natural number $n$, coefficients $f_1, \ldots, f_n \in R$, and elements $g_1, \ldots, g_n \in s$ such that: \[ \sum_{i=1}^n f_i \cdot g_i = m \]

Submodule.span_eq_iUnion_nat theorem

 (s : Set M) :
  (Submodule.span R s : Set M) =
    ⋃ (n : ℕ), (fun (f : Fin n → (R × M)) ↦ ∑ i, (f i).1 • (f i).2) '' ({f | ∀ i, (f i).2 ∈ s})

Full source

/-- The span of a subset `s` is the union over all `n` of the set of linear combinations of at most
`n` terms belonging to `s`. -/
lemma Submodule.span_eq_iUnion_nat (s : Set M) :
    (Submodule.span R s : Set M) = ⋃ (n : ℕ),
      (fun (f : Fin n → (R × M)) ↦ ∑ i, (f i).1 • (f i).2) '' ({f | ∀ i, (f i).2 ∈ s}) := by
  ext m
  simp only [SetLike.mem_coe, mem_iUnion, mem_image, mem_setOf_eq, mem_span_set']
  refine exists_congr (fun n ↦ ⟨?_, ?_⟩)
  · rintro ⟨f, g, rfl⟩
    exact ⟨fun i ↦ (f i, g i), fun i ↦ (g i).2, rfl⟩
  · rintro ⟨f, hf, rfl⟩
    exact ⟨fun i ↦ (f i).1, fun i ↦ ⟨(f i).2, (hf i)⟩, rfl⟩

Span as Union of Finite Linear Combinations

Informal description

For any subset $s$ of an $R$-module $M$, the span of $s$ is equal to the union over all natural numbers $n$ of the set of all linear combinations $\sum_{i=1}^n r_i \cdot m_i$ where each $m_i \in s$ and $r_i \in R$. In other words: \[ \text{span}_R(s) = \bigcup_{n \in \mathbb{N}} \left\{ \sum_{i=1}^n r_i m_i \;\Big|\; \forall i, (r_i, m_i) \in R \times s \right\} \]

Finsupp.addSingleEquiv definition

: (ι →₀ R) ≃ₗ[R] (ι →₀ R)

Full source

/-- Given `c : ι → R` and an index `i` such that `c i = 0`, this is the linear isomorphism sending
the `j`-th standard basis vector to itself plus `c j` multiplied with the `i`-th standard basis
vector (in particular, the `i`-th standard basis vector is kept invariant). -/
def Finsupp.addSingleEquiv : (ι →₀ R) ≃ₗ[R] (ι →₀ R) := by
  refine .ofLinear (linearCombination _ fun j ↦ single j 1 + single i (c j))
    (linearCombination _ fun j ↦ single j 1 - single i (c j)) ?_ ?_ <;>
  ext j k <;> obtain rfl | hk := eq_or_ne i k
  · simp [h₀]
  · simp [single_eq_of_ne hk]
  · simp [h₀]
  · simp [single_eq_of_ne hk]

Linear isomorphism of finitely supported functions via basis adjustment

Informal description

Given a family of elements $(v_i)_{i \in \iota}$ in an $R$-module $M$ and an index $i \in \iota$ such that $c_i = 0$, this defines a linear isomorphism between the space of finitely supported functions $\iota \to_{\text{f}} R$ and itself. The isomorphism maps the standard basis vector $e_j$ (which takes value 1 at $j$ and 0 elsewhere) to $e_j + c_j e_i$ for each $j \in \iota$, and in particular leaves $e_i$ invariant.

Finsupp.linearCombination_comp_addSingleEquiv theorem

(v : ι → M) : linearCombination R v ∘ₗ addSingleEquiv i c h₀ = linearCombination R (v + (c · • v i))

Full source

theorem Finsupp.linearCombination_comp_addSingleEquiv (v : ι → M) :
    linearCombinationlinearCombination R v ∘ₗ addSingleEquiv i c h₀ = linearCombination R (v + (c · • v i)) := by
  ext; simp [addSingleEquiv]

Composition of Linear Combination with Basis Adjustment Equals Linear Combination of Modified Family

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $\iota$ an index set. Given a family of elements $(v_i)_{i \in \iota}$ in $M$, an index $i \in \iota$, a scalar $c \in R$ with $c_i = 0$, and the linear combination map $\text{linearCombination}_R v : (\iota \to_{\text{f}} R) \to M$, the composition of this map with the linear isomorphism $\text{addSingleEquiv}_{i,c,h_0}$ equals the linear combination map for the modified family $(v + (c \cdot v_i))_{i \in \iota}$. In symbols: \[ \text{linearCombination}_R v \circ \text{addSingleEquiv}_{i,c,h_0} = \text{linearCombination}_R (v + (c \cdot v_i)) \]

Mathlib.LinearAlgebra.Finsupp.LinearCombination

Main definitions

Tags