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' = Pi.single 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, Pi.single (i : Fin 3) (1 : R) 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

• 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 = Pi.single i 1 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.

@[deprecated LinearMap.single]

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 R φ

@[deprecated Pi.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, deprecated Pi.single_apply]

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

@[deprecated LinearMap.coe_single]

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, deprecated Pi.single_eq_same]

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

@[deprecated Pi.single_eq_of_ne]

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

@[deprecated LinearMap.single_eq_pi_diag]

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)

@[deprecated LinearMap.ker_single]

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) = ⊥

@[deprecated LinearMap.proj_comp_single]

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

@[deprecated LinearMap.proj_comp_single_same]

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

@[deprecated LinearMap.proj_comp_single_ne]

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

@[deprecated LinearMap.iSup_range_single_le_iInf_ker_proj]

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)

@[deprecated LinearMap.iInf_ker_proj_le_iSup_range_single]

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)

@[deprecated LinearMap.iSup_range_single_eq_iInf_ker_proj]

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 : I.Finite) : ⨆ i ∈ I, LinearMap.range (LinearMap.stdBasis R φ i) = ⨅ i ∈ J, LinearMap.ker (LinearMap.proj i)

@[deprecated LinearMap.iSup_range_single]

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) = ⊤

@[deprecated LinearMap.disjoint_single_single]

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))

@[deprecated]

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_single {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) => Pi.single ji.fst (v ji.fst ji.snd)

@[deprecated Pi.linearIndependent_single]

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.piCongrRight fun (j : η) => (s j).repr) ≪≫ₗ (Finsupp.sigmaFinsuppLEquivPiFinsupp R).symm }

@[simp]

theorem Pi.basis_repr_single {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 (Pi.single j ((s j) i)) = Finsupp.single ⟨j, i⟩ 1

@[simp, deprecated Pi.basis_repr_single]

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)) = 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 : η) → 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 = Pi.single 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 = Pi.single 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 η] : (Pi.basisFun R η).equivFun = 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 = (Pi.basisFun R ι).constr 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 = ∑ 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 Basis.matrix {ι : Type u_1} {R : Type u_2} {M : Type u_3} (m : Type u_4) (n : Type u_5) [Fintype m] [Fintype n] [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : Basis (m × n × ι) R (Matrix m n M)

The standard basis of Matrix m n M given a basis on M.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Basis.matrix_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {m : Type u_4} {n : Type u_5} [Fintype m] [Fintype n] [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : m) (j : n) (k : ι) [DecidableEq m] [DecidableEq n] : (Basis.matrix m n b) (i, j, k) = Matrix.stdBasisMatrix i j (b k)

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 = ((Pi.basis fun (x : m) => Pi.basisFun R n).reindex (Equiv.sigmaEquivProd m n)).map (Matrix.ofLinearEquiv R)

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