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} [Semiring R] (φ : ι → Type u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) : φ i →ₗ[R] (i : ι) → φ i

The standard basis of the product of φ.

Equations

• LinearMap.stdBasis R φ = LinearMap.single

theorem LinearMap.stdBasis_apply (R : Type u_1) {ι : Type u_2} [Semiring R] (φ : ι → Type u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) (b : φ i) : (LinearMap.stdBasis R φ i) b = Function.update 0 i b

@[simp]

theorem LinearMap.stdBasis_apply' (R : Type u_1) {ι : Type u_2} [Semiring R] [DecidableEq ι] (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} [Semiring R] (φ : ι → Type u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) : ⇑(LinearMap.stdBasis R φ i) = Pi.single i

@[simp]

theorem LinearMap.stdBasis_same (R : Type u_1) {ι : Type u_2} [Semiring R] (φ : ι → Type u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) (b : φ i) : (LinearMap.stdBasis R φ i) b i = b

theorem LinearMap.stdBasis_ne (R : Type u_1) {ι : Type u_2} [Semiring R] (φ : ι → Type u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) (j : ι) (h : j ≠ i) (b : φ i) : (LinearMap.stdBasis R φ i) b j = 0

theorem LinearMap.stdBasis_eq_pi_diag (R : Type u_1) {ι : Type u_2} [Semiring R] (φ : ι → Type u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) : LinearMap.stdBasis R φ i = LinearMap.pi (LinearMap.diag i)

theorem LinearMap.ker_stdBasis (R : Type u_1) {ι : Type u_2} [Semiring R] (φ : ι → Type u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) : LinearMap.ker (LinearMap.stdBasis R φ i) = ⊥

theorem LinearMap.proj_comp_stdBasis (R : Type u_1) {ι : Type u_2} [Semiring R] (φ : ι → Type u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) (j : ι) : LinearMap.proj i ∘ₗ LinearMap.stdBasis R φ j = LinearMap.diag j i

theorem LinearMap.proj_stdBasis_same (R : Type u_1) {ι : Type u_2} [Semiring R] (φ : ι → Type u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) : LinearMap.proj i ∘ₗ LinearMap.stdBasis R φ i = LinearMap.id

theorem LinearMap.proj_stdBasis_ne (R : Type u_1) {ι : Type u_2} [Semiring R] (φ : ι → Type u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) (j : ι) (h : i ≠ j) : LinearMap.proj i ∘ₗ LinearMap.stdBasis R φ j = 0

theorem LinearMap.iSup_range_stdBasis_le_iInf_ker_proj (R : Type u_1) {ι : Type u_2} [Semiring R] (φ : ι → Type u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (I : Set ι) (J : Set ι) (h : Disjoint I J) : ⨆ i ∈ I, LinearMap.range (LinearMap.stdBasis R φ i) ≤ ⨅ i ∈ J, LinearMap.ker (LinearMap.proj i)

theorem LinearMap.iInf_ker_proj_le_iSup_range_stdBasis (R : Type u_1) {ι : Type u_2} [Semiring R] (φ : ι → Type u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] {I : Finset ι} {J : Set ι} (hu : Set.univ ⊆ ↑I ∪ J) : ⨅ i ∈ J, LinearMap.ker (LinearMap.proj i) ≤ ⨆ i ∈ I, LinearMap.range (LinearMap.stdBasis R φ i)

theorem LinearMap.iSup_range_stdBasis_eq_iInf_ker_proj (R : Type u_1) {ι : Type u_2} [Semiring R] (φ : ι → Type u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] {I : Set ι} {J : Set ι} (hd : Disjoint I J) (hu : Set.univ ⊆ I ∪ J) (hI : Set.Finite I) : ⨆ i ∈ I, LinearMap.range (LinearMap.stdBasis R φ i) = ⨅ i ∈ J, LinearMap.ker (LinearMap.proj i)

theorem LinearMap.iSup_range_stdBasis (R : Type u_1) {ι : Type u_2} [Semiring R] (φ : ι → Type u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] [Finite ι] : ⨆ (i : ι), LinearMap.range (LinearMap.stdBasis R φ i) = ⊤

theorem LinearMap.disjoint_stdBasis_stdBasis (R : Type u_1) {ι : Type u_2} [Semiring R] (φ : ι → Type u_3) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (I : Set ι) (J : Set ι) (h : Disjoint I J) : Disjoint (⨆ i ∈ I, LinearMap.range (LinearMap.stdBasis R φ i)) (⨆ i ∈ J, LinearMap.range (LinearMap.stdBasis R φ i))

theorem LinearMap.stdBasis_eq_single (R : Type u_1) {ι : Type u_2} [Semiring R] [DecidableEq ι] {a : R} : (fun (i : ι) => (LinearMap.stdBasis R (fun (x : ι) => R) i) a) = fun (i : ι) => ⇑(Finsupp.single i a)

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)] [DecidableEq η] (v : (j : η) → ιs j → Ms 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} [Semiring R] [(i : η) → AddCommMonoid (Ms i)] [(i : η) → Module R (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.basisFun.

Equations

• Pi.basis s = { repr := LinearEquiv.trans (LinearEquiv.piCongrRight fun (j : η) => (s j).repr) (LinearEquiv.symm (Finsupp.sigmaFinsuppLEquivPiFinsupp R)) }

@[simp]

theorem Pi.basis_repr_stdBasis {R : Type u_1} {η : Type u_2} {ιs : η → Type u_3} {Ms : η → Type u_4} [Semiring R] [(i : η) → AddCommMonoid (Ms i)] [(i : η) → Module R (Ms i)] [Fintype η] [DecidableEq η] (s : (j : η) → Basis (ιs j) R (Ms j)) (j : η) (i : ιs j) : (Pi.basis s).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} [Semiring R] [(i : η) → AddCommMonoid (Ms i)] [(i : η) → Module R (Ms i)] [Fintype η] [DecidableEq η] (s : (j : η) → Basis (ιs j) R (Ms j)) (ji : (j : η) × ιs j) : (Pi.basis s) 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} [Semiring R] [(i : η) → AddCommMonoid (Ms i)] [(i : η) → Module R (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.basisFun (R : Type u_1) (η : Type u_2) [Semiring R] [Finite η] : Basis η R (η → R)

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

Equations

• Pi.basisFun R η = Basis.ofEquivFun (LinearEquiv.refl R (η → R))

@[simp]

theorem Pi.basisFun_apply (R : Type u_1) (η : Type u_2) [Semiring R] [Finite η] [DecidableEq η] (i : η) : (Pi.basisFun R η) i = (LinearMap.stdBasis R (fun (x : η) => R) i) 1

@[simp]

theorem Pi.basisFun_repr (R : Type u_1) (η : Type u_2) [Semiring R] [Finite η] (x : η → R) (i : η) : ((Pi.basisFun R η).repr x) i = x i

@[simp]

theorem Pi.basisFun_equivFun (R : Type u_1) (η : Type u_2) [Semiring R] [Finite η] : Basis.equivFun (Pi.basisFun R η) = LinearEquiv.refl R (η → R)

noncomputable def Module.piEquiv (ι : Type u_1) (R : Type u_2) (M : Type u_3) [Finite ι] [CommSemiring R] [AddCommMonoid M] [Module R M] : (ι → M) ≃ₗ[R] (ι → R) →ₗ[R] M

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

Equations

• Module.piEquiv ι R M = Basis.constr (Pi.basisFun R ι) R

theorem Module.piEquiv_apply_apply (ι : Type u_5) (R : Type u_6) (M : Type u_7) [Fintype ι] [CommSemiring R] [AddCommMonoid M] [Module R M] (v : ι → M) (w : ι → R) : ((Module.piEquiv ι R M) 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) [Finite ι] [CommSemiring R] [AddCommMonoid M] [Module R M] (v : ι → M) : LinearMap.range ((Module.piEquiv ι R M) v) = Submodule.span R (Set.range v)

@[simp]

theorem Module.surjective_piEquiv_apply_iff (ι : Type u_1) (R : Type u_2) (M : Type u_3) [Finite ι] [CommSemiring R] [AddCommMonoid M] [Module R M] (v : ι → M) : Function.Surjective ⇑((Module.piEquiv ι R M) v) ↔ Submodule.span R (Set.range v) = ⊤

noncomputable def Matrix.stdBasis (R : Type u_1) (m : Type u_2) (n : Type u_3) [Fintype m] [Finite n] [Semiring R] : Basis (m × n) R (Matrix m n R)

The standard basis of Matrix m n R.

Equations

• Matrix.stdBasis R m n = Basis.reindex (Pi.basis fun (x : m) => Pi.basisFun R n) (Equiv.sigmaEquivProd m n)

theorem Matrix.stdBasis_eq_stdBasisMatrix (R : Type u_1) {m : Type u_2} {n : Type u_3} [Fintype m] [Finite n] [Semiring R] (i : m) (j : n) [DecidableEq m] [DecidableEq n] : (Matrix.stdBasis R m n) (i, j) = Matrix.stdBasisMatrix i j 1