# 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' = LinearMap.stdBasis 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.basisFun.

To give a concrete example, LinearMap.stdBasis R (fun (i : Fin 3) ↦ R) i 1 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 #

• LinearMap.stdBasis R M: if x is a basis vector of M i, then LinearMap.stdBasis 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.basisFun R η: the standard basis on R^η, i.e. η → R, given by Pi.basisFun R η i 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.
def LinearMap.stdBasis (R : Type u_1) {ι : Type u_2} [] (φ : ιType u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (i : ι) :
φ i →ₗ[R] (i : ι) → φ i

The standard basis of the product of φ.

Equations
• = LinearMap.single
Instances For
theorem LinearMap.stdBasis_apply (R : Type u_1) {ι : Type u_2} [] (φ : ιType u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (i : ι) (b : φ i) :
() b =
@[simp]
theorem LinearMap.stdBasis_apply' (R : Type u_1) {ι : Type u_2} [] [] (i : ι) (i' : ι) :
(LinearMap.stdBasis R (fun (_x : ι) => R) i) 1 i' = if i = i' then 1 else 0
theorem LinearMap.coe_stdBasis (R : Type u_1) {ι : Type u_2} [] (φ : ιType u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (i : ι) :
() =
@[simp]
theorem LinearMap.stdBasis_same (R : Type u_1) {ι : Type u_2} [] (φ : ιType u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (i : ι) (b : φ i) :
() b i = b
theorem LinearMap.stdBasis_ne (R : Type u_1) {ι : Type u_2} [] (φ : ιType u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (i : ι) (j : ι) (h : j i) (b : φ i) :
() b j = 0
theorem LinearMap.stdBasis_eq_pi_diag (R : Type u_1) {ι : Type u_2} [] (φ : ιType u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (i : ι) :
theorem LinearMap.ker_stdBasis (R : Type u_1) {ι : Type u_2} [] (φ : ιType u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (i : ι) :
theorem LinearMap.proj_comp_stdBasis (R : Type u_1) {ι : Type u_2} [] (φ : ιType u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (i : ι) (j : ι) :
∘ₗ =
theorem LinearMap.proj_stdBasis_same (R : Type u_1) {ι : Type u_2} [] (φ : ιType u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (i : ι) :
∘ₗ = LinearMap.id
theorem LinearMap.proj_stdBasis_ne (R : Type u_1) {ι : Type u_2} [] (φ : ιType u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (i : ι) (j : ι) (h : i j) :
∘ₗ = 0
theorem LinearMap.iSup_range_stdBasis_le_iInf_ker_proj (R : Type u_1) {ι : Type u_2} [] (φ : ιType u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (I : Set ι) (J : Set ι) (h : Disjoint I J) :
⨆ i ∈ I, ⨅ i ∈ J,
theorem LinearMap.iInf_ker_proj_le_iSup_range_stdBasis (R : Type u_1) {ι : Type u_2} [] (φ : ιType u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] {I : } {J : Set ι} (hu : Set.univ I J) :
⨅ i ∈ J, ⨆ i ∈ I,
theorem LinearMap.iSup_range_stdBasis_eq_iInf_ker_proj (R : Type u_1) {ι : Type u_2} [] (φ : ιType u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] {I : Set ι} {J : Set ι} (hd : Disjoint I J) (hu : Set.univ I J) (hI : ) :
⨆ i ∈ I, = ⨅ i ∈ J,
theorem LinearMap.iSup_range_stdBasis (R : Type u_1) {ι : Type u_2} [] (φ : ιType u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] [] :
⨆ (i : ι), =
theorem LinearMap.disjoint_stdBasis_stdBasis (R : Type u_1) {ι : Type u_2} [] (φ : ιType u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [] (I : Set ι) (J : Set ι) (h : Disjoint I J) :
Disjoint (⨆ i ∈ I, ) (⨆ i ∈ J, )
theorem LinearMap.stdBasis_eq_single (R : Type u_1) {ι : Type u_2} [] [] {a : R} :
(fun (i : ι) => (LinearMap.stdBasis R (fun (x : ι) => R) i) a) = fun (i : ι) => ()
theorem Pi.linearIndependent_stdBasis {R : Type u_1} {η : Type u_2} {ιs : ηType u_3} {Ms : ηType u_4} [Ring R] [(i : η) → AddCommGroup (Ms i)] [(i : η) → Module R (Ms i)] [] (v : (j : η) → ιs jMs j) (hs : ∀ (i : η), LinearIndependent R (v i)) :
LinearIndependent R fun (ji : (j : η) × ιs j) => (LinearMap.stdBasis R Ms ji.fst) (v ji.fst ji.snd)
noncomputable def Pi.basis {R : Type u_1} {η : Type u_2} {ιs : ηType u_3} {Ms : ηType u_4} [] [(i : η) → AddCommMonoid (Ms i)] [(i : η) → Module R (Ms i)] [] (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.basisFun.

Equations
Instances For
@[simp]
theorem Pi.basis_repr_stdBasis {R : Type u_1} {η : Type u_2} {ιs : ηType u_3} {Ms : ηType u_4} [] [(i : η) → AddCommMonoid (Ms i)] [(i : η) → Module R (Ms i)] [] [] (s : (j : η) → Basis (ιs j) R (Ms j)) (j : η) (i : ιs j) :
().repr ((LinearMap.stdBasis R (fun (j : η) => Ms j) j) ((s j) i)) = Finsupp.single { fst := j, snd := i } 1
@[simp]
theorem Pi.basis_apply {R : Type u_1} {η : Type u_2} {ιs : ηType u_3} {Ms : ηType u_4} [] [(i : η) → AddCommMonoid (Ms i)] [(i : η) → Module R (Ms i)] [] [] (s : (j : η) → Basis (ιs j) R (Ms j)) (ji : (j : η) × ιs j) :
() ji = (LinearMap.stdBasis R 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} [] [(i : η) → AddCommMonoid (Ms i)] [(i : η) → Module R (Ms i)] [] (s : (j : η) → Basis (ιs j) R (Ms j)) (x : (j : η) → Ms j) (ji : (j : η) × ιs j) :
(().repr x) ji = ((s ji.fst).repr (x ji.fst)) ji.snd
noncomputable def Pi.basisFun (R : Type u_1) (η : Type u_2) [] [] :
Basis η R (ηR)

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

Equations
Instances For
@[simp]
theorem Pi.basisFun_apply (R : Type u_1) (η : Type u_2) [] [] [] (i : η) :
() i = (LinearMap.stdBasis R (fun (x : η) => R) i) 1
@[simp]
theorem Pi.basisFun_repr (R : Type u_1) (η : Type u_2) [] [] (x : ηR) (i : η) :
(().repr x) i = x i
@[simp]
theorem Pi.basisFun_equivFun (R : Type u_1) (η : Type u_2) [] [] :
= LinearEquiv.refl R (ηR)
noncomputable def Module.piEquiv (ι : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module R M] :
(ιM) ≃ₗ[R] (ιR) →ₗ[R] M

The natural linear equivalence: Mⁱ ≃ Hom(Rⁱ, M) for an R-module M.

Equations
Instances For
theorem Module.piEquiv_apply_apply (ι : Type u_5) (R : Type u_6) (M : Type u_7) [] [] [] [Module R M] (v : ιM) (w : ιR) :
(() v) w = Finset.sum Finset.univ fun (i : ι) => w i v i
@[simp]
theorem Module.range_piEquiv (ι : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module R M] (v : ιM) :
@[simp]
theorem Module.surjective_piEquiv_apply_iff (ι : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module R M] (v : ιM) :
noncomputable def Matrix.stdBasis (R : Type u_1) (m : Type u_2) (n : Type u_3) [] [] [] :
Basis (m × n) R (Matrix m n R)

The standard basis of Matrix m n R.

Equations
Instances For
theorem Matrix.stdBasis_eq_stdBasisMatrix (R : Type u_1) {m : Type u_2} {n : Type u_3} [] [] [] (i : m) (j : n) [] [] :
() (i, j) =