mathlib3 documentation

linear_algebra.dual

Dual vector spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The dual space of an $R$-module $M$ is the $R$-module of $R$-linear maps $M \to R$.

Main definitions #

Main results #

TODO #

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

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

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

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') :
@[simp]
theorem module.dual_prod_dual_equiv_dual_symm_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'] (f : M × M' →ₗ[R] R) :
def module.dual_prod_dual_equiv_dual (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'] :

Taking duals distributes over products.

Equations
@[simp]
theorem module.dual_prod_dual_equiv_dual_apply_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'] (f : (M →ₗ[R] R) × (M' →ₗ[R] R)) (ᾰ : M × M') :
((module.dual_prod_dual_equiv_dual R M M') f) = (f.fst) ᾰ.fst + (f.snd) ᾰ.snd
@[simp]
theorem module.dual_prod_dual_equiv_dual_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'] (φ : module.dual R M) (ψ : module.dual R M') :
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₂) :

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
theorem linear_map.dual_map_def {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.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₂) :
@[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₁) :
((f.dual_map) g) x = g (f x)
@[simp]
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₃) :
theorem linear_map.dual_map_injective_of_surjective {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₂} (hf : function.surjective f) :

If a linear map is surjective, then its dual is injective.

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

The linear_equiv version of linear_map.dual_map.

Equations
@[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₁) :
((f.dual_map) g) x = g (f x)
@[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₁] :
@[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₃) :
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) :

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
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
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) [finite ι] :
@[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) :
finset.univ.sum (λ (x : ι), f (b x) b.coord x) = f
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) [finite ι] :

A vector space is linearly equivalent to its dual space.

Equations
@[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) [finite ι] (m : M) :
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) [finite ι] :
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) [finite ι] (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) [finite ι] (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) [finite ι] (l : module.dual R M) (i : ι) :
((b.dual_basis.repr) l) i = l (b 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) [finite ι] (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) [finite ι] :
@[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) [finite ι] :
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.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} [finite ι] (b : basis ι 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} [finite ι] (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} [finite ι] (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] :
@[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] :
@[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] [finite ι] (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_rank_eq {K : Type u_3} {V : Type u_4} {ι : Type u_5} [comm_ring K] [add_comm_group V] [module K V] [finite ι] (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.eval_apply_eq_zero_iff (K : Type u_1) {V : Type u_2} [field K] [add_comm_group V] [module K V] (v : V) :
(module.dual.eval K V) v = 0 v = 0
theorem module.forall_dual_apply_eq_zero_iff (K : Type u_1) {V : Type u_2} [field K] [add_comm_group V] [module K V] (v : V) :
( (φ : module.dual K V), φ v = 0) v = 0
theorem module.dual_rank_eq {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] [finite_dimensional 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] :

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

Equations
noncomputable def module.map_eval_equiv (K : Type u_1) (V : Type u_2) [field K] [add_comm_group V] [module K V] [finite_dimensional K V] :

The isomorphism module.eval_equiv induces an order isomorphism on subspaces.

Equations
@[simp]

Try using set.to_finite to dispatch a set.finite goal.

@[nolint]
structure module.dual_bases {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) :
Prop
  • eval : (i j : ι), (ε i) (e j) = ite (i = j) 1 0
  • total : {m : M}, ( (i : ι), (ε i) m = 0) m = 0
  • finite : ( (m : M), {i : ι | (ε i) m 0}.finite) . "use_finite_instance"

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

noncomputable def module.dual_bases.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 : module.dual_bases e ε) (m : M) :
ι →₀ R

The coefficients of v on the basis e

Equations
@[simp]
theorem module.dual_bases.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 : module.dual_bases e ε) (m : M) (i : ι) :
(h.coeffs m) i = (ε i) m
def module.dual_bases.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 module.dual_bases.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 module.dual_bases.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 : module.dual_bases e ε) (l : ι →₀ R) (i : ι) :
(ε i) (module.dual_bases.lc e l) = l i
@[simp]
theorem module.dual_bases.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 : module.dual_bases e ε) (l : ι →₀ R) :
@[simp]
theorem module.dual_bases.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 : module.dual_bases e ε) (m : M) :

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

noncomputable def module.dual_bases.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 : module.dual_bases e ε) :
basis ι R M

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

Equations
@[simp]
theorem module.dual_bases.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 : module.dual_bases e ε) (m : M) :
(h.basis.repr) m = h.coeffs m
@[simp]
theorem module.dual_bases.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 : module.dual_bases e ε) (l : ι →₀ R) :
@[simp]
theorem module.dual_bases.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 : module.dual_bases e ε) :
(h.basis) = e
theorem module.dual_bases.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 : module.dual_bases e ε) {H : set ι} {x : M} (hmem : x submodule.span R (e '' H)) (i : ι) :
(ε i) x 0 i H
theorem module.dual_bases.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 : module.dual_bases e ε) [fintype ι] :

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

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) :
φ W.dual_annihilator (w : M), w W φ w = 0

That $\operatorname{ker}(\iota^* : V^* \to W^*) = \operatorname{ann}(W)$. This is the definition of the dual annihilator of the submodule $W$.

def submodule.dual_coannihilator {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (Φ : submodule R (module.dual R M)) :

The dual_annihilator of a submodule of the dual space pulled back along the evaluation map module.dual.eval.

Equations
theorem submodule.mem_dual_coannihilator {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_coannihilator (φ : module.dual R M), φ Φ φ x = 0
theorem submodule.dual_annihilator_supr_eq {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {ι : Type u_1} (U : ι submodule R M) :
( (i : ι), U i).dual_annihilator = (i : ι), (U i).dual_annihilator
theorem submodule.dual_coannihilator_supr_eq {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {ι : Type u_1} (U : ι submodule R (module.dual R M)) :
( (i : ι), U i).dual_coannihilator = (i : ι), (U i).dual_coannihilator
theorem submodule.supr_dual_annihilator_le_infi {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {ι : Type u_1} (U : ι submodule R M) :
( (i : ι), (U i).dual_annihilator) ( (i : ι), U i).dual_annihilator

See also subspace.dual_annihilator_infi_eq for vector subspaces when ι is finite.

theorem subspace.forall_mem_dual_annihilator_apply_eq_zero_iff {K : Type u} {V : Type v} [field K] [add_comm_group V] [module K V] (W : subspace K V) (v : V) :
noncomputable 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 an arbitrary extension of φ to an element of the dual of V. That is, dual_lift W φ sends w ∈ W to φ x and x in a chosen 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⟩

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

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

The natural isomorphism from 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) :
@[protected, instance]
def submodule.dual_copairing {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (W : submodule R M) :

Given a submodule, corestrict to the pairing on M ⧸ W by simultaneously restricting to W.dual_annihilator.

See subspace.dual_copairing_nondegenerate.

Equations
@[simp]
theorem submodule.dual_copairing_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {W : submodule R M} (φ : (W.dual_annihilator)) (x : M) :

Given a submodule, restrict to the pairing on W by simultaneously corestricting to module.dual R M ⧸ W.dual_annihilator. This is submodule.dual_restrict factored through the quotient by its kernel (which is W.dual_annihilator by definition).

See subspace.dual_pairing_nondegenerate.

Equations
@[simp]
theorem submodule.dual_pairing_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {W : submodule R M} (φ : module.dual R M) (x : W) :

That $\operatorname{im}(q^* : (V/W)^* \to V^*) = \operatorname{ann}(W)$.

Equivalence $(M/W)^* \approx \operatorname{ann}(W)$. That is, there is a one-to-one correspondence between the dual of M ⧸ W and those elements of the dual of M that vanish on W.

The inverse of this is submodule.dual_copairing.

Equations
@[simp]
theorem linear_map.dual_pairing_nondegenerate {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [module K V₁] :
theorem linear_map.dual_map_surjective_of_injective {K : Type u_1} [field K] {V₁ : Type u_2} {V₂ : Type u_3} [add_comm_group V₁] [module K V₁] [add_comm_group V₂] [module K V₂] {f : V₁ →ₗ[K] V₂} (hf : function.injective f) :
theorem linear_map.range_dual_map_eq_dual_annihilator_ker {K : Type u_1} [field K] {V₁ : Type u_2} {V₂ : Type u_3} [add_comm_group V₁] [module K V₁] [add_comm_group V₂] [module K V₂] (f : V₁ →ₗ[K] V₂) :
@[simp]
theorem linear_map.dual_map_surjective_iff {K : Type u_1} [field K] {V₁ : Type u_2} {V₂ : Type u_3} [add_comm_group V₁] [module K V₁] [add_comm_group V₂] [module K V₂] {f : V₁ →ₗ[K] V₂} :

For vector spaces, f.dual_map is surjective if and only if f is injective

theorem subspace.dual_pairing_nondegenerate {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [module K V₁] (W : subspace K V₁) :
theorem subspace.dual_copairing_nondegenerate {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [module K V₁] (W : subspace K V₁) :
theorem subspace.dual_annihilator_infi_eq {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [module K V₁] {ι : Type u_3} [finite ι] (W : ι subspace K V₁) :
theorem subspace.is_compl_dual_annihilator {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [module K V₁] {W W' : subspace K V₁} (h : is_compl W W') :

For vector spaces, dual annihilators carry direct sum decompositions to direct sum decompositions.

noncomputable def subspace.dual_quot_distrib {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [module K V₁] [finite_dimensional K V₁] (W : subspace K V₁) :

For finite-dimensional vector spaces, one can distribute duals over quotients by identifying W.dual_lift.range with W. Note that this depends on a choice of splitting of V₁.

Equations
@[simp]
theorem linear_map.dual_map_injective_iff {K : Type u_1} [field K] {V₁ : Type u_2} {V₂ : Type u_3} [add_comm_group V₁] [module K V₁] [add_comm_group V₂] [module K V₂] [finite_dimensional K V₂] {f : V₁ →ₗ[K] V₂} :

f.dual_map is injective if and only if f is surjective

@[simp]
theorem linear_map.dual_map_bijective_iff {K : Type u_1} [field K] {V₁ : Type u_2} {V₂ : Type u_3} [add_comm_group V₁] [module K V₁] [add_comm_group V₂] [module K V₂] [finite_dimensional K V₂] {f : V₁ →ₗ[K] V₂} :

f.dual_map is bijective if and only if f is

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

An inverse to dual_tensor_dual_map given bases.

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

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) :
@[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)) :
((tensor_product.dual_distrib_equiv_of_basis b c).symm) = finset.univ.sum (λ (x : ι), finset.univ.sum (λ (x_1 : κ), (b x ⊗ₜ[R] c x_1) b.coord x ⊗ₜ[R] c.coord x_1))
@[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] :

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.

Equations