# mathlib3documentation

linear_algebra.std_basis

# 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: if x is a basis vector of M i, then linear_map.std_basis R M i x is the ith standard basis vector of Π i, M i.
• pi.basis s: given a basis s i for each M i, the standard basis on Π i, M i
• pi.basis_fun R η: the standard basis on R^η, i.e. η → R, given by pi.basis_fun R η i j = if i = j then 1 else 0.
• matrix.std_basis R n m: the standard basis on matrix n m R, given by matrix.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 : ι), (φ 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 : ι), (φ i)] [decidable_eq ι] (i : ι) (b : φ i) :
i) b = b
@[simp]
theorem linear_map.std_basis_apply' (R : Type u_1) {ι : Type u_2} [semiring R] [decidable_eq ι] (i i' : ι) :
(λ (_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 : ι), (φ i)] [decidable_eq ι] (i : ι) :
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 : ι), (φ i)] [decidable_eq ι] (i : ι) (b : φ i) :
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 : ι), (φ i)] [decidable_eq ι] (i j : ι) (h : j i) (b : φ i) :
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 : ι), (φ 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 : ι), (φ 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 : ι), (φ i)] [decidable_eq ι] (i j : ι) :
.comp 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 : ι), (φ 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 : ι), (φ i)] [decidable_eq ι] (i j : ι) (h : i j) :
.comp 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 : ι), (φ i)] [decidable_eq ι] (I J : set ι) (h : J) :
( (i : ι) (H : i I), linear_map.range i)) (i : ι) (H : i J),
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 : ι), (φ i)] [decidable_eq ι] {I : finset ι} {J : set ι} (hu : set.univ I J) :
( (i : ι) (H : i J), (i : ι) (H : i 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 : ι), (φ i)] [decidable_eq ι] {I J : set ι} (hd : J) (hu : set.univ I J) (hI : I.finite) :
( (i : ι) (H : i I), linear_map.range i)) = (i : ι) (H : i J),
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 : ι), (φ i)] [decidable_eq ι] [finite ι] :
( (i : ι), linear_map.range 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 : ι), (φ i)] [decidable_eq ι] (I J : set ι) (h : J) :
disjoint ( (i : ι) (H : i I), linear_map.range i)) ( (i : ι) (H : i J), linear_map.range i))
theorem linear_map.std_basis_eq_single (R : Type u_1) {ι : Type u_2} [semiring R] [decidable_eq ι] {a : R} :
(λ (i : ι), (λ (_x : ι), R) i) a) = λ (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 : η), (Ms i)] [decidable_eq η] (v : Π (j : η), ιs j Ms j) (hs : (i : η), (v i)) :
(λ (ji : Σ (j : η), ιs j), 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 : η), (Ms i)] [fintype η] (s : Π (j : η), basis (ιs j) R (Ms j)) :
basis (Σ (j : η), ιs j) R (Π (j : η), 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
@[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 : η), (Ms i)] [fintype η] [decidable_eq η] (s : Π (j : η), basis (ιs j) R (Ms j)) (j : η) (i : ιs j) :
((pi.basis s).repr) ( (λ (j : η), Ms j) j) ((s j) i)) = finsupp.single j, i⟩ 1
@[simp]
theorem pi.basis_apply {R : Type u_1} {η : Type u_2} {ιs : η Type u_3} {Ms : η Type u_4} [semiring R] [Π (i : η), add_comm_monoid (Ms i)] [Π (i : η), (Ms i)] [fintype η] [decidable_eq η] (s : Π (j : η), basis (ιs j) R (Ms j)) (ji : Σ (j : η), (λ (j : η), ιs j) j) :
(pi.basis s) ji = Ms ji.fst) ((s ji.fst) ji.snd)
@[simp]
theorem pi.basis_repr {R : Type u_1} {η : Type u_2} {ιs : η Type u_3} {Ms : η Type u_4} [semiring R] [Π (i : η), add_comm_monoid (Ms i)] [Π (i : η), (Ms i)] [fintype η] (s : Π (j : η), basis (ιs j) R (Ms j)) (x : Π (j : η), Ms j) (ji : Σ (j : η), ιs j) :
(((pi.basis s).repr) x) ji = (((s ji.fst).repr) (x ji.fst)) ji.snd
noncomputable def pi.basis_fun (R : Type u_1) (η : Type u_2) [semiring R] [fintype η] :
R R)

The basis on η → R where the ith basis vector is function.update 0 i 1.

Equations
@[simp]
theorem pi.basis_fun_apply (R : Type u_1) (η : Type u_2) [semiring R] [fintype η] [decidable_eq η] (i : η) :
η) i = (λ (i : η), R) i) 1
@[simp]
theorem pi.basis_fun_repr (R : Type u_1) (η : Type u_2) [semiring R] [fintype η] (x : η R) (i : η) :
(((pi.basis_fun R η).repr) x) i = x i
@[simp]
theorem pi.basis_fun_equiv_fun (R : Type u_1) (η : Type u_2) [semiring R] [fintype η] :
η).equiv_fun = R)
noncomputable def matrix.std_basis (R : Type u_1) (m : Type u_2) (n : Type u_3) [fintype m] [fintype n] [semiring R] :
basis (m × n) R (matrix m n R)

The standard basis of matrix m n R.

Equations
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] :
n m) (i, j) =