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

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

Equations
@[simp]
theorem module.dual.eval_apply (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [module 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] [module R M] {M' : Type u_3} [add_comm_monoid 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_semiring R] [add_comm_monoid M] [module R M] {M' : Type u_3} [add_comm_monoid 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_semiring R] [add_comm_monoid M] [module R M] {M' : Type u_3} [add_comm_monoid M'] [module R M'] {M'' : Type u_4} [add_comm_monoid M''] [module R M''] (u : M' →ₗ[R] M'') (v : M →ₗ[R] M') :
def basis.to_dual {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] [decidable_eq ι] (b : basis ι R M) :

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 basis.to_dual_apply {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] [decidable_eq ι] (b : basis ι R M) (i j : ι) :
((b.to_dual) (b i)) (b j) = ite (i = j) 1 0
@[simp]
theorem basis.to_dual_total_left {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] [decidable_eq ι] (b : basis ι R M) (f : ι →₀ R) (i : ι) :
((b.to_dual) ((finsupp.total ι M R b) f)) (b i) = f i
@[simp]
theorem basis.to_dual_total_right {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] [decidable_eq ι] (b : basis ι R M) (f : ι →₀ R) (i : ι) :
((b.to_dual) (b i)) ((finsupp.total ι M R b) f) = f i
theorem basis.to_dual_apply_left {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] [decidable_eq ι] (b : basis ι R M) (m : M) (i : ι) :
((b.to_dual) m) (b i) = ((b.repr) m) i
theorem basis.to_dual_apply_right {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] [decidable_eq ι] (b : basis ι R M) (i : ι) (m : M) :
((b.to_dual) (b i)) m = ((b.repr) m) i
theorem basis.coe_to_dual_self {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] [decidable_eq ι] (b : basis ι R M) (i : ι) :
(b.to_dual) (b i) = b.coord i
def basis.to_dual_flip {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] [decidable_eq ι] (b : basis ι R M) (m : M) :

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

Equations
theorem basis.to_dual_flip_apply {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] [decidable_eq ι] (b : basis ι R M) (m₁ m₂ : M) :
(b.to_dual_flip m₁) m₂ = ((b.to_dual) m₂) m₁
theorem basis.to_dual_eq_repr {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] [decidable_eq ι] (b : basis ι R M) (m : M) (i : ι) :
((b.to_dual) m) (b i) = ((b.repr) m) i
theorem basis.to_dual_eq_equiv_fun {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] [decidable_eq ι] (b : basis ι R M) [fintype ι] (m : M) (i : ι) :
((b.to_dual) m) (b i) = (b.equiv_fun) m i
theorem basis.to_dual_inj {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] [decidable_eq ι] (b : basis ι R M) (m : M) (a : (b.to_dual) m = 0) :
m = 0
theorem basis.to_dual_ker {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] [decidable_eq ι] (b : basis ι R M) :
theorem basis.to_dual_range {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_semiring R] [add_comm_monoid M] [module R M] [decidable_eq ι] (b : basis ι R M) [fin : fintype ι] :
def basis.to_dual_equiv {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [decidable_eq ι] (b : basis ι R M) [fintype ι] :

A vector space is linearly equivalent to its dual space.

Equations
@[simp]
theorem basis.to_dual_equiv_symm_apply {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [decidable_eq ι] (b : basis ι R M) [fintype ι] (ᾰ : module.dual R M) :
@[simp]
theorem basis.to_dual_equiv_apply {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [decidable_eq ι] (b : basis ι R M) [fintype ι] (ᾰ : M) :
(b.to_dual_equiv) ᾰ = (b.to_dual) ᾰ
def basis.dual_basis {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [decidable_eq ι] (b : basis ι R M) [fintype ι] :
basis ι R (module.dual R M)

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

Equations
theorem basis.dual_basis_apply_self {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [decidable_eq ι] (b : basis ι R M) [fintype ι] (i j : ι) :
((b.dual_basis) i) (b j) = ite (j = i) 1 0
theorem basis.total_dual_basis {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [decidable_eq ι] (b : basis ι R M) [fintype ι] (f : ι →₀ R) (i : ι) :
((finsupp.total ι (module.dual R M) R (b.dual_basis)) f) (b i) = f i
theorem basis.dual_basis_repr {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [decidable_eq ι] (b : basis ι R M) [fintype ι] (l : module.dual R M) (i : ι) :
((b.dual_basis.repr) l) i = l (b i)
theorem basis.dual_basis_equiv_fun {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [decidable_eq ι] (b : basis ι R M) [fintype ι] (l : module.dual R M) (i : ι) :
theorem basis.dual_basis_apply {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [decidable_eq ι] (b : basis ι R M) [fintype ι] (i : ι) (m : M) :
((b.dual_basis) i) m = ((b.repr) m) i
@[simp]
theorem basis.coe_dual_basis {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [decidable_eq ι] (b : basis ι R M) [fintype ι] :
@[simp]
theorem basis.to_dual_to_dual {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [decidable_eq ι] (b : basis ι R M) [fintype ι] :
theorem basis.eval_ker {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {ι : Type u_3} (b : basis ι R M) :
theorem basis.eval_range {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {ι : Type u_3} [fintype ι] (b : basis ι R M) :
def basis.eval_equiv {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {ι : Type u_3} [fintype ι] (b : basis ι R M) :

A module with a basis is linearly equivalent to the dual of its dual space.

Equations
@[simp]
theorem basis.eval_equiv_to_linear_map {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {ι : Type u_3} [fintype ι] (b : basis ι R M) :
@[simp]
theorem basis.total_coord {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [fintype ι] (b : basis ι R M) (f : ι →₀ R) (i : ι) :
((finsupp.total ι (module.dual R M) R b.coord) f) (b i) = f i

simp normal form version of total_dual_basis

theorem basis.dual_dim_eq {K : Type u_3} {V : Type u_4} {ι : Type u_5} [field K] [add_comm_group V] [module K V] [fintype ι] (b : basis ι K V) :
theorem module.eval_ker {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] :
theorem module.dual_dim_eq {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] :
theorem module.erange_coe {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] :
def module.eval_equiv (K : Type u_1) (V : Type u_2) [field K] [add_comm_group V] [module K V] [finite_dimensional K V] :

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

Equations
@[simp]
theorem module.eval_equiv_to_linear_map {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] :
@[nolint]
structure dual_pair {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [add_comm_group M] [module R M] [decidable_eq ι] (e : ι → M) (ε : ι → module.dual R M) :
Type (max u_2 u_3)
  • eval : ∀ (i j : ι), (ε i) (e j) = ite (i = j) 1 0
  • total : ∀ {m : M}, (∀ (i : ι), (ε i) m = 0)m = 0
  • finite : Π (m : M), fintype {i : ι | (ε i) m 0}

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

def dual_pair.coeffs {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} {ε : ι → module.dual R M} [decidable_eq ι] (h : dual_pair e ε) (m : M) :
ι →₀ R

The coefficients of v on the basis e

Equations
@[simp]
theorem dual_pair.coeffs_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} {ε : ι → module.dual R M} [decidable_eq ι] (h : dual_pair e ε) (m : M) (i : ι) :
(h.coeffs m) i = (ε i) m
def dual_pair.lc {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {ι : Type u_3} (e : ι → M) (l : ι →₀ R) :
M

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

Equations
theorem dual_pair.lc_def {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [add_comm_group M] [module R M] (e : ι → M) (l : ι →₀ R) :
theorem dual_pair.dual_lc {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} {ε : ι → module.dual R M} [decidable_eq ι] (h : dual_pair e ε) (l : ι →₀ R) (i : ι) :
(ε i) (dual_pair.lc e l) = l i
@[simp]
theorem dual_pair.coeffs_lc {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} {ε : ι → module.dual R M} [decidable_eq ι] (h : dual_pair e ε) (l : ι →₀ R) :
@[simp]
theorem dual_pair.lc_coeffs {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} {ε : ι → module.dual R M} [decidable_eq ι] (h : dual_pair e ε) (m : M) :

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

@[simp]
theorem dual_pair.basis_repr_symm_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} {ε : ι → module.dual R M} [decidable_eq ι] (h : dual_pair e ε) (l : ι →₀ R) :
@[simp]
theorem dual_pair.basis_repr_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} {ε : ι → module.dual R M} [decidable_eq ι] (h : dual_pair e ε) (m : M) :
(h.basis.repr) m = h.coeffs m
def dual_pair.basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} {ε : ι → module.dual R M} [decidable_eq ι] (h : dual_pair e ε) :
basis ι R M

(h : dual_pair e ε).basis shows the family of vectors e forms a basis.

Equations
@[simp]
theorem dual_pair.coe_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} {ε : ι → module.dual R M} [decidable_eq ι] (h : dual_pair e ε) :
(h.basis) = e
theorem dual_pair.mem_of_mem_span {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} {ε : ι → module.dual R M} [decidable_eq ι] (h : dual_pair e ε) {H : set ι} {x : M} (hmem : x submodule.span R (e '' H)) (i : ι) :
(ε i) x 0i H
theorem dual_pair.coe_dual_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} {ε : ι → module.dual R M} [decidable_eq ι] (h : dual_pair e ε) [fintype ι] :
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] [module 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] [module 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] [module 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] [module K V] (W : subspace K V) :
theorem subspace.dual_lift_injective {K : Type u} {V : Type v} [field K] [add_comm_group V] [module 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] [module 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] [module K V] {W : subspace K V} (φ : module.dual K W) :
@[instance]
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.finrank_range_dual_map_eq_finrank_range {K : Type u_4} [field K] {V₁ : Type u_5} {V₂ : Type u_6} [add_comm_group V₁] [module K V₁] [add_comm_group V₂] [module 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₁] [module K V₁] [add_comm_group V₂] [module K V₂] [finite_dimensional K V₂] [finite_dimensional K V₁] (f : V₁ →ₗ[K] V₂) :