Mathlib.LinearAlgebra.Finsupp.VectorSpace

Finsupp.linearIndependent_single theorem

 {φ : ι → Type*} (f : ∀ ι, φ ι → M) (hf : ∀ i, LinearIndependent R (f i)) :
  LinearIndependent R fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)

Full source

theorem linearIndependent_single {φ : ι → Type*} (f : ∀ ι, φ ι → M)
    (hf : ∀ i, LinearIndependent R (f i)) :
    LinearIndependent R fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2) := by
  classical
  have : linearCombination R (fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)) =
    (finsuppLequivDFinsupp R).symm.toLinearMap ∘ₗ
    DFinsupp.mapRange.linearMap (fun i ↦ linearCombination R (f i)) ∘ₗ
    (sigmaFinsuppLequivDFinsupp R).toLinearMap := by ext; simp
  rw [LinearIndependent, this]
  exact (finsuppLequivDFinsupp R).symm.injective.comp <|
    ((DFinsupp.mapRange_injective _ fun _ ↦ map_zero _).mpr hf).comp (Equiv.injective _)

Linear Independence of Single-Point Embeddings from Linearly Independent Families

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $\phi : \iota \to \text{Type}$ a family of types indexed by $\iota$. Given a family of functions $f_i : \phi(i) \to M$ such that for each $i \in \iota$, the vectors $\{f_i(x)\}_{x \in \phi(i)}$ are linearly independent over $R$, then the vectors $\{\text{single}_i(f_i(x))\}_{(i,x) \in \Sigma_i \phi(i)}$ are also linearly independent over $R$ in the space of finitely supported functions $\iota \to_{\text{f}} M$. Here, $\text{single}_i(m)$ denotes the finitely supported function that takes value $m$ at $i$ and zero elsewhere, and $\Sigma_i \phi(i)$ is the dependent pair type consisting of pairs $(i,x)$ where $i \in \iota$ and $x \in \phi(i)$.

Finsupp.linearIndependent_single_iff theorem

 {φ : ι → Type*} {f : ∀ ι, φ ι → M} :
  LinearIndependent R (fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)) ↔ ∀ i, LinearIndependent R (f i)

Full source

lemma linearIndependent_single_iff {φ : ι → Type*} {f : ∀ ι, φ ι → M} :
    LinearIndependentLinearIndependent R (fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)) ↔
      ∀ i, LinearIndependent R (f i) := by
  refine ⟨fun h i => ?_, linearIndependent_single _⟩
  replace h := h.comp _ (sigma_mk_injective  (i := i))
  exact .of_comp (Finsupp.lsingle i) h

Linear Independence of Single-Point Embeddings Characterized by Componentwise Linear Independence

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $\phi : \iota \to \text{Type}$ a family of types indexed by $\iota$. Given a family of functions $f_i : \phi(i) \to M$, the family of vectors $\{\text{single}_i(f_i(x))\}_{(i,x) \in \Sigma_i \phi(i)}$ is linearly independent over $R$ in the space of finitely supported functions $\iota \to_{\text{f}} M$ if and only if for each $i \in \iota$, the family $\{f_i(x)\}_{x \in \phi(i)}$ is linearly independent over $R$. Here, $\text{single}_i(m)$ denotes the finitely supported function that takes value $m$ at $i$ and zero elsewhere, and $\Sigma_i \phi(i)$ is the dependent pair type consisting of pairs $(i,x)$ where $i \in \iota$ and $x \in \phi(i)$.

Finsupp.basis definition

{φ : ι → Type*} (b : ∀ i, Basis (φ i) R M) : Basis (Σ i, φ i) R (ι →₀ M)

Full source

/-- The basis on `ι →₀ M` with basis vectors `fun ⟨i, x⟩ ↦ single i (b i x)`. -/
protected def basis {φ : ι → Type*} (b : ∀ i, Basis (φ i) R M) : Basis (Σi, φ i) R (ι →₀ M) :=
  Basis.ofRepr
    { toFun := fun g =>
        { toFun := fun ix => (b ix.1).repr (g ix.1) ix.2
          support := g.support.sigma fun i => ((b i).repr (g i)).support
          mem_support_toFun := fun ix => by
            simp only [Finset.mem_sigma, mem_support_iff, and_iff_right_iff_imp, Ne]
            intro b hg
            simp [hg] at b }
      invFun := fun g =>
        { toFun := fun i => (b i).repr.symm (g.comapDomain _ sigma_mk_injective.injOn)
          support := g.support.image Sigma.fst
          mem_support_toFun := fun i => by
            rw [Ne, ← (b i).repr.injective.eq_iff, (b i).repr.apply_symm_apply,
                DFunLike.ext_iff]
            simp only [exists_prop, LinearEquiv.map_zero, comapDomain_apply, zero_apply,
              exists_and_right, mem_support_iff, exists_eq_right, Sigma.exists, Finset.mem_image,
              not_forall] }
      left_inv := fun g => by
        ext i
        rw [← (b i).repr.injective.eq_iff]
        ext x
        simp only [coe_mk, LinearEquiv.apply_symm_apply, comapDomain_apply]
      right_inv := fun g => by
        ext ⟨i, x⟩
        simp only [coe_mk, LinearEquiv.apply_symm_apply, comapDomain_apply]
      map_add' := fun g h => by
        ext ⟨i, x⟩
        simp only [coe_mk, add_apply, LinearEquiv.map_add]
      map_smul' := fun c h => by
        ext ⟨i, x⟩
        simp only [coe_mk, smul_apply, LinearEquiv.map_smul, RingHom.id_apply] }

Basis of finitely supported functions from a family of bases

Informal description

Given an indexed family of bases $b_i$ for an $R$-module $M$ over index sets $\phi(i)$, the structure `Finsupp.basis b` defines a basis for the space of finitely supported functions $\iota \to_{\text{f}} M$. The basis vectors are given by $\text{single}_i (b_i x)$ for each pair $(i, x) \in \Sigma_i \phi(i)$, where $\text{single}_i$ is the function that is $b_i x$ at $i$ and zero elsewhere. This basis establishes a linear equivalence between $\iota \to_{\text{f}} M$ and the space of finitely supported functions from $\Sigma_i \phi(i)$ to $R$, where the coordinates of a function $g \in \iota \to_{\text{f}} M$ are obtained by applying the representation isomorphism of each $b_i$ to $g(i)$.

Finsupp.basis_repr theorem

 {φ : ι → Type*} (b : ∀ i, Basis (φ i) R M) (g : ι →₀ M) (ix) :
  (Finsupp.basis b).repr g ix = (b ix.1).repr (g ix.1) ix.2

Full source

@[simp]
theorem basis_repr {φ : ι → Type*} (b : ∀ i, Basis (φ i) R M) (g : ι →₀ M) (ix) :
    (Finsupp.basis b).repr g ix = (b ix.1).repr (g ix.1) ix.2 :=
  rfl

Coordinate Representation of Finitely Supported Functions with Respect to a Family of Bases

Informal description

Let $\iota$ be an index type, $R$ a ring, and $M$ an $R$-module. Given a family of bases $\{b_i\}_{i \in \iota}$ where each $b_i$ is a basis for $M$ indexed by $\phi(i)$, and a finitely supported function $g : \iota \to_{\text{f}} M$, the coordinate representation of $g$ with respect to the basis `Finsupp.basis b` at the index `ix = (i, x)` is equal to the coordinate representation of $g(i)$ with respect to the basis $b_i$ at $x$. In other words, for any $(i, x) \in \Sigma_i \phi(i)$, we have: $$(\text{Finsupp.basis } b).\text{repr } g (i, x) = (b_i).\text{repr } (g(i)) x.$$

Finsupp.coe_basis theorem

 {φ : ι → Type*} (b : ∀ i, Basis (φ i) R M) : ⇑(Finsupp.basis b) = fun ix : Σ i, φ i => single ix.1 (b ix.1 ix.2)

Full source

@[simp]
theorem coe_basis {φ : ι → Type*} (b : ∀ i, Basis (φ i) R M) :
    ⇑(Finsupp.basis b) = fun ix : Σi, φ i => single ix.1 (b ix.1 ix.2) :=
  funext fun ⟨i, x⟩ =>
    Basis.apply_eq_iff.mpr <| by
      classical
      ext ⟨j, y⟩
      by_cases h : i = j
      · cases h
        simp [Finsupp.single_apply_left sigma_mk_injective]
      · simp_all

Basis Vectors of Finitely Supported Functions as Single-Point Evaluations

Informal description

Given an indexed family of bases $\{b_i\}_{i \in \iota}$ for an $R$-module $M$, where each $b_i$ is indexed by a type $\phi(i)$, the basis vectors of the finitely supported functions $\iota \to_{\text{f}} M$ are given by the function that maps each pair $(i, x) \in \Sigma_i \phi(i)$ to the finitely supported function $\text{single}_i (b_i x)$, which takes the value $b_i x$ at $i$ and zero elsewhere. In other words, the basis map $\text{Finsupp.basis } b$ is equal to the function that sends $(i, x)$ to $\text{single}_i (b_i x)$.

Module.Free.finsupp instance

[Module.Free R M] : Module.Free R (ι →₀ M)

Full source

instance _root_.Module.Free.finsupp [Module.Free R M] : Module.Free R (ι →₀ M) :=
  .of_basis (Finsupp.basis fun _ => Module.Free.chooseBasis R M)

Finitely Supported Functions of a Free Module are Free

Informal description

For any semiring $R$ and any free $R$-module $M$, the space of finitely supported functions $\iota \to_{\text{f}} M$ is also a free $R$-module.

Finsupp.basisSingleOne definition

: Basis ι R (ι →₀ R)

Full source

/-- The basis on `ι →₀ R` with basis vectors `fun i ↦ single i 1`. -/
@[simps]
protected def basisSingleOne : Basis ι R (ι →₀ R) :=
  Basis.ofRepr (LinearEquiv.refl _ _)

Standard basis of finitely supported functions

Informal description

The basis of the module $\iota \to_{\text{f}} R$ (finitely supported functions from $\iota$ to $R$) where the basis vectors are the functions $\text{single}_i(1)$ for each $i \in \iota$, which take the value $1$ at $i$ and $0$ elsewhere. This basis provides a linear isomorphism between $\iota \to_{\text{f}} R$ and itself via the identity map.

Finsupp.coe_basisSingleOne theorem

: (Finsupp.basisSingleOne : ι → ι →₀ R) = fun i => Finsupp.single i 1

Full source

@[simp]
theorem coe_basisSingleOne : (Finsupp.basisSingleOne : ι → ι →₀ R) = fun i => Finsupp.single i 1 :=
  funext fun _ => Basis.apply_eq_iff.mpr rfl

Standard Basis Vectors of Finitely Supported Functions as Single Nonzero Functions

Informal description

The standard basis vectors of the module of finitely supported functions from $\iota$ to $R$ are given by the functions $\text{single}_i(1)$ for each $i \in \iota$, where $\text{single}_i(1)$ is the function that takes the value $1$ at $i$ and $0$ elsewhere. Formally, the basis vectors of the basis `Finsupp.basisSingleOne` are exactly these functions, i.e., $(\text{Finsupp.basisSingleOne} : \iota \to \iota \to_{\text{f}} R) = \lambda i, \text{single}_i(1)$.

Finsupp.linearIndependent_single_one theorem

: LinearIndependent R fun i : ι ↦ single i (1 : R)

Full source

lemma linearIndependent_single_one : LinearIndependent R fun i : ι ↦ single i (1 : R) :=
  Finsupp.basisSingleOne.linearIndependent

Linear independence of standard basis functions $\text{single}_i(1)$

Informal description

The family of finitely supported functions $\{\text{single}_i(1)\}_{i \in \iota}$, where each $\text{single}_i(1)$ is the function that takes the value $1$ at $i$ and $0$ elsewhere, is linearly independent over the ring $R$.

Finsupp.linearIndependent_single_of_ne_zero theorem

[NoZeroSMulDivisors R M] {v : ι → M} (hv : ∀ i, v i ≠ 0) : LinearIndependent R fun i : ι ↦ single i (v i)

Full source

lemma linearIndependent_single_of_ne_zero [NoZeroSMulDivisors R M] {v : ι → M} (hv : ∀ i, v i ≠ 0) :
    LinearIndependent R fun i : ι ↦ single i (v i) := by
  rw [← linearIndependent_equiv (Equiv.sigmaPUnit ι)]
  exact linearIndependent_single (f := fun i (_ : Unit) ↦ v i) <| by
    simp +contextual [Fintype.linearIndependent_iff, hv]

Linear Independence of Single-Point Embeddings of Nonzero Vectors

Informal description

Let $R$ be a semiring and $M$ an $R$-module with no zero smul divisors (i.e., $r \cdot m = 0$ implies $r = 0$ or $m = 0$). Given a family of vectors $v : \iota \to M$ such that $v_i \neq 0$ for all $i \in \iota$, the family of finitely supported functions $\{\text{single}_i(v_i)\}_{i \in \iota}$ is linearly independent over $R$, where $\text{single}_i(v_i)$ denotes the function that takes value $v_i$ at $i$ and zero elsewhere.

DFinsupp.basis definition

{η : ι → Type*} (b : ∀ i, Basis (η i) R (M i)) : Basis (Σ i, η i) R (Π₀ i, M i)

Full source

/-- The direct sum of free modules is free.

Note that while this is stated for `DFinsupp` not `DirectSum`, the types are defeq. -/
noncomputable def basis {η : ι → Type*} (b : ∀ i, Basis (η i) R (M i)) :
    Basis (Σi, η i) R (Π₀ i, M i) :=
  .ofRepr
    ((mapRange.linearEquiv fun i => (b i).repr).trans (sigmaFinsuppLequivDFinsupp R).symm)

Basis for dependent finitely supported functions from individual bases

Informal description

Given a family of $R$-modules $\{M_i\}_{i \in \iota}$ and for each $i \in \iota$ a basis $b_i$ for $M_i$ indexed by $\eta_i$, the dependent finitely supported functions $\Pi₀ i, M_i$ form a free $R$-module with basis indexed by $\Sigma i, \eta_i$ (the disjoint union of the index types). More precisely, the basis is constructed through the linear equivalence between $\Pi₀ i, M_i$ and $\Sigma i, \eta_i \to₀ R$ (finitely supported functions on the disjoint union), obtained by: 1. Applying each basis representation $(b_i).repr : M_i \simeq (\eta_i \to₀ R)$ pointwise 2. Composing with the linear equivalence $\Sigma i, \eta_i \to₀ R \simeq \Pi₀ i, (\eta_i \to₀ R)$

Module.Free.dfinsupp instance

[∀ i : ι, Module.Free R (M i)] : Module.Free R (Π₀ i, M i)

Full source

instance _root_.Module.Free.dfinsupp [∀ i : ι, Module.Free R (M i)] : Module.Free R (Π₀ i, M i) :=
  .of_basis <| DFinsupp.basis fun i => Module.Free.chooseBasis R (M i)

Free Module Structure on Dependent Functions with Finite Support

Informal description

For any family of $R$-modules $\{M_i\}_{i \in \iota}$ where each $M_i$ is a free $R$-module, the dependent finitely supported functions $\Pi₀ i, M_i$ also form a free $R$-module.

Module.Free.trans theorem

 {R S M : Type*} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M]
  [IsScalarTower R S M] [Module.Free S M] [Module.Free R S] : Module.Free R M

Full source

lemma Module.Free.trans {R S M : Type*} [CommSemiring R] [Semiring S] [Algebra R S]
    [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [Module.Free S M]
    [Module.Free R S] : Module.Free R M :=
  let e : (ChooseBasisIndex S M →₀ S) ≃ₗ[R] ChooseBasisIndex S M →₀ (ChooseBasisIndex R S →₀ R) :=
    Finsupp.mapRange.linearEquiv (chooseBasis R S).repr
  let e : M ≃ₗ[R] ChooseBasisIndex S M →₀ (ChooseBasisIndex R S →₀ R) :=
    (chooseBasis S M).repr.restrictScalars R ≪≫ₗ e
  .of_equiv e.symm

Transitivity of Free Modules: $M$ free over $S$ and $S$ free over $R$ implies $M$ free over $R$

Informal description

Let $R$ be a commutative semiring, $S$ a semiring equipped with an $R$-algebra structure, and $M$ an additive commutative monoid with compatible $R$-module and $S$-module structures such that the scalar multiplication satisfies $r \cdot (s \cdot m) = (r \cdot s) \cdot m$ for all $r \in R$, $s \in S$, $m \in M$. If $M$ is a free $S$-module and $S$ is a free $R$-module, then $M$ is also a free $R$-module.

Finset.sum_single_ite theorem

[Fintype n] (a : R) (i : n) : (∑ x : n, Finsupp.single x (if i = x then a else 0)) = Finsupp.single i a

Full source

theorem _root_.Finset.sum_single_ite [Fintype n] (a : R) (i : n) :
    (∑ x : n, Finsupp.single x (if i = x then a else 0)) = Finsupp.single i a := by
  simp only [apply_ite (Finsupp.single _), Finsupp.single_zero, Finset.sum_ite_eq,
    if_pos (Finset.mem_univ _)]

Sum of Single-Point Functions Equals Single-Point Function

Informal description

Let $n$ be a finite type and $R$ be a commutative semiring. For any element $a \in R$ and any index $i \in n$, the sum over all $x \in n$ of the finitely supported function $\text{single}_x(a)$ (where $a$ is placed at $x$ if $x = i$ and $0$ otherwise) equals the finitely supported function $\text{single}_i(a)$.

Basis.equivFun_symm_single theorem

[Finite n] (b : Basis n R M) (i : n) : b.equivFun.symm (Pi.single i 1) = b i

Full source

@[simp]
theorem equivFun_symm_single [Finite n] (b : Basis n R M) (i : n) :
    b.equivFun.symm (Pi.single i 1) = b i := by
  cases nonempty_fintype n
  simp [Pi.single_apply]

Inverse Coordinate Representation of Basis Vector: $b.\text{equivFun}^{-1}(\text{single}_i(1)) = b(i)$

Informal description

Let $M$ be a module over a ring $R$ with a finite basis $b$ indexed by a finite type $n$. For any index $i \in n$, the inverse of the coordinate representation isomorphism $b.\text{equivFun}^{-1}$ applied to the function $\text{single}_i(1)$ (which is $1$ at $i$ and $0$ elsewhere) equals the basis vector $b(i)$. In other words, the linear combination $\sum_{j \in n} (\text{single}_i(1))(j) \cdot b(j)$ simplifies to $b(i)$.

Basis.repr_smul' theorem

(i : ι) (r : R) (s : S) : B.repr (algebraMap R S r * s) i = r * B.repr s i

Full source

/-- For any `r : R`, `s : S`, we have
  `B.repr ((algebra_map R S r) * s) i = r * (B.repr s i) `. -/
theorem Basis.repr_smul' (i : ι) (r : R) (s : S) :
    B.repr (algebraMap R S r * s) i = r * B.repr s i := by
  rw [← smul_eq_mul, ← smul_eq_mul, algebraMap_smul, map_smul, Finsupp.smul_apply]

Scalar Multiplication in Basis Representation: $B_{\text{repr}}(r \cdot s)_i = r \cdot B_{\text{repr}}(s)_i$

Informal description

Let $B$ be a basis for an $R$-module $M$ indexed by $\iota$, and let $S$ be an $R$-algebra. For any $r \in R$, $s \in S$, and $i \in \iota$, the $i$-th coordinate of the representation of $(\text{algebraMap}\, R\, S\, r) \cdot s$ in the basis $B$ is equal to $r$ multiplied by the $i$-th coordinate of the representation of $s$ in $B$, i.e., \[ B_{\text{repr}}((\text{algebraMap}\, R\, S\, r) \cdot s)_i = r \cdot B_{\text{repr}}(s)_i. \]