Mathlib.LinearAlgebra.StdBasis

Module docstring

{"# The standard basis

This file defines the standard basis Pi.basis (s : ∀ j, Basis (ι j) R (M j)), which is the Σ j, ι j-indexed basis of Π j, M j. The basis vectors are given by Pi.basis s ⟨j, i⟩ j' = Pi.single j' (s j) i = if j = j' then s i else 0.

The standard basis on R^η, i.e. η → R is called Pi.basisFun.

To give a concrete example, Pi.single (i : Fin 3) (1 : R) gives the ith unit basis vector in R³, and Pi.basisFun R (Fin 3) proves this is a basis over Fin 3 → R.

Main definitions

Pi.basis s: given a basis s i for each M i, the standard basis on Π i, M i
Pi.basisFun R η: the standard basis on R^η, i.e. η → R, given by Pi.basisFun R η i j = Pi.single i 1 j = if i = j then 1 else 0.
Matrix.stdBasis R n m: the standard basis on Matrix n m R, given by Matrix.stdBasis R n m (i, j) i' j' = if (i, j) = (i', j') then 1 else 0.

Pi.linearIndependent_single theorem

 [Ring R] [∀ i, AddCommGroup (Ms i)] [∀ i, Module R (Ms i)] [DecidableEq η] (v : ∀ j, ιs j → Ms j)
  (hs : ∀ i, LinearIndependent R (v i)) : LinearIndependent R fun ji : Σ j, ιs j ↦ Pi.single ji.1 (v ji.1 ji.2)

Full source

theorem linearIndependent_single [Ring R] [∀ i, AddCommGroup (Ms i)] [∀ i, Module R (Ms i)]
    [DecidableEq η] (v : ∀ j, ιs j → Ms j) (hs : ∀ i, LinearIndependent R (v i)) :
    LinearIndependent R fun ji : Σj, ιs j ↦ Pi.single ji.1 (v ji.1 ji.2) := by
  have hs' : ∀ j : η, LinearIndependent R fun i : ιs j => LinearMap.single R Ms j (v j i) := by
    intro j
    exact (hs j).map' _ (LinearMap.ker_single _ _ _)
  apply linearIndependent_iUnion_finite hs'
  intro j J _ hiJ
  have h₀ :
    ∀ j, span R (range fun i : ιs j => LinearMap.single R Ms j (v j i)) ≤
      LinearMap.range (LinearMap.single R Ms j) := by
    intro j
    rw [span_le, LinearMap.range_coe]
    apply range_comp_subset_range
  have h₁ :
    span R (range fun i : ιs j => LinearMap.single R Ms j (v j i)) ≤
      ⨆ i ∈ ({j} : Set _), LinearMap.range (LinearMap.single R Ms i) := by
    rw [@iSup_singleton _ _ _ fun i => LinearMap.range (LinearMap.single R (Ms) i)]
    apply h₀
  have h₂ :
    ⨆ j ∈ J, span R (range fun i : ιs j => LinearMap.single R Ms j (v j i)) ≤
      ⨆ j ∈ J, LinearMap.range (LinearMap.single R (fun j : η => Ms j) j) :=
    iSup₂_mono fun i _ => h₀ i
  have h₃ : Disjoint (fun i : η => i ∈ ({j} : Set _)) J := by
    convert Set.disjoint_singleton_left.2 hiJ using 0
  exact (disjoint_single_single _ _ _ _ h₃).mono h₁ h₂

Linear Independence of Standard Basis Vectors in Product Modules

Informal description

Let $R$ be a ring, and for each $i$, let $M_i$ be an $R$-module. Suppose for each $j$, we have a family of vectors $v_j : \iota_j \to M_j$ that is linearly independent over $R$. Then the family of vectors in the product module $\prod_j M_j$ given by $(j, i) \mapsto \text{Pi.single}_j (v_j i)$ (where $\text{Pi.single}_j$ is the function that is $v_j i$ at index $j$ and zero elsewhere) is also linearly independent over $R$.

Pi.linearIndependent_single_one theorem

(ι R : Type*) [Ring R] [DecidableEq ι] : LinearIndependent R (fun i : ι ↦ Pi.single i (1 : R))

Full source

theorem linearIndependent_single_one (ι R : Type*) [Ring R] [DecidableEq ι] :
    LinearIndependent R (fun i : ι ↦ Pi.single i (1 : R)) := by
  rw [← linearIndependent_equiv (Equiv.sigmaPUnit ι)]
  exact Pi.linearIndependent_single (fun (_ : ι) (_ : Unit) ↦ (1 : R))
    <| by simp +contextual [Fintype.linearIndependent_iff]

Linear Independence of Standard Basis Vectors in Function Space

Informal description

Let $R$ be a ring and $\iota$ be a type with decidable equality. The family of vectors $\{ \text{Pi.single}_i (1_R) \}_{i \in \iota}$ in the product module $\prod_{i \in \iota} R$ is linearly independent over $R$, where $\text{Pi.single}_i (1_R)$ is the function that is $1_R$ at index $i$ and zero elsewhere.

Pi.linearIndependent_single_of_ne_zero theorem

 {ι R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [DecidableEq ι] {v : ι → M}
  (hv : ∀ i, v i ≠ 0) : LinearIndependent R fun i : ι ↦ Pi.single i (v i)

Full source

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

Linear Independence of Nonzero Single Vectors in Product Module

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero smul divisors (i.e., $r \cdot m = 0$ implies $r = 0$ or $m = 0$). Let $\iota$ be a type with decidable equality, and let $v : \iota \to M$ be a family of vectors such that $v(i) \neq 0$ for all $i \in \iota$. Then the family of vectors $\{ \text{Pi.single}_i (v(i)) \}_{i \in \iota}$ in the product module $\prod_{i \in \iota} M$ is linearly independent over $R$, where $\text{Pi.single}_i (v(i))$ is the function that equals $v(i)$ at index $i$ and is zero elsewhere.

Pi.linearIndependent_single_ne_zero theorem

 {ι R : Type*} [Ring R] [NoZeroDivisors R] [DecidableEq ι] {v : ι → R} (hv : ∀ i, v i ≠ 0) :
  LinearIndependent R (fun i : ι ↦ Pi.single i (v i))

Full source

@[deprecated linearIndependent_single_of_ne_zero (since := "2025-04-14")]
theorem linearIndependent_single_ne_zero {ι R : Type*} [Ring R] [NoZeroDivisors R] [DecidableEq ι]
    {v : ι → R} (hv : ∀ i, v i ≠ 0) : LinearIndependent R (fun i : ι ↦ Pi.single i (v i)) :=
  linearIndependent_single_of_ne_zero hv

Linear Independence of Nonzero Single Functions in Product Ring

Informal description

Let $R$ be a ring with no zero divisors, $\iota$ a type with decidable equality, and $v : \iota \to R$ a family of elements in $R$ such that $v(i) \neq 0$ for all $i \in \iota$. Then the family of functions $\{ \text{single}_i (v(i)) \}_{i \in \iota}$ in the product module $\prod_{i \in \iota} R$ is linearly independent over $R$, where $\text{single}_i (v(i))$ is the function that equals $v(i)$ at index $i$ and is zero elsewhere.

Pi.basis definition

(s : ∀ j, Basis (ιs j) R (Ms j)) : Basis (Σ j, ιs j) R (∀ j, Ms j)

Full source

/-- `Pi.basis (s : ∀ j, Basis (ιs j) R (Ms j))` is the `Σ j, ιs j`-indexed basis on `Π j, Ms j`
given by `s j` on each component.

For the standard basis over `R` on the finite-dimensional space `η → R` see `Pi.basisFun`.
-/
protected noncomputable def basis (s : ∀ j, Basis (ιs j) R (Ms j)) :
    Basis (Σj, ιs j) R (∀ j, Ms j) :=
  Basis.ofRepr
    ((LinearEquiv.piCongrRight fun j => (s j).repr) ≪≫ₗ
      (Finsupp.sigmaFinsuppLEquivPiFinsupp R).symm)

Standard basis of a product of modules

Informal description

Given for each index $j$ a basis $s_j$ of the $R$-module $M_j$ indexed by $\iota_j$, the function `Pi.basis` constructs the standard basis of the product module $\prod_j M_j$. This basis is indexed by the disjoint union $\Sigma j, \iota_j$ (pairs $(j, i)$ where $i \in \iota_j$), and the basis vector corresponding to $(j, i)$ is the function that is $s_j i$ in the $j$-th coordinate and zero elsewhere.

Pi.basis_repr_single theorem

 [DecidableEq η] (s : ∀ j, Basis (ιs j) R (Ms j)) (j i) :
  (Pi.basis s).repr (Pi.single j (s j i)) = Finsupp.single ⟨j, i⟩ 1

Full source

@[simp]
theorem basis_repr_single [DecidableEq η] (s : ∀ j, Basis (ιs j) R (Ms j)) (j i) :
    (Pi.basis s).repr (Pi.single j (s j i)) = Finsupp.single ⟨j, i⟩ 1 := by
  classical
  ext ⟨j', i'⟩
  by_cases hj : j = j'
  · subst hj
    simp only [Pi.basis, LinearEquiv.trans_apply, Basis.repr_self, Pi.single_eq_same,
      LinearEquiv.piCongrRight, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
      Basis.repr_symm_apply, LinearEquiv.coe_mk, ne_eq, Sigma.mk.inj_iff, heq_eq_eq, true_and]
    symm
    simp [Finsupp.single_apply]
  simp only [Pi.basis, LinearEquiv.trans_apply, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
    LinearEquiv.piCongrRight, coe_single]
  dsimp
  rw [Pi.single_eq_of_ne (Ne.symm hj), LinearEquiv.map_zero, Finsupp.zero_apply,
    Finsupp.single_eq_of_ne]
  rintro ⟨⟩
  contradiction

Representation of Standard Basis Vectors in Product Module

Informal description

Let $R$ be a ring, $\eta$ an index set, and for each $j \in \eta$, let $M_j$ be an $R$-module with basis $s_j$ indexed by $\iota_j$. For any $j \in \eta$ and $i \in \iota_j$, the representation of the basis vector $\text{Pi.single}_j (s_j i)$ (which is $s_j i$ in the $j$-th coordinate and zero elsewhere) with respect to the standard basis $\text{Pi.basis } s$ is given by the indicator function $\delta_{(j,i)}$ (which is 1 at $(j,i)$ and zero elsewhere). More precisely, we have: $$(\text{Pi.basis } s).\text{repr}(\text{Pi.single}_j (s_j i)) = \delta_{(j,i)}$$ where $\delta_{(j,i)}$ denotes the function that is 1 at $(j,i)$ and zero elsewhere in the disjoint union $\Sigma j, \iota_j$.

Pi.basis_apply theorem

[DecidableEq η] (s : ∀ j, Basis (ιs j) R (Ms j)) (ji) : Pi.basis s ji = Pi.single ji.1 (s ji.1 ji.2)

Full source

@[simp]
theorem basis_apply [DecidableEq η] (s : ∀ j, Basis (ιs j) R (Ms j)) (ji) :
    Pi.basis s ji = Pi.single ji.1 (s ji.1 ji.2) :=
  Basis.apply_eq_iff.mpr (by simp)

Explicit Form of Standard Basis Vectors in Product Module

Informal description

Let $R$ be a ring, $\eta$ an index set, and for each $j \in \eta$, let $M_j$ be an $R$-module with basis $s_j$ indexed by $\iota_j$. For any pair $(j, i) \in \Sigma j, \iota_j$, the basis vector $\text{Pi.basis } s (j, i)$ in the product module $\prod_{j \in \eta} M_j$ is equal to the function that is $s_j i$ in the $j$-th coordinate and zero elsewhere. More precisely, we have: $$\text{Pi.basis } s (j, i) = \text{Pi.single}_j (s_j i)$$ where $\text{Pi.single}_j (s_j i)$ denotes the function that takes the value $s_j i$ at $j$ and zero at all other indices.

Pi.basis_repr theorem

(s : ∀ j, Basis (ιs j) R (Ms j)) (x) (ji) : (Pi.basis s).repr x ji = (s ji.1).repr (x ji.1) ji.2

Full source

@[simp]
theorem basis_repr (s : ∀ j, Basis (ιs j) R (Ms j)) (x) (ji) :
    (Pi.basis s).repr x ji = (s ji.1).repr (x ji.1) ji.2 :=
  rfl

Coefficient Extraction in Standard Basis of Product Module

Informal description

Let $R$ be a ring, $\eta$ an index set, and for each $j \in \eta$, let $M_j$ be an $R$-module with basis $s_j$ indexed by $\iota_j$. For any element $x$ in the product module $\prod_{j \in \eta} M_j$ and any pair $(j, i) \in \Sigma j, \iota_j$, the coefficient of the basis vector corresponding to $(j, i)$ in the expansion of $x$ with respect to the standard basis $\text{Pi.basis } s$ is equal to the coefficient of $x_j$ with respect to the basis $s_j$ at index $i$. More precisely, if $\text{Pi.basis } s$ is the standard basis constructed from the family of bases $s$, then for any $x \in \prod_j M_j$ and any $(j, i) \in \Sigma j, \iota_j$, we have: $$(\text{Pi.basis } s).\text{repr}(x)_{(j,i)} = (s_j).\text{repr}(x_j)_i$$ where $\text{repr}$ denotes the representation of an element in terms of the given basis.

Pi.basisFun definition

: Basis η R (η → R)

Full source

/-- The basis on `η → R` where the `i`th basis vector is `Function.update 0 i 1`. -/
noncomputable def basisFun : Basis η R (η → R) :=
  Basis.ofEquivFun (LinearEquiv.refl _ _)

Standard basis on function space $\eta \to R$

Informal description

The standard basis on the space of functions $\eta \to R$, where for each index $i \in \eta$, the basis vector is the function that takes the value $1$ at $i$ and $0$ elsewhere. More formally, the basis is given by the vectors $\{e_i\}_{i \in \eta}$, where $e_i(j) = \delta_{ij}$ (Kronecker delta). This means $e_i(j) = 1$ if $i = j$ and $0$ otherwise.

Pi.basisFun_apply theorem

[DecidableEq η] (i) : basisFun R η i = Pi.single i 1

Full source

@[simp]
theorem basisFun_apply [DecidableEq η] (i) :
    basisFun R η i = Pi.single i 1 := by
  simp only [basisFun, Basis.coe_ofEquivFun, LinearEquiv.refl_symm, LinearEquiv.refl_apply]

Standard Basis Vector as Indicator Function

Informal description

For any type $\eta$ with decidable equality and any ring $R$, the $i$-th vector of the standard basis on the function space $\eta \to R$ is given by the function $\text{Pi.single } i \ 1$, which takes the value $1$ at $i$ and $0$ elsewhere.

Pi.basisFun_repr theorem

(x : η → R) (i : η) : (Pi.basisFun R η).repr x i = x i

Full source

@[simp]
theorem basisFun_repr (x : η → R) (i : η) : (Pi.basisFun R η).repr x i = x i := by simp [basisFun]

Standard Basis Coordinates are Function Values

Informal description

For any function $x \colon \eta \to R$ and any index $i \in \eta$, the $i$-th coordinate of $x$ with respect to the standard basis $\{e_j\}_{j \in \eta}$ (where $e_j(k) = \delta_{jk}$) is equal to the value $x(i)$. In other words, the representation of $x$ in the standard basis satisfies $(\text{basisFun } R \eta)^{-1}(x)(i) = x(i)$ for all $i \in \eta$.

Pi.basisFun_equivFun theorem

: (Pi.basisFun R η).equivFun = LinearEquiv.refl _ _

Full source

@[simp]
theorem basisFun_equivFun : (Pi.basisFun R η).equivFun = LinearEquiv.refl _ _ :=
  Basis.equivFun_ofEquivFun _

Standard basis coordinate map is identity

Informal description

The equivalence function of the standard basis `Pi.basisFun R η` is equal to the identity linear equivalence on the function space $\eta \to R$. More precisely, for the standard basis $\{e_i\}_{i \in \eta}$ on $R^\eta$, the map that sends a vector to its coordinates in this basis is exactly the identity map when viewed as a linear equivalence.

Module.piEquiv definition

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

Full source

/-- The natural linear equivalence: `Mⁱ ≃ Hom(Rⁱ, M)` for an `R`-module `M`. -/
noncomputable def piEquiv : (ι → M) ≃ₗ[R] ((ι → R) →ₗ[R] M) := Basis.constr (Pi.basisFun R ι) R

Linear equivalence between function space and linear maps from the standard basis

Informal description

The natural linear equivalence between the space of functions $\iota \to M$ and the space of linear maps $(\iota \to R) \to M$ for an $R$-module $M$. More precisely, given a finite type $\iota$, a commutative semiring $R$, and an $R$-module $M$, the equivalence maps a function $v : \iota \to M$ to the linear map that sends $w : \iota \to R$ to $\sum_{i} w(i) \cdot v(i)$. This equivalence can be constructed using the standard basis on $\iota \to R$ (i.e., the basis vectors $e_i$ where $e_i(j) = \delta_{ij}$).

Module.piEquiv_apply_apply theorem

 (ι R M : Type*) [Fintype ι] [CommSemiring R] [AddCommMonoid M] [Module R M] (v : ι → M) (w : ι → R) :
  piEquiv ι R M v w = ∑ i, w i • v i

Full source

lemma piEquiv_apply_apply (ι R M : Type*) [Fintype ι] [CommSemiring R]
    [AddCommMonoid M] [Module R M] (v : ι → M) (w : ι → R) :
    piEquiv ι R M v w = ∑ i, w i • v i := by
  simp only [piEquiv, Basis.constr_apply_fintype, Basis.equivFun_apply]
  congr

Evaluation of Linear Equivalence Between Function Space and Linear Maps from Standard Basis

Informal description

For a finite type $\iota$, a commutative semiring $R$, and an $R$-module $M$, given a function $v \colon \iota \to M$ and a function $w \colon \iota \to R$, the evaluation of the linear equivalence $\text{piEquiv}_{\iota,R,M}(v)$ at $w$ equals the sum $\sum_{i \in \iota} w(i) \cdot v(i)$.

Module.range_piEquiv theorem

(v : ι → M) : LinearMap.range (piEquiv ι R M v) = span R (range v)

Full source

@[simp] lemma range_piEquiv (v : ι → M) :
    LinearMap.range (piEquiv ι R M v) = span R (range v) :=
  Basis.constr_range _ _

Range of Linear Equivalence Between Function Space and Linear Maps from Standard Basis Equals Span of Range

Informal description

For any function $v \colon \iota \to M$ from a finite type $\iota$ to an $R$-module $M$, the range of the linear map $\text{piEquiv}_{\iota,R,M}(v)$ is equal to the $R$-linear span of the range of $v$.

Module.surjective_piEquiv_apply_iff theorem

(v : ι → M) : Surjective (piEquiv ι R M v) ↔ span R (range v) = ⊤

Full source

@[simp] lemma surjective_piEquiv_apply_iff (v : ι → M) :
    SurjectiveSurjective (piEquiv ι R M v) ↔ span R (range v) = ⊤ := by
  rw [← LinearMap.range_eq_top, range_piEquiv]

Surjectivity Criterion for Linear Equivalence via Span Condition

Informal description

For a finite type $\iota$, a commutative semiring $R$, and an $R$-module $M$, given a function $v \colon \iota \to M$, the linear map $\text{piEquiv}_{\iota,R,M}(v)$ is surjective if and only if the $R$-linear span of the range of $v$ is the entire module $M$.

Module.Free.pi instance

 (M : ι → Type*) [Finite ι] [∀ i : ι, AddCommMonoid (M i)] [∀ i : ι, Module R (M i)] [∀ i : ι, Module.Free R (M i)] :
  Module.Free R (∀ i, M i)

Full source

/-- The product of finitely many free modules is free. -/
instance _root_.Module.Free.pi (M : ι → Type*) [Finite ι] [∀ i : ι, AddCommMonoid (M i)]
    [∀ i : ι, Module R (M i)] [∀ i : ι, Module.Free R (M i)] : Module.Free R (∀ i, M i) :=
  let ⟨_⟩ := nonempty_fintype ι
  .of_basis <| Pi.basis fun i => Module.Free.chooseBasis R (M i)

Freeness of Finite Product of Free Modules

Informal description

For a finite index set $\iota$ and a family of $R$-modules $(M_i)_{i \in \iota}$ where each $M_i$ is free, the product module $\prod_{i \in \iota} M_i$ is also free.

Module.Free.function instance

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

Full source

/-- The product of finitely many free modules is free (non-dependent version to help with typeclass
search). -/
instance _root_.Module.Free.function [Finite ι] [Module.Free R M] : Module.Free R (ι → M) :=
  Free.pi _ _

Freeness of Function Spaces over Finite Types

Informal description

For a finite type $\iota$ and a free $R$-module $M$, the function space $\iota \to M$ is also a free $R$-module.