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 (λ (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.comp (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.comp (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.comp (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 ∈ I), LinearMap.range (LinearMap.stdBasis R φ i) ≤ ⨅ (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 : ι) (_ : i ∈ J), LinearMap.ker (LinearMap.proj i) ≤ ⨆ (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 ∈ I), LinearMap.range (LinearMap.stdBasis R φ i) = ⨅ (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 ∈ I), LinearMap.range (LinearMap.stdBasis R φ i)) (⨆ (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 => ↑fun₀ | 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 => ↑(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 Ms j) (↑(s j) i)) = fun₀ | { 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] [Fintype η] : 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] [Fintype η] [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] [Fintype η] (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] [Fintype η] : Basis.equivFun (Pi.basisFun R η) = LinearEquiv.refl R (η → R)

noncomputable def Module.piEquiv (ι : Type u_1) (R : Type u_2) (M : Type u_3) [Fintype ι] [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_1) (R : Type u_2) (M : Type u_3) [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) [Fintype ι] [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) [Fintype ι] [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] [Fintype 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 => 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] [Fintype n] [Semiring R] (i : n) (j : m) [DecidableEq n] [DecidableEq m] : ↑(Matrix.stdBasis R n m) (i, j) = Matrix.stdBasisMatrix i j 1