Dual vector spaces
The dual space of an R-module M is the R-module of linear maps M → R.
Main definitions
dual R Mdefines the dual space of M over R.- Given a basis for a K-vector space
V,is_basis.to_dualproduces a map fromVtodual K V. - Given families of vectors
eandε,dual_pair e εstates that these families have the characteristic properties of a basis and a dual.
Main results
to_dual_equiv: the dual space is linearly equivalent to the primal space.dual_pair.is_basisanddual_pair.eq_dual: ifeandεform a dual pair,eis a basis andεis its dual basis.
Notation
We sometimes use V' as local notation for dual K V.
@[instance]
def
module.dual.add_comm_group
(R : Type u_1)
(M : Type u_2)
[comm_ring R]
[add_comm_group M]
[module R M] :
add_comm_group (module.dual R M)
@[instance]
def
module.dual.inst
(R : Type u_1)
(M : Type u_2)
[comm_ring R]
[add_comm_group M]
[module R M] :
module R (module.dual R M)
def
module.dual
(R : Type u_1)
(M : Type u_2)
[comm_ring R]
[add_comm_group M]
[module R M] :
Type (max u_2 u_1)
The dual space of an R-module M is the R-module of linear maps M → R.
Equations
- module.dual R M = (M →ₗ[R] R)
@[instance]
def
module.dual.inhabited
(R : Type u_1)
(M : Type u_2)
[comm_ring R]
[add_comm_group M]
[module R M] :
inhabited (module.dual R M)
Equations
@[instance]
def
module.dual.has_coe_to_fun
(R : Type u_1)
(M : Type u_2)
[comm_ring R]
[add_comm_group M]
[module R M] :
has_coe_to_fun (module.dual R M)
Equations
- module.dual.has_coe_to_fun R M = {F := λ (x : module.dual R M), M → R, coe := linear_map.to_fun semiring.to_semimodule}
def
module.dual.eval
(R : Type u_1)
(M : Type u_2)
[comm_ring R]
[add_comm_group M]
[module R M] :
M →ₗ[R] module.dual R (module.dual R M)
Maps a module M to the dual of the dual of M. See vector_space.erange_coe and
vector_space.eval_equiv.
Equations
theorem
module.dual.eval_apply
(R : Type u_1)
(M : Type u_2)
[comm_ring R]
[add_comm_group M]
[module R M]
(v : M)
(a : module.dual R M) :
⇑(⇑(module.dual.eval R M) v) a = ⇑a v
def
module.dual.transpose
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M'] :
(M →ₗ[R] M') →ₗ[R] module.dual R M' →ₗ[R] module.dual R M
The transposition of linear maps, as a linear map from M →ₗ[R] M' to
dual R M' →ₗ[R] dual R M.
Equations
- module.dual.transpose = (linear_map.llcomp R M M' R).flip
theorem
module.dual.transpose_apply
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
(u : M →ₗ[R] M')
(l : module.dual R M') :
⇑(⇑module.dual.transpose u) l = linear_map.comp l u
theorem
module.dual.transpose_comp
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
{M'' : Type u_4}
[add_comm_group M'']
[module R M'']
(u : M' →ₗ[R] M'')
(v : M →ₗ[R] M') :
⇑module.dual.transpose (u.comp v) = (⇑module.dual.transpose v).comp (⇑module.dual.transpose u)
def
is_basis.to_dual
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B) :
V →ₗ[K] module.dual K V
The linear map from a vector space equipped with basis to its dual vector space, taking basis elements to corresponding dual basis elements.
theorem
is_basis.to_dual_apply
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
(i j : ι) :
@[simp]
theorem
is_basis.to_dual_total_left
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
(f : ι →₀ K)
(i : ι) :
@[simp]
theorem
is_basis.to_dual_total_right
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
(f : ι →₀ K)
(i : ι) :
theorem
is_basis.to_dual_apply_left
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
(v : V)
(i : ι) :
theorem
is_basis.to_dual_apply_right
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
(i : ι)
(v : V) :
def
is_basis.to_dual_flip
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
(v : V) :
Equations
- h.to_dual_flip v = h.to_dual.flip.to_fun v
def
is_basis.coord_fun
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
{B : ι → V}
(h : is_basis K B)
(i : ι) :
Equations
- h.coord_fun i = (is_basis.eval_finsupp_at i).comp h.repr
theorem
is_basis.coord_fun_eq_repr
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
{B : ι → V}
(h : is_basis K B)
(v : V)
(i : ι) :
theorem
is_basis.to_dual_swap_eq_to_dual
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
(v w : V) :
theorem
is_basis.to_dual_eq_repr
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
(v : V)
(i : ι) :
theorem
is_basis.to_dual_eq_equiv_fun
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
[fintype ι]
(v : V)
(i : ι) :
theorem
is_basis.to_dual_inj
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
(v : V)
(a : ⇑(h.to_dual) v = 0) :
v = 0
theorem
is_basis.to_dual_ker
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B) :
theorem
is_basis.to_dual_range
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
[fin : fintype ι] :
def
is_basis.dual_basis
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
(a : ι) :
module.dual K V
Maps a basis for V to a basis for the dual space.
Equations
- h.dual_basis = λ (i : ι), ⇑(h.to_dual) (B i)
theorem
is_basis.dual_lin_independent
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B) :
@[simp]
theorem
is_basis.dual_basis_apply_self
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
(i j : ι) :
⇑(h.dual_basis i) (B j) = ite (i = j) 1 0
def
is_basis.to_dual_equiv
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
[fintype ι] :
V ≃ₗ[K] module.dual K V
A vector space is linearly equivalent to its dual space.
Equations
theorem
is_basis.dual_basis_is_basis
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
[fintype ι] :
is_basis K h.dual_basis
@[simp]
theorem
is_basis.total_dual_basis
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
[fintype ι]
(f : ι →₀ K)
(i : ι) :
⇑(⇑(finsupp.total ι (module.dual K V) K h.dual_basis) f) (B i) = ⇑f i
theorem
is_basis.dual_basis_repr
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
[fintype ι]
(l : module.dual K V)
(i : ι) :
theorem
is_basis.dual_basis_equiv_fun
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
[fintype ι]
(l : module.dual K V)
(i : ι) :
theorem
is_basis.dual_basis_apply
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
[fintype ι]
(i : ι)
(v : V) :
⇑(h.dual_basis i) v = ⇑(h.equiv_fun) v i
@[simp]
theorem
is_basis.to_dual_to_dual
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[de : decidable_eq ι]
{B : ι → V}
(h : is_basis K B)
[fintype ι] :
_.to_dual.comp h.to_dual = module.dual.eval K V
theorem
is_basis.dual_dim_eq
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
{B : ι → V}
(h : is_basis K B)
[fintype ι] :
(vector_space.dim K V).lift = vector_space.dim K (module.dual K V)
theorem
vector_space.eval_ker
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V] :
(module.dual.eval K V).ker = ⊥
theorem
vector_space.dual_dim_eq
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
(h : vector_space.dim K V < cardinal.omega) :
(vector_space.dim K V).lift = vector_space.dim K (module.dual K V)
theorem
vector_space.erange_coe
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
(h : vector_space.dim K V < cardinal.omega) :
(module.dual.eval K V).range = ⊤
def
vector_space.eval_equiv
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
(h : vector_space.dim K V < cardinal.omega) :
V ≃ₗ[K] module.dual K (module.dual K V)
A vector space is linearly equivalent to the dual of its dual space.
Equations
structure
dual_pair
{K : Type u}
{V : Type v}
{ι : Type w}
[decidable_eq ι]
[field K]
[add_comm_group V]
[vector_space K V]
(e : ι → V)
(ε : ι → module.dual K V) :
Type (max v w)
- eval : ∀ (i j : ι), ⇑(ε i) (e j) = ite (i = j) 1 0
- total : ∀ {v : V}, (∀ (i : ι), ⇑(ε i) v = 0) → v = 0
- finite : Π (v : V), fintype ↥{i : ι | ⇑(ε i) v ≠ 0}
e and ε have characteristic properties of a basis and its dual
def
dual_pair.coeffs
{K : Type u}
{V : Type v}
{ι : Type w}
[dι : decidable_eq ι]
[field K]
[add_comm_group V]
[vector_space K V]
{e : ι → V}
{ε : ι → module.dual K V}
(h : dual_pair e ε)
(v : V) :
ι →₀ K
The coefficients of v on the basis e
@[simp]
theorem
dual_pair.coeffs_apply
{K : Type u}
{V : Type v}
{ι : Type w}
[dι : decidable_eq ι]
[field K]
[add_comm_group V]
[vector_space K V]
{e : ι → V}
{ε : ι → module.dual K V}
(h : dual_pair e ε)
(v : V)
(i : ι) :
def
dual_pair.lc
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
(e : ι → V)
(l : ι →₀ K) :
V
linear combinations of elements of e.
This is a convenient abbreviation for finsupp.total _ V K e l
Equations
- dual_pair.lc e l = l.sum (λ (i : ι) (a : K), a • e i)
theorem
dual_pair.dual_lc
{K : Type u}
{V : Type v}
{ι : Type w}
[dι : decidable_eq ι]
[field K]
[add_comm_group V]
[vector_space K V]
{e : ι → V}
{ε : ι → module.dual K V}
(h : dual_pair e ε)
(l : ι →₀ K)
(i : ι) :
⇑(ε i) (dual_pair.lc e l) = ⇑l i
@[simp]
theorem
dual_pair.coeffs_lc
{K : Type u}
{V : Type v}
{ι : Type w}
[dι : decidable_eq ι]
[field K]
[add_comm_group V]
[vector_space K V]
{e : ι → V}
{ε : ι → module.dual K V}
(h : dual_pair e ε)
(l : ι →₀ K) :
h.coeffs (dual_pair.lc e l) = l
theorem
dual_pair.decomposition
{K : Type u}
{V : Type v}
{ι : Type w}
[dι : decidable_eq ι]
[field K]
[add_comm_group V]
[vector_space K V]
{e : ι → V}
{ε : ι → module.dual K V}
(h : dual_pair e ε)
(v : V) :
dual_pair.lc e (h.coeffs v) = v
For any v : V n, \sum_{p ∈ Q n} (ε p v) • e p = v
theorem
dual_pair.mem_of_mem_span
{K : Type u}
{V : Type v}
{ι : Type w}
[dι : decidable_eq ι]
[field K]
[add_comm_group V]
[vector_space K V]
{e : ι → V}
{ε : ι → module.dual K V}
(h : dual_pair e ε)
{H : set ι}
{x : V}
(hmem : x ∈ submodule.span K (e '' H))
(i : ι)
(a : ⇑(ε i) x ≠ 0) :
i ∈ H
theorem
dual_pair.is_basis
{K : Type u}
{V : Type v}
{ι : Type w}
[dι : decidable_eq ι]
[field K]
[add_comm_group V]
[vector_space K V]
{e : ι → V}
{ε : ι → module.dual K V}
(h : dual_pair e ε) :
is_basis K e
theorem
dual_pair.eq_dual
{K : Type u}
{V : Type v}
{ι : Type w}
[dι : decidable_eq ι]
[field K]
[add_comm_group V]
[vector_space K V]
{e : ι → V}
{ε : ι → module.dual K V}
(h : dual_pair e ε) :
ε = _.dual_basis