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.

TODO #

Erdös-Kaplansky theorem about the dimension of a dual vector space in case of infinite dimension.

@[instance]
def module.dual.add_comm_monoid (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [semimodule R M] :
def module.dual (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [semimodule 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.semimodule (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [semimodule R M] :
@[instance]
def module.dual.add_comm_group {S : Type u_1} [comm_ring S] {N : Type u_2} [add_comm_group N] [module S N] :
Equations
@[instance]
def module.dual.inhabited (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [semimodule R M] :
Equations
@[instance]
def module.dual.has_coe_to_fun (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [semimodule R M] :
Equations
def module.dual.eval (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [semimodule 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_semiring R] [add_comm_monoid M] [semimodule R M] (v : M) (a : module.dual R M) :
def module.dual.transpose {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [semimodule R M] {M' : Type u_3} [add_comm_monoid M'] [semimodule 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_semiring R] [add_comm_monoid M] [semimodule R M] {M' : Type u_3} [add_comm_monoid M'] [semimodule 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_semiring R] [add_comm_monoid M] [semimodule R M] {M' : Type u_3} [add_comm_monoid M'] [semimodule R M'] {M'' : Type u_4} [add_comm_monoid M''] [semimodule 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) (h : is_basis K B) :

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) (h : is_basis K B) (v : V) :

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

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} (h : is_basis K B) (i : ι) :

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) (a : (is_basis.to_dual B h) 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) :
ι → 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] [finite_dimensional K V] :
def vector_space.eval_equiv (K : Type u) (V : Type v) [field K] [add_comm_group V] [vector_space K V] [finite_dimensional 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] (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

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] (e : ι → V) (l : ι →₀ 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} (h : dual_pair 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 ε) :
def submodule.dual_restrict {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (W : submodule R M) :

The dual_restrict of a submodule W of M is the linear map from the dual of M to the dual of W such that the domain of each linear map is restricted to W.

Equations
@[simp]
theorem submodule.dual_restrict_apply {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (W : submodule R M) (φ : module.dual R M) (x : W) :
def submodule.dual_annihilator {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (W : submodule R M) :

The dual_annihilator of a submodule W is the set of linear maps φ such that φ w = 0 for all w ∈ W.

Equations
@[simp]
theorem submodule.mem_dual_annihilator {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {W : submodule R M} (φ : module.dual R M) :
φ W.dual_annihilator ∀ (w : M), w Wφ w = 0
def submodule.dual_annihilator_comap {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (Φ : submodule R (module.dual R M)) :

The pullback of a submodule in the dual space along the evaluation map.

Equations
theorem submodule.mem_dual_annihilator_comap_iff {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {Φ : submodule R (module.dual R M)} (x : M) :
x Φ.dual_annihilator_comap ∀ (φ : module.dual R M), φ Φφ x = 0
def subspace.dual_lift {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] (W : subspace K V) :

Given a subspace W of V and an element of its dual φ, dual_lift W φ is the natural extension of φ to an element of the dual of V. That is, dual_lift W φ sends w ∈ W to φ x and x in the complement of W to 0.

Equations
@[simp]
theorem subspace.dual_lift_of_subtype {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {W : subspace K V} {φ : module.dual K W} (w : W) :
((W.dual_lift) φ) w = φ w
theorem subspace.dual_lift_of_mem {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {W : subspace K V} {φ : module.dual K W} {w : V} (hw : w W) :
((W.dual_lift) φ) w = φ w, hw⟩
@[simp]
theorem subspace.dual_restrict_comp_dual_lift {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] (W : subspace K V) :
theorem subspace.dual_lift_injective {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {W : subspace K V} :

The quotient by the dual_annihilator of a subspace is isomorphic to the dual of that subspace.

Equations
def subspace.dual_equiv_dual {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] (W : subspace K V) :

The natural isomorphism forom the dual of a subspace W to W.dual_lift.range.

Equations
@[simp]
theorem subspace.dual_equiv_dual_apply {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {W : subspace K V} (φ : module.dual K W) :
@[instance]

The quotient by a subspace is isomorphic to its dual annihilator.

Equations
def linear_map.dual_map {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] (f : M₁ →ₗ[R] M₂) :

Given a linear map f : M₁ →ₗ[R] M₂, f.dual_map is the linear map between the dual of M₂ and M₁ such that it maps the functional φ to φ ∘ f.

Equations
@[simp]
theorem linear_map.dual_map_apply {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] (f : M₁ →ₗ[R] M₂) (g : module.dual R M₂) (x : M₁) :
((f.dual_map) g) x = g (f x)
@[simp]
theorem linear_map.dual_map_id {R : Type u_1} [comm_ring R] {M₁ : Type u_2} [add_comm_group M₁] [module R M₁] :
theorem linear_map.dual_map_comp_dual_map {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] {M₃ : Type u_4} [add_comm_group M₃] [module R M₃] (f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
def linear_equiv.dual_map {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] (f : M₁ ≃ₗ[R] M₂) :

The linear_equiv version of linear_map.dual_map.

Equations
@[simp]
theorem linear_equiv.dual_map_apply {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] (f : M₁ ≃ₗ[R] M₂) (g : module.dual R M₂) (x : M₁) :
((f.dual_map) g) x = g (f x)
@[simp]
theorem linear_equiv.dual_map_refl {R : Type u_1} [comm_ring R] {M₁ : Type u_2} [add_comm_group M₁] [module R M₁] :
@[simp]
theorem linear_equiv.dual_map_symm {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] {f : M₁ ≃ₗ[R] M₂} :
theorem linear_equiv.dual_map_trans {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] {M₃ : Type u_4} [add_comm_group M₃] [module R M₃] (f : M₁ ≃ₗ[R] M₂) (g : M₂ ≃ₗ[R] M₃) :
theorem linear_map.ker_dual_map_eq_dual_annihilator_range {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] (f : M₁ →ₗ[R] M₂) :
theorem linear_map.range_dual_map_le_dual_annihilator_ker {R : Type u_1} [comm_ring R] {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] (f : M₁ →ₗ[R] M₂) :
@[simp]
theorem linear_map.findim_range_dual_map_eq_findim_range {K : Type u_4} [field K] {V₁ : Type u_5} {V₂ : Type u_6} [add_comm_group V₁] [vector_space K V₁] [add_comm_group V₂] [vector_space K V₂] [finite_dimensional K V₂] (f : V₁ →ₗ[K] V₂) :
theorem linear_map.range_dual_map_eq_dual_annihilator_ker {K : Type u_4} [field K] {V₁ : Type u_5} {V₂ : Type u_6} [add_comm_group V₁] [vector_space K V₁] [add_comm_group V₂] [vector_space K V₂] [finite_dimensional K V₂] [finite_dimensional K V₁] (f : V₁ →ₗ[K] V₂) :