mathlib documentation

linear_algebra.std_basis

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 , and pi.is_basis_fun proves this is a basis over fin 3 → R.

Main definitions #

Main results #

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 : ι) :
φ i →ₗ[R] Π (i : ι), φ 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) :
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 : ι) :
@[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 : ι) :
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 : ι) :
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 : ι) :
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 : ι) :
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) :
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 jMs 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 jMs j) (hs : ∀ (j : η), is_basis R (s j)) :
is_basis R (λ (ji : Σ (j : η), ιs j), (linear_map.std_basis R Ms ji.fst) (s ji.fst ji.snd))
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 : η) :
((_.repr) x) i = x i