mathlib documentation

linear_algebra.dual

Dual vector spaces

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

Main definitions

Main results

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] :

@[instance]
def module.dual.inst (R : Type u_1) (M : Type u_2) [comm_ring R] [add_comm_group M] [module 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
@[instance]
def module.dual.inhabited (R : Type u_1) (M : Type u_2) [comm_ring R] [add_comm_group M] [module 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] :

Equations
def module.dual.eval (R : Type u_1) (M : Type u_2) [comm_ring R] [add_comm_group M] [module 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
@[simp]
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) :

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'] :

The transposition of linear maps, as a linear map from M →ₗ[R] M' to dual R M' →ₗ[R] dual R M.

Equations
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') :

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

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

Equations
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 : ι) :
((is_basis.to_dual B h) (B i)) (B j) = ite (i = j) 1 0

@[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 : ι) :
((is_basis.to_dual B h) ((finsupp.total ι V K B) f)) (B i) = f 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 : ι) :
((is_basis.to_dual B h) (B i)) ((finsupp.total ι V K B) f) = f 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 : ι) :
((is_basis.to_dual B h) v) (B i) = ((h.repr) 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) :
((is_basis.to_dual B h) (B i)) v = ((h.repr) v) i

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) :
is_basis K BV → (V →ₗ[K] K)

h.to_dual_flip v is the linear map sending w to h.to_dual w v.

Equations
def is_basis.eval_finsupp_at {K : Type u} {ι : Type w} [field K] :
ι → ((ι →₀ K) →ₗ[K] K)

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

Equations
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} :
is_basis K Bι → (V →ₗ[K] K)

h.coord_fun i sends vectors to their i'th coordinate with respect to the basis h.

Equations
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 : ι) :
(h.coord_fun i) v = ((h.repr) 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 : ι) :
((is_basis.to_dual B h) v) (B i) = ((h.repr) 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 : ι) :
((is_basis.to_dual B h) v) (B i) = (h.equiv_fun) 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) :
(is_basis.to_dual B h) v = 0v = 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} :
is_basis K Bι → module.dual K V

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

Equations
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 ι] :

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 ι] :

@[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 : ι) :
((_.repr) l) i = l (B 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 : ι) :
(_.equiv_fun) l i = l (B 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 ι] :

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 ι] :

theorem vector_space.eval_ker {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] :

theorem vector_space.erange_coe {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] :

def vector_space.eval_equiv {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] :

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

Equations
@[nolint]
structure dual_pair {K : Type u} {V : Type v} {ι : Type w} [decidable_eq ι] [field K] [add_comm_group V] [vector_space K V] :
(ι → 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} :
dual_pair e εV → ι →₀ K

The coefficients of v on the basis e

Equations
@[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 : ι) :
(h.coeffs v) i = (ε i) v

def dual_pair.lc {K : Type u} {V : Type v} {ι : Type w} [field K] [add_comm_group V] [vector_space K V] :
(ι → V)→₀ K) → V

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

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

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

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 : ι) :
(ε i) x 0i 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} :
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 ε) :