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 an
R-moduleM,basis.to_dualproduces a map fromMtodual R M. - Given families of vectors
eandε,dual_pair e εstates that these families have the characteristic properties of a basis and a dual. dual_annihilator Wis the submodule ofdual R Mwhere every element annihilatesW.
Main results #
to_dual_equiv: the linear equivalence between the dual module and primal module, given a finite basis.dual_pair.basisanddual_pair.eq_dual: ifeandεform a dual pair,eis a basis andεis its dual basis.quot_equiv_annihilator: the quotient by a subspace is isomorphic to its dual annihilator.
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.
@[protected, instance]
def
module.dual.module
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
module R (module.dual R M)
@[protected, 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] :
add_comm_monoid (module.dual 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
- module.dual R M = (M →ₗ[R] R)
@[protected, 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] :
add_comm_group (module.dual S N)
@[protected, instance]
def
module.linear_map_class
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
linear_map_class (module.dual R M) R M R
Equations
def
module.dual_pairing
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
module.dual R M →ₗ[R] M →ₗ[R] R
The canonical pairing of a vector space and its algebraic dual.
Equations
@[simp]
theorem
module.dual_pairing_apply
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M]
(v : module.dual R M)
(x : M) :
⇑(⇑(module.dual_pairing R M) v) x = ⇑v x
@[protected, instance]
def
module.dual.inhabited
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
inhabited (module.dual R M)
Equations
@[protected, 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] :
has_coe_to_fun (module.dual R M) (λ (_x : module.dual R M), M → R)
Equations
def
module.dual.eval
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid 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 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) :
⇑(⇑(module.dual.eval R M) v) a = ⇑a v
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'] :
(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_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') :
⇑(⇑module.dual.transpose u) l = linear_map.comp l u
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') :
⇑module.dual.transpose (u.comp v) = (⇑module.dual.transpose v).comp (⇑module.dual.transpose u)
noncomputable
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) :
M →ₗ[R] module.dual 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.
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 : ι) :
@[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 : ι) :
@[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 : ι) :
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 : ι) :
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) :
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 : ι) :
noncomputable
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
- b.to_dual_flip m = ⇑(b.to_dual.flip) m
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) :
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 : ι) :
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 : ι) :
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 ι] :
@[simp]
theorem
basis.sum_dual_apply_smul_coord
{R : Type u_1}
{M : Type u_2}
{ι : Type u_5}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
[fintype ι]
(b : basis ι R M)
(f : module.dual R M) :
noncomputable
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 ι] :
M ≃ₗ[R] module.dual R M
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) :
⇑(b.to_dual_equiv.symm) ᾰ = ⇑((linear_equiv.of_injective b.to_dual _).symm) (⇑((linear_equiv.of_top (linear_map.range b.to_dual) _).symm) ᾰ)
@[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) ᾰ
noncomputable
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
- b.dual_basis = b.map b.to_dual_equiv
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 : ι) :
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 : ι) :
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) :
@[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 ι] :
⇑(b.dual_basis) = b.coord
@[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 ι] :
b.dual_basis.to_dual.comp b.to_dual = module.dual.eval R M
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) :
linear_map.ker (module.dual.eval 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) :
linear_map.range (module.dual.eval R M) = ⊤
noncomputable
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) :
M ≃ₗ[R] module.dual R (module.dual R M)
A module with a basis is linearly equivalent to the dual of its dual space.
Equations
- b.eval_equiv = linear_equiv.of_bijective (module.dual.eval R M) _ _
@[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) :
@[protected, instance]
def
basis.dual_free
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
[module.finite R M]
[module.free R M]
[nontrivial R] :
module.free R (module.dual R M)
@[protected, instance]
def
basis.dual_finite
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
[module.finite R M]
[module.free R M]
[nontrivial R] :
module.finite R (module.dual 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) :
(module.rank K V).lift = module.rank K (module.dual K V)
theorem
module.eval_ker
{K : Type u_1}
{V : Type u_2}
[field K]
[add_comm_group V]
[module K V] :
linear_map.ker (module.dual.eval 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] :
(module.rank K V).lift = module.rank K (module.dual 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] :
linear_map.range (module.dual.eval K V) = ⊤
noncomputable
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] :
V ≃ₗ[K] module.dual K (module.dual K V)
A vector space is linearly equivalent to the dual of its dual space.
Equations
- module.eval_equiv K V = linear_equiv.of_bijective (module.dual.eval K V) _ _
@[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] :
(module.eval_equiv K V).to_linear_map = module.dual.eval K V
@[nolint]
structure
dual_pair
{R : Type u_1}
{M : Type u_2}
{ι : Type u_3}
[comm_semiring R]
[add_comm_monoid 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
Instances for dual_pair
- dual_pair.has_sizeof_inst
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
@[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 : ι) :
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
- dual_pair.lc e l = l.sum (λ (i : ι) (a : R), a • e i)
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) :
dual_pair.lc e l = ⇑(finsupp.total ι M R e) l
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) :
h.coeffs (dual_pair.lc e l) = l
@[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) :
dual_pair.lc e (h.coeffs 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) :
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.
@[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 ε) :
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 : ι) :
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 ι] :
⇑(h.basis.dual_basis) = ε
def
submodule.dual_restrict
{R : Type u}
{M : Type v}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
(W : submodule R M) :
module.dual R M →ₗ[R] module.dual R ↥W
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_semiring R]
[add_comm_monoid 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_semiring R]
[add_comm_monoid M]
[module R M]
(W : submodule R M) :
submodule R (module.dual 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_semiring R]
[add_comm_monoid M]
[module R M]
{W : submodule R M}
(φ : module.dual R M) :
theorem
submodule.dual_restrict_ker_eq_dual_annihilator
{R : Type u}
{M : Type v}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
(W : submodule R M) :
theorem
submodule.dual_annihilator_sup_eq_inf_dual_annihilator
{R : Type u}
{M : Type v}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
(U V : submodule R M) :
(U ⊔ V).dual_annihilator = U.dual_annihilator ⊓ V.dual_annihilator
def
submodule.dual_annihilator_comap
{R : Type u}
{M : Type v}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
(Φ : submodule R (module.dual R M)) :
submodule 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_semiring R]
[add_comm_monoid M]
[module R M]
{Φ : submodule R (module.dual R M)}
(x : M) :
x ∈ Φ.dual_annihilator_comap ↔ ∀ (φ : module.dual R M), φ ∈ Φ → ⇑φ x = 0
noncomputable
def
subspace.dual_lift
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(W : subspace K V) :
module.dual K ↥W →ₗ[K] module.dual 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
- W.dual_lift = let h : {x // is_compl W x} := classical.indefinite_description (λ (x : submodule K V), is_compl W x) _ in (linear_map.of_is_compl_prod _).comp (linear_map.inl K (module.dual K ↥W) (↥(h.val) →ₗ[K] K))
@[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) :
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) :
@[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) :
(submodule.dual_restrict W).comp W.dual_lift = 1
theorem
subspace.dual_restrict_left_inverse
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(W : subspace K V) :
theorem
subspace.dual_lift_right_inverse
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(W : subspace K V) :
theorem
subspace.dual_restrict_surjective
{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} :
noncomputable
def
subspace.quot_annihilator_equiv
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(W : subspace K V) :
(module.dual K V ⧸ submodule.dual_annihilator W) ≃ₗ[K] module.dual K ↥W
The quotient by the dual_annihilator of a subspace is isomorphic to the
dual of that subspace.
noncomputable
def
subspace.dual_equiv_dual
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(W : subspace K V) :
module.dual K ↥W ≃ₗ[K] ↥(linear_map.range W.dual_lift)
The natural isomorphism forom the dual of a subspace W to W.dual_lift.range.
theorem
subspace.dual_equiv_dual_def
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(W : subspace K V) :
@[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) :
@[protected, instance]
def
subspace.module.dual.finite_dimensional
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[H : finite_dimensional K V] :
finite_dimensional K (module.dual K V)
@[simp]
theorem
subspace.dual_finrank_eq
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
noncomputable
def
subspace.quot_dual_equiv_annihilator
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(W : subspace K V) :
(module.dual K V ⧸ linear_map.range W.dual_lift) ≃ₗ[K] ↥(submodule.dual_annihilator W)
The quotient by the dual is isomorphic to its dual annihilator.
noncomputable
def
subspace.quot_equiv_annihilator
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(W : subspace K V) :
(V ⧸ W) ≃ₗ[K] ↥(submodule.dual_annihilator W)
The quotient by a subspace is isomorphic to its dual annihilator.
@[simp]
theorem
subspace.finrank_dual_annihilator_comap_eq
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{Φ : subspace K (module.dual K V)} :
theorem
subspace.finrank_add_finrank_dual_annihilator_comap_eq
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(W : subspace K (module.dual K V)) :
def
linear_map.dual_map
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
(f : M₁ →ₗ[R] M₂) :
module.dual R M₂ →ₗ[R] module.dual 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
- f.dual_map = linear_map.lcomp R R f
@[simp]
theorem
linear_map.dual_map_apply
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
(f : M₁ →ₗ[R] M₂)
(g : module.dual R M₂)
(x : M₁) :
@[simp]
theorem
linear_map.dual_map_id
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
[add_comm_monoid M₁]
[module R M₁] :
theorem
linear_map.dual_map_comp_dual_map
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid 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_semiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
(f : M₁ ≃ₗ[R] M₂) :
module.dual R M₂ ≃ₗ[R] module.dual R M₁
The linear_equiv version of linear_map.dual_map.
@[simp]
theorem
linear_equiv.dual_map_apply
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
(f : M₁ ≃ₗ[R] M₂)
(g : module.dual R M₂)
(x : M₁) :
@[simp]
theorem
linear_equiv.dual_map_refl
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
[add_comm_monoid M₁]
[module R M₁] :
(linear_equiv.refl R M₁).dual_map = linear_equiv.refl R (module.dual R M₁)
@[simp]
theorem
linear_equiv.dual_map_symm
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
{f : M₁ ≃ₗ[R] M₂} :
theorem
linear_equiv.dual_map_trans
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid 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_semiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
(f : M₁ →ₗ[R] M₂) :
theorem
linear_map.range_dual_map_le_dual_annihilator_ker
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid 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₂) :
theorem
linear_map.dual_pairing_nondegenerate
{K : Type u_4}
{V : Type u_5}
[field K]
[add_comm_group V]
[module K V] :
def
tensor_product.dual_distrib
(R : Type u_1)
(M : Type u_2)
(N : Type u_3)
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N] :
tensor_product R (module.dual R M) (module.dual R N) →ₗ[R] module.dual R (tensor_product R M N)
The canonical linear map from dual M ⊗ dual N to dual (M ⊗ N),
sending f ⊗ g to the composition of tensor_product.map f g with
the natural isomorphism R ⊗ R ≃ R.
Equations
- tensor_product.dual_distrib R M N = ↑(tensor_product.lid R R).comp_right.comp (tensor_product.hom_tensor_hom_map R M N R R)
@[simp]
theorem
tensor_product.dual_distrib_apply
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
(f : module.dual R M)
(g : module.dual R N)
(m : M)
(n : N) :
noncomputable
def
tensor_product.dual_distrib_inv_of_basis
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
[decidable_eq ι]
[decidable_eq κ]
[fintype ι]
[fintype κ]
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(b : basis ι R M)
(c : basis κ R N) :
module.dual R (tensor_product R M N) →ₗ[R] tensor_product R (module.dual R M) (module.dual R N)
An inverse to dual_tensor_dual_map given bases.
Equations
- tensor_product.dual_distrib_inv_of_basis b c = finset.univ.sum (λ (i : ι), finset.univ.sum (λ (j : κ), (⇑((linear_map.ring_lmap_equiv_self R ℕ (tensor_product R (module.dual R M) (module.dual R N))).symm) (⇑(b.dual_basis) i ⊗ₜ[R] ⇑(c.dual_basis) j)).comp ((⇑linear_map.applyₗ (⇑c j)).comp ((⇑linear_map.applyₗ (⇑b i)).comp (tensor_product.lcurry R M N R)))))
@[simp]
theorem
tensor_product.dual_distrib_inv_of_basis_apply
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
[decidable_eq ι]
[decidable_eq κ]
[fintype ι]
[fintype κ]
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(b : basis ι R M)
(c : basis κ R N)
(f : module.dual R (tensor_product R M N)) :
⇑(tensor_product.dual_distrib_inv_of_basis b c) f = finset.univ.sum (λ (i : ι), finset.univ.sum (λ (j : κ), ⇑f (⇑b i ⊗ₜ[R] ⇑c j) • ⇑(b.dual_basis) i ⊗ₜ[R] ⇑(c.dual_basis) j))
noncomputable
def
tensor_product.dual_distrib_equiv_of_basis
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
[decidable_eq ι]
[decidable_eq κ]
[fintype ι]
[fintype κ]
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(b : basis ι R M)
(c : basis κ R N) :
tensor_product R (module.dual R M) (module.dual R N) ≃ₗ[R] module.dual R (tensor_product R M N)
A linear equivalence between dual M ⊗ dual N and dual (M ⊗ N) given bases for M and N.
It sends f ⊗ g to the composition of tensor_product.map f g with the natural
isomorphism R ⊗ R ≃ R.
Equations
@[simp]
theorem
tensor_product.dual_distrib_equiv_of_basis_apply_apply
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
[decidable_eq ι]
[decidable_eq κ]
[fintype ι]
[fintype κ]
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(b : basis ι R M)
(c : basis κ R N)
(ᾰ : tensor_product R (module.dual R M) (module.dual R N))
(ᾰ_1 : tensor_product R M N) :
⇑(⇑(tensor_product.dual_distrib_equiv_of_basis b c) ᾰ) ᾰ_1 = ⇑(tensor_product.lid R R) (⇑(⇑(tensor_product.hom_tensor_hom_map R M N R R) ᾰ) ᾰ_1)
@[simp]
theorem
tensor_product.dual_distrib_equiv_of_basis_symm_apply
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
[decidable_eq ι]
[decidable_eq κ]
[fintype ι]
[fintype κ]
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(b : basis ι R M)
(c : basis κ R N)
(ᾰ : module.dual R (tensor_product R M N)) :
@[simp]
noncomputable
def
tensor_product.dual_distrib_equiv
(R : Type u_1)
(M : Type u_2)
(N : Type u_3)
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
[module.finite R M]
[module.finite R N]
[module.free R M]
[module.free R N]
[nontrivial R] :
tensor_product R (module.dual R M) (module.dual R N) ≃ₗ[R] module.dual R (tensor_product R M N)
A linear equivalence between dual M ⊗ dual N and dual (M ⊗ N) when M and N are finite free
modules. It sends f ⊗ g to the composition of tensor_product.map f g with the natural
isomorphism R ⊗ R ≃ R.