Documentation

Mathlib.LinearAlgebra.Dual.Basis

Bases of dual vector spaces #

The dual space of an $R$-module $M$ is the $R$-module of $R$-linear maps $M \to R$. This file concerns bases on dual vector spaces.

Main definitions #

Main results #

def Basis.toDual {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) :

The linear map from a vector space equipped with basis to its dual vector space, taking basis elements to corresponding dual basis elements.

Equations
Instances For
    theorem Basis.toDual_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (i j : ι) :
    (b.toDual (b i)) (b j) = if i = j then 1 else 0
    @[simp]
    theorem Basis.toDual_linearCombination_left {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) :
    (b.toDual ((Finsupp.linearCombination R b) f)) (b i) = f i
    @[simp]
    theorem Basis.toDual_linearCombination_right {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) :
    (b.toDual (b i)) ((Finsupp.linearCombination R b) f) = f i
    theorem Basis.toDual_apply_left {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) (i : ι) :
    (b.toDual m) (b i) = (b.repr m) i
    theorem Basis.toDual_apply_right {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (i : ι) (m : M) :
    (b.toDual (b i)) m = (b.repr m) i
    theorem Basis.coe_toDual_self {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (i : ι) :
    b.toDual (b i) = b.coord i
    def Basis.toDualFlip {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) :

    h.toDual_flip v is the linear map sending w to h.toDual w v.

    Equations
    Instances For
      theorem Basis.toDualFlip_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m₁ m₂ : M) :
      (b.toDualFlip m₁) m₂ = (b.toDual m₂) m₁
      theorem Basis.toDual_eq_repr {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) (i : ι) :
      (b.toDual m) (b i) = (b.repr m) i
      theorem Basis.toDual_eq_equivFun {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (m : M) (i : ι) :
      (b.toDual m) (b i) = b.equivFun m i
      theorem Basis.toDual_injective {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) :
      theorem Basis.toDual_inj {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) (a : b.toDual m = 0) :
      m = 0
      theorem Basis.toDual_ker {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) :
      theorem Basis.toDual_range {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] :
      @[simp]
      theorem Basis.sum_dual_apply_smul_coord {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) (f : Module.Dual R M) :
      x : ι, f (b x) b.coord x = f
      def Basis.toDualEquiv {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] :

      A vector space is linearly equivalent to its dual space.

      Equations
      Instances For
        @[simp]
        theorem Basis.toDualEquiv_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (m : M) :
        def Basis.dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] :
        Basis ι R (Module.Dual R M)

        Maps a basis for V to a basis for the dual space.

        Equations
        Instances For
          theorem Basis.dualBasis_apply_self {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (i j : ι) :
          (b.dualBasis i) (b j) = if j = i then 1 else 0
          theorem Basis.linearCombination_dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (f : ι →₀ R) (i : ι) :
          ((Finsupp.linearCombination R b.dualBasis) f) (b i) = f i
          @[simp]
          theorem Basis.dualBasis_repr {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (l : Module.Dual R M) (i : ι) :
          (b.dualBasis.repr l) i = l (b i)
          theorem Basis.dualBasis_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (i : ι) (m : M) :
          (b.dualBasis i) m = (b.repr m) i
          @[simp]
          theorem Basis.coe_dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] :
          @[simp]
          theorem Basis.toDual_toDual {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] :
          theorem Basis.dualBasis_equivFun {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (l : Module.Dual R M) (i : ι) :
          b.dualBasis.equivFun l i = l (b i)
          theorem Basis.eval_ker {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_1} (b : Basis ι R M) :
          theorem Basis.eval_range {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_1} [Finite ι] (b : Basis ι R M) :
          @[simp]
          theorem Basis.linearCombination_coord {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [Finite ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) :
          ((Finsupp.linearCombination R b.coord) f) (b i) = f i

          simp normal form version of linearCombination_dualBasis

          Try using Set.toFinite to dispatch a Set.Finite goal.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            structure Module.DualBases {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : ιM) (ε : ιDual R M) :

            e and ε have characteristic properties of a basis and its dual

            • eval_same (i : ι) : (ε i) (e i) = 1
            • eval_of_ne : Pairwise fun (i j : ι) => (ε i) (e j) = 0
            • total {m : M} : (∀ (i : ι), (ε i) m = 0)m = 0
            • finite (m : M) : {i : ι | (ε i) m 0}.Finite
            Instances For
              def Module.DualBases.coeffs {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιDual R M} (h : DualBases e ε) (m : M) :
              ι →₀ R

              The coefficients of v on the basis e

              Equations
              • h.coeffs m = { support := .toFinset, toFun := fun (i : ι) => (ε i) m, mem_support_toFun := }
              Instances For
                @[simp]
                theorem Module.DualBases.coeffs_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιDual R M} (h : DualBases e ε) (m : M) (i : ι) :
                (h.coeffs m) i = (ε i) m
                def Module.DualBases.lc {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_4} (e : ιM) (l : ι →₀ R) :
                M

                linear combinations of elements of e. This is a convenient abbreviation for Finsupp.linearCombination R e l

                Equations
                Instances For
                  theorem Module.DualBases.lc_def {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (e : ιM) (l : ι →₀ R) :
                  theorem Module.DualBases.dual_lc {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιDual R M} (h : DualBases e ε) (l : ι →₀ R) (i : ι) :
                  (ε i) (lc e l) = l i
                  @[simp]
                  theorem Module.DualBases.coeffs_lc {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιDual R M} (h : DualBases e ε) (l : ι →₀ R) :
                  h.coeffs (lc e l) = l
                  @[simp]
                  theorem Module.DualBases.lc_coeffs {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιDual R M} (h : DualBases e ε) (m : M) :
                  lc e (h.coeffs m) = m

                  For any m : M n, \sum_{p ∈ Q n} (ε p m) • e p = m

                  def Module.DualBases.basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιDual R M} (h : DualBases e ε) :
                  Basis ι R M

                  (h : DualBases e ε).basis shows the family of vectors e forms a basis.

                  Equations
                  Instances For
                    @[simp]
                    theorem Module.DualBases.basis_repr_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιDual R M} (h : DualBases e ε) (m : M) :
                    h.basis.repr m = h.coeffs m
                    theorem Module.DualBases.basis_repr_symm_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιDual R M} (h : DualBases e ε) (l : ι →₀ R) :
                    h.basis.repr.symm l = lc e l
                    @[simp]
                    theorem Module.DualBases.coe_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιDual R M} (h : DualBases e ε) :
                    h.basis = e
                    theorem Module.DualBases.mem_of_mem_span {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιDual R M} (h : DualBases e ε) {H : Set ι} {x : M} (hmem : x Submodule.span R (e '' H)) (i : ι) :
                    (ε i) x 0i H
                    theorem Module.DualBases.coe_dualBasis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ιM} {ε : ιDual R M} (h : DualBases e ε) [DecidableEq ι] [Finite ι] :
                    h.basis.dualBasis = ε