# mathlibdocumentation

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

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

## Main results

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

## 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] [ M] :

@[instance]
def module.dual.inst (R : Type u_1) (M : Type u_2) [comm_ring R] [ M] :
M)

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

Equations
@[instance]
def module.dual.has_coe_to_fun (R : Type u_1) (M : Type u_2) [comm_ring R] [ M] :

Equations
• = {F := λ (x : M), M → R, coe :=
def module.dual.eval (R : Type u_1) (M : Type u_2) [comm_ring R] [ M] :
M →ₗ[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] [ M] (v : M) (a : M) :
( M) v) a = a v

def module.dual.transpose {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {M' : Type u_3} [add_comm_group M'] [ M'] :
(M →ₗ[R] M') →ₗ[R] M' →ₗ[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] [ M] {M' : Type u_3} [add_comm_group M'] [ M'] (u : M →ₗ[R] M') (l : M') :
=

theorem module.dual.transpose_comp {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {M' : Type u_3} [add_comm_group M'] [ M'] {M'' : Type u_4} [add_comm_group M''] [ M''] (u : M' →ₗ[R] M'') (v : M →ₗ[R] M') :

def is_basis.to_dual {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] [de : decidable_eq ι] (B : ι → V) :
B(V →ₗ[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] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) (i j : ι) :
( 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] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) (f : ι →₀ K) (i : ι) :
( h) ( 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] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) (f : ι →₀ K) (i : ι) :
( h) (B i)) ( V K B) f) = f i

theorem is_basis.to_dual_apply_left {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) (v : V) (i : ι) :
( 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] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) (i : ι) (v : V) :
( h) (B i)) v = ((h.repr) v) i

def is_basis.to_dual_flip {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] [de : decidable_eq ι] (B : ι → V) :
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] [ V] {B : ι → V} :
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] [ V] {B : ι → V} (h : 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] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) (v w : V) :
v) w = ( h) w) v

theorem is_basis.to_dual_eq_repr {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) (v : V) (i : ι) :
( 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] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) [fintype ι] (v : V) (i : ι) :
( 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] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) (v : V) :
h) v = 0v = 0

theorem is_basis.to_dual_ker {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) :
h).ker =

theorem is_basis.to_dual_range {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) [fin : fintype ι] :
h).range =

def is_basis.dual_basis {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] [de : decidable_eq ι] {B : ι → V} :
Bι → 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] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) :

@[simp]
theorem is_basis.dual_basis_apply_self {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] [de : decidable_eq ι] {B : ι → V} (h : 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] [ V] [de : decidable_eq ι] (B : ι → V) (h : 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] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) [fintype ι] :

@[simp]
theorem is_basis.total_dual_basis {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) [fintype ι] (f : ι →₀ K) (i : ι) :
( 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] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) [fintype ι] (l : 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] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) [fintype ι] (l : 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] [ V] [de : decidable_eq ι] {B : ι → V} (h : 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] [ V] [de : decidable_eq ι] {B : ι → V} (h : B) [fintype ι] :
.comp h) =

theorem is_basis.dual_dim_eq {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] {B : ι → V} (h : B) [fintype ι] :
V).lift = V)

theorem vector_space.eval_ker {K : Type u} {V : Type v} [field K] [ V] :
V).ker =

theorem vector_space.dual_dim_eq {K : Type u} {V : Type v} [field K] [ V] :
V).lift = V)

theorem vector_space.erange_coe {K : Type u} {V : Type v} [field K] [ V] :
V).range =

def vector_space.eval_equiv {K : Type u} {V : Type v} [field K] [ V] :
(V ≃ₗ[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] [ V] :
(ι → V)(ι → 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] [ V] {e : ι → V} {ε : ι → V} :
ε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] [ V] {e : ι → V} {ε : ι → V} (h : ε) (v : V) (i : ι) :
(h.coeffs v) i = (ε i) v

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

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

Equations
• 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] [ V] {e : ι → V} {ε : ι → V} (h : ε) (l : ι →₀ K) (i : ι) :
(ε i) l) = l i

@[simp]
theorem dual_pair.coeffs_lc {K : Type u} {V : Type v} {ι : Type w} [dι : decidable_eq ι] [field K] [ V] {e : ι → V} {ε : ι → V} (h : ε) (l : ι →₀ K) :
h.coeffs l) = l

theorem dual_pair.decomposition {K : Type u} {V : Type v} {ι : Type w} [dι : decidable_eq ι] [field K] [ V] {e : ι → V} {ε : ι → V} (h : ε) (v : V) :
(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] [ V] {e : ι → V} {ε : ι → V} (h : ε) {H : set ι} {x : V} (hmem : x (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] [ V] {e : ι → V} {ε : ι → V} :
ε e

theorem dual_pair.eq_dual {K : Type u} {V : Type v} {ι : Type w} [dι : decidable_eq ι] [field K] [ V] {e : ι → V} {ε : ι → V} (h : ε) :