The standard basis #
This file defines the standard basis std_basis R φ i b j, which is b where i = j and 0
elsewhere.
To give a concrete example, std_basis R (λ (i : fin 3), R) i 1 gives the ith unit basis vector
in R³, and pi.is_basis_fun proves this is a basis over fin 3 → R.
Main definitions #
linear_map.std_basis R ϕ i b: thei'th standardR-basis vector onΠ i, ϕ i, scaled byb.
Main results #
pi.is_basis_std_basis:std_basisturns a component-wise basis into a basis on the product type.pi.is_basis_fun:std_basis R (λ _, R) i 1is a basis forn → R.
def
linear_map.std_basis
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule 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 : ι), semimodule R (φ i)]
[decidable_eq ι]
(i : ι)
(b : φ i) :
⇑(linear_map.std_basis R φ i) b = function.update 0 i b
theorem
linear_map.coe_std_basis
(R : Type u_1)
{ι : Type u_2}
[semiring R]
(φ : ι → Type u_3)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), semimodule 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 : ι), semimodule 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 : ι), semimodule 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 : ι), semimodule 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 : ι), semimodule R (φ i)]
[decidable_eq ι]
(i : ι) :
(linear_map.std_basis R φ i).ker = ⊥
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 : ι), semimodule 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 : ι), semimodule 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 : ι), semimodule 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 : ι), semimodule R (φ i)]
[decidable_eq ι]
(I J : set ι)
(h : disjoint I J) :
(⨆ (i : ι) (H : i ∈ I), (linear_map.std_basis R φ i).range) ≤ ⨅ (i : ι) (H : i ∈ J), (linear_map.proj i).ker
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 : ι), semimodule R (φ i)]
[decidable_eq ι]
{I : finset ι}
{J : set ι}
(hu : set.univ ⊆ ↑I ∪ J) :
(⨅ (i : ι) (H : i ∈ J), (linear_map.proj i).ker) ≤ ⨆ (i : ι) (H : i ∈ I), (linear_map.std_basis R φ i).range
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 : ι), semimodule 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.std_basis R φ i).range) = ⨅ (i : ι) (H : i ∈ J), (linear_map.proj i).ker
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 : ι), semimodule R (φ i)]
[decidable_eq ι]
[fintype ι] :
(⨆ (i : ι), (linear_map.std_basis R φ i).range) = ⊤
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 : ι), semimodule R (φ i)]
[decidable_eq ι]
(I J : set ι)
(h : disjoint I J) :
disjoint (⨆ (i : ι) (H : i ∈ I), (linear_map.std_basis R φ i).range) (⨆ (i : ι) (H : i ∈ J), (linear_map.std_basis R φ i).range)
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))
theorem
pi.is_basis_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)]
[fintype η]
[decidable_eq η]
(s : Π (j : η), ιs j → Ms j)
(hs : ∀ (j : η), is_basis R (s j)) :
theorem
pi.is_basis_fun₀
(R : Type u_1)
(η : Type u_2)
[ring R]
[fintype η]
[decidable_eq η] :
is_basis R (λ (ji : Σ (j : η), unit), ⇑(linear_map.std_basis R (λ (i : η), R) ji.fst) 1)
theorem
pi.is_basis_fun
(R : Type u_1)
(η : Type u_2)
[ring R]
[fintype η]
[decidable_eq η] :
is_basis R (λ (i : η), ⇑(linear_map.std_basis R (λ (i : η), R) i) 1)
@[simp]
theorem
pi.is_basis_fun_repr
(R : Type u_1)
(η : Type u_2)
[ring R]
[fintype η]
[decidable_eq η]
(x : η → R)
(i : η) :