Documentation

Mathlib.LinearAlgebra.StdBasis

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 , and Pi.basisFun R (Fin 3) proves this is a basis over Fin 3 → R.

Main definitions #

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

Instances For
    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) :
    @[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 : ι) :
    @[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 : ι) :
    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 : ι) :
    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 : ι) :
    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 : ι) :
    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) :
    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 jMs 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.

    Instances For
      @[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.

      Instances For
        @[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 η] :
        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.

        Instances For
          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) :
          @[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) :
          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.

          Instances For
            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