Dual vector spaces

The dual space of an R-module M is the R-module of linear maps M → R.

Main definitions

dual R M defines the dual space of M over R.
Given a basis for a K-vector space V, is_basis.to_dual produces a map from V to dual K V.
Given families of vectors e and ε, dual_pair e ε states that these families have the characteristic properties of a basis and a dual.

to_dual_equiv : the dual space is linearly equivalent to the primal space.
dual_pair.is_basis and dual_pair.eq_dual: if e and ε form a dual pair, e is a basis and ε is its dual basis.

We sometimes use V' as local notation for dual K V.

Because of unresolved type class issues, the following local instance can be of use:

private def help_tcs : has_scalar K V := mul_action.to_has_scalar _ _
local attribute [instance] help_tcs

The dual space of an R-module M is the R-module of linear maps M → R.

Maps a module M to the dual of the dual of M. See vector_space.eval_range and vector_space.eval_equiv.

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

Evaluation of finitely supported functions at a fixed point i, as a K-linear map.

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

A vector space is linearly equivalent to its dual space.

A vector space is linearly equivalent to the dual of its dual space.

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

The coefficients of v on the basis e

linear combinations of elements of e. This is a convenient abbreviation for finsupp.total _ V K e l

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