The standard basis #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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' = linear_map.std_basis R M j' (s j) i = if j = j' then s i else 0.
The standard basis on R^η, i.e. η → R is called pi.basis_fun.
To give a concrete example, linear_map.std_basis R (λ (i : fin 3), R) i 1
gives the ith unit basis vector in R³, and pi.basis_fun R (fin 3) proves
this is a basis over fin 3 → R.
Main definitions #
linear_map.std_basis R M: ifxis a basis vector ofM i, thenlinear_map.std_basis R M i xis theith standard basis vector ofΠ i, M i.pi.basis s: given a basiss ifor eachM i, the standard basis onΠ i, M ipi.basis_fun R η: the standard basis onR^η, i.e.η → R, given bypi.basis_fun R η i j = if i = j then 1 else 0.matrix.std_basis R n m: the standard basis onmatrix n m R, given bymatrix.std_basis R n m (i, j) i' j' = if (i, j) = (i', j') then 1 else 0.
def
linear_map.std_basis
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i : ι) :
The standard basis of the product of φ.
Equations
theorem
linear_map.std_basis_apply
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i : ι)
(b : φ i) :
⇑(linear_map.std_basis R φ i) b = function.update 0 i b
@[simp]
theorem
linear_map.std_basis_apply'
(R : Type u_1)
{ι : Type u_2}
[semiring R]
[decidable_eq ι]
(i i' : ι) :
⇑(linear_map.std_basis R (λ (_x : ι), R) i) 1 i' = ite (i = i') 1 0
theorem
linear_map.coe_std_basis
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i : ι) :
⇑(linear_map.std_basis R φ i) = pi.single i
@[simp]
theorem
linear_map.std_basis_same
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i : ι)
(b : φ i) :
⇑(linear_map.std_basis R φ i) b i = b
theorem
linear_map.std_basis_ne
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i j : ι)
(h : j ≠ i)
(b : φ i) :
⇑(linear_map.std_basis R φ i) b j = 0
theorem
linear_map.std_basis_eq_pi_diag
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i : ι) :
linear_map.std_basis R φ i = linear_map.pi (linear_map.diag i)
theorem
linear_map.ker_std_basis
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i : ι) :
linear_map.ker (linear_map.std_basis R φ i) = ⊥
theorem
linear_map.proj_comp_std_basis
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i j : ι) :
(linear_map.proj i).comp (linear_map.std_basis R φ j) = linear_map.diag j i
theorem
linear_map.proj_std_basis_same
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i : ι) :
(linear_map.proj i).comp (linear_map.std_basis R φ i) = linear_map.id
theorem
linear_map.proj_std_basis_ne
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i j : ι)
(h : i ≠ j) :
(linear_map.proj i).comp (linear_map.std_basis R φ j) = 0
theorem
linear_map.supr_range_std_basis_le_infi_ker_proj
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(I J : set ι)
(h : disjoint I J) :
(⨆ (i : ι) (H : i ∈ I), linear_map.range (linear_map.std_basis R φ i)) ≤ ⨅ (i : ι) (H : i ∈ J), linear_map.ker (linear_map.proj i)
theorem
linear_map.infi_ker_proj_le_supr_range_std_basis
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
{I : finset ι}
{J : set ι}
(hu : set.univ ⊆ ↑I ∪ J) :
(⨅ (i : ι) (H : i ∈ J), linear_map.ker (linear_map.proj i)) ≤ ⨆ (i : ι) (H : i ∈ I), linear_map.range (linear_map.std_basis R φ i)
theorem
linear_map.supr_range_std_basis_eq_infi_ker_proj
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
{I J : set ι}
(hd : disjoint I J)
(hu : set.univ ⊆ I ∪ J)
(hI : I.finite) :
(⨆ (i : ι) (H : i ∈ I), linear_map.range (linear_map.std_basis R φ i)) = ⨅ (i : ι) (H : i ∈ J), linear_map.ker (linear_map.proj i)
theorem
linear_map.supr_range_std_basis
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
[finite ι] :
(⨆ (i : ι), linear_map.range (linear_map.std_basis R φ i)) = ⊤
theorem
linear_map.disjoint_std_basis_std_basis
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(I J : set ι)
(h : disjoint I J) :
disjoint (⨆ (i : ι) (H : i ∈ I), linear_map.range (linear_map.std_basis R φ i)) (⨆ (i : ι) (H : i ∈ J), linear_map.range (linear_map.std_basis R φ i))
theorem
linear_map.std_basis_eq_single
(R : Type u_1)
{ι : Type u_2}
[semiring R]
[decidable_eq ι]
{a : R} :
(λ (i : ι), ⇑(linear_map.std_basis R (λ (_x : ι), R) i) a) = λ (i : ι), ⇑(finsupp.single i a)
theorem
pi.linear_independent_std_basis
{R : Type u_1}
{η : Type u_2}
{ιs : η → Type u_3}
{Ms : η → Type u_4}
[ring R]
[Π (i : η), add_comm_group (Ms i)]
[Π (i : η), module R (Ms i)]
[decidable_eq η]
(v : Π (j : η), ιs j → Ms j)
(hs : ∀ (i : η), linear_independent R (v i)) :
linear_independent R (λ (ji : Σ (j : η), ιs j), ⇑(linear_map.std_basis R Ms ji.fst) (v ji.fst ji.snd))
@[protected]
noncomputable
def
pi.basis
{R : Type u_1}
{η : Type u_2}
{ιs : η → Type u_3}
{Ms : η → Type u_4}
[semiring R]
[Π (i : η), add_comm_monoid (Ms i)]
[Π (i : η), module R (Ms i)]
[fintype η]
(s : Π (j : η), basis (ιs j) R (Ms j)) :
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.basis_fun.
Equations
- pi.basis s = {repr := (linear_equiv.Pi_congr_right (λ (j : η), (s j).repr)).trans (finsupp.sigma_finsupp_lequiv_pi_finsupp R).symm}
@[simp]
theorem
pi.basis_repr_std_basis
{R : Type u_1}
{η : Type u_2}
{ιs : η → Type u_3}
{Ms : η → Type u_4}
[semiring R]
[Π (i : η), add_comm_monoid (Ms i)]
[Π (i : η), module R (Ms i)]
[fintype η]
[decidable_eq η]
(s : Π (j : η), basis (ιs j) R (Ms j))
(j : η)
(i : ιs j) :
⇑((pi.basis s).repr) (⇑(linear_map.std_basis R (λ (j : η), Ms j) j) (⇑(s j) i)) = finsupp.single ⟨j, i⟩ 1
The basis on η → R where the ith basis vector is function.update 0 i 1.
Equations
- pi.basis_fun R η = basis.of_equiv_fun (linear_equiv.refl R (η → R))
@[simp]
theorem
pi.basis_fun_apply
(R : Type u_1)
(η : Type u_2)
[semiring R]
[fintype η]
[decidable_eq η]
(i : η) :
⇑(pi.basis_fun R η) i = ⇑(linear_map.std_basis R (λ (i : η), R) i) 1
@[simp]
theorem
pi.basis_fun_equiv_fun
(R : Type u_1)
(η : Type u_2)
[semiring R]
[fintype η] :
(pi.basis_fun R η).equiv_fun = linear_equiv.refl R (η → R)
noncomputable
def
matrix.std_basis
(R : Type u_1)
(m : Type u_2)
(n : Type u_3)
[fintype m]
[fintype n]
[semiring R] :
The standard basis of matrix m n R.
Equations
- matrix.std_basis R m n = (pi.basis (λ (i : m), pi.basis_fun R n)).reindex (equiv.sigma_equiv_prod m n)
theorem
matrix.std_basis_eq_std_basis_matrix
(R : Type u_1)
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
[semiring R]
(i : n)
(j : m)
[decidable_eq n]
[decidable_eq m] :
⇑(matrix.std_basis R n m) (i, j) = matrix.std_basis_matrix i j 1