# mathlib3documentation

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 #

• Duals and transposes:
• module.dual R M defines the dual space of the R-module M, as M →ₗ[R] R.
• module.dual_pairing R M is the canonical pairing between dual R M and M.
• module.dual.eval R M : M →ₗ[R] dual R (dual R) is the canonical map to the double dual.
• module.dual.transpose is the linear map from M →ₗ[R] M' to dual R M' →ₗ[R] dual R M.
• linear_map.dual_map is module.dual.transpose of a given linear map, for dot notation.
• linear_equiv.dual_map is for the dual of an equivalence.
• Bases:
• basis.to_dual produces the map M →ₗ[R] dual R M associated to a basis for an R-module M.
• basis.to_dual_equiv is the equivalence M ≃ₗ[R] dual R M associated to a finite basis.
• basis.dual_basis is a basis for dual R M given a finite basis for M.
• module.dual_bases e ε is the proposition that the families e of vectors and ε of dual vectors have the characteristic properties of a basis and a dual.
• Submodules:
• submodule.dual_restrict W is the transpose dual R M →ₗ[R] dual R W of the inclusion map.
• submodule.dual_annihilator W is the kernel of W.dual_restrict. That is, it is the submodule of dual R M whose elements all annihilate W.
• submodule.dual_restrict_comap W' is the dual annihilator of W' : submodule R (dual R M), pulled back along module.dual.eval R M.
• submodule.dual_copairing W is the canonical pairing between W.dual_annihilator and M ⧸ W. It is nondegenerate for vector spaces (subspace.dual_copairing_nondegenerate).
• submodule.dual_pairing W is the canonical pairing between dual R M ⧸ W.dual_annihilator and W. It is nondegenerate for vector spaces (subspace.dual_pairing_nondegenerate).
• Vector spaces:
• subspace.dual_lift W is an arbitrary section (using choice) of submodule.dual_restrict W.

## Main results #

• Bases:
• module.dual_basis.basis and module.dual_basis.coe_basis: if e and ε form a dual pair, then e is a basis.
• module.dual_basis.coe_dual_basis: if e and ε form a dual pair, then ε is a basis.
• Annihilators:
• module.dual_annihilator_gc R M is the antitone Galois correspondence between submodule.dual_annihilator and submodule.dual_coannihilator.
• linear_map.ker_dual_map_eq_dual_annihilator_range says that f.dual_map.ker = f.range.dual_annihilator
• linear_map.range_dual_map_eq_dual_annihilator_ker_of_subtype_range_surjective says that f.dual_map.range = f.ker.dual_annihilator; this is specialized to vector spaces in linear_map.range_dual_map_eq_dual_annihilator_ker.
• submodule.dual_quot_equiv_dual_annihilator is the equivalence dual R (M ⧸ W) ≃ₗ[R] W.dual_annihilator
• Vector spaces:
• subspace.dual_annihilator_dual_coannihilator_eq says that the double dual annihilator, pulled back ground module.dual.eval, is the original submodule.
• subspace.dual_annihilator_gci says that module.dual_annihilator_gc R M is an antitone Galois coinsertion.
• subspace.quot_annihilator_equiv is the equivalence dual K V ⧸ W.dual_annihilator ≃ₗ[K] dual K W.
• linear_map.dual_pairing_nondegenerate says that module.dual_pairing is nondegenerate.
• subspace.is_compl_dual_annihilator says that the dual annihilator carries complementary subspaces to complementary subspaces.
• Finite-dimensional vector spaces:
• module.eval_equiv is the equivalence V ≃ₗ[K] dual K (dual K V)
• module.map_eval_equiv is the order isomorphism between subspaces of V and subspaces of dual K (dual K V).
• subspace.quot_dual_equiv_annihilator W is the equivalence (dual K V ⧸ W.dual_lift.range) ≃ₗ[K] W.dual_annihilator, where W.dual_lift.range is a copy of dual K W inside dual K V.
• subspace.quot_equiv_annihilator W is the equivalence (V ⧸ W) ≃ₗ[K] W.dual_annihilator
• subspace.dual_quot_distrib W is an equivalence dual K (V₁ ⧸ W) ≃ₗ[K] dual K V₁ ⧸ W.dual_lift.range from an arbitrary choice of splitting of V₁.

## 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) [ 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) [ 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) [ M] (v : M) (x : M) :
( M) v) x = v x
@[protected, instance]
def module.dual.inhabited (R : Type u_1) (M : Type u_2) [ M] :
Equations
@[protected, instance]
def module.dual.has_coe_to_fun (R : Type u_1) (M : Type u_2) [ M] :
(λ (_x : M), M R)
Equations
def module.dual.eval (R : Type u_1) (M : Type u_2) [ M] :
M →ₗ[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) [ M] (v : M) (a : M) :
( M) v) a = a v
def module.dual.transpose {R : Type u_1} {M : Type u_2} [ M] {M' : Type u_3} [add_comm_monoid M'] [ M'] :
(M →ₗ[R] M') →ₗ[R] M' →ₗ[R] M

The transposition of linear maps, as a linear map from M →ₗ[R] M' to dual R M' →ₗ[R] dual R M.

Equations
theorem module.dual.transpose_apply {R : Type u_1} {M : Type u_2} [ M] {M' : Type u_3} [add_comm_monoid M'] [ M'] (u : M →ₗ[R] M') (l : M') :
=
theorem module.dual.transpose_comp {R : Type u_1} {M : Type u_2} [ M] {M' : Type u_3} [add_comm_monoid M'] [ M'] {M'' : Type u_4} [add_comm_monoid M''] [ 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) [ M] (M' : Type u_3) [add_comm_monoid M'] [ M'] (f : M × M' →ₗ[R] R) :
M').symm) f = (f.comp M M'), f.comp M M'))
def module.dual_prod_dual_equiv_dual (R : Type u_1) (M : Type u_2) [ M] (M' : Type u_3) [add_comm_monoid M'] [ M'] :
M × M') ≃ₗ[R] (M × 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) [ M] (M' : Type u_3) [add_comm_monoid M'] [ M'] (f : (M →ₗ[R] R) × (M' →ₗ[R] R)) (ᾰ : M × 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) [ M] (M' : Type u_3) [add_comm_monoid M'] [ M'] (φ : M) (ψ : M') :
M') (φ, ψ) =
def linear_map.dual_map {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] (f : M₁ →ₗ[R] M₂) :
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} {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] (f : M₁ →ₗ[R] M₂) :
theorem linear_map.dual_map_apply' {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] (f : M₁ →ₗ[R] M₂) (g : M₂) :
(f.dual_map) g =
@[simp]
theorem linear_map.dual_map_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] (f : M₁ →ₗ[R] M₂) (g : M₂) (x : M₁) :
((f.dual_map) g) x = g (f x)
@[simp]
theorem linear_map.dual_map_id {R : Type u_1} {M₁ : Type u_2} [add_comm_monoid M₁] [ M₁] :
theorem linear_map.dual_map_comp_dual_map {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] {M₃ : Type u_4} [add_comm_group M₃] [ M₃] (f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
theorem linear_map.dual_map_injective_of_surjective {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ 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} {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] (f : M₁ ≃ₗ[R] M₂) :
M₂ ≃ₗ[R] M₁

The linear_equiv version of linear_map.dual_map.

Equations
@[simp]
theorem linear_equiv.dual_map_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] (f : M₁ ≃ₗ[R] M₂) (g : M₂) (x : M₁) :
((f.dual_map) g) x = g (f x)
@[simp]
theorem linear_equiv.dual_map_refl {R : Type u_1} {M₁ : Type u_2} [add_comm_monoid M₁] [ M₁] :
M₁).dual_map = M₁)
@[simp]
theorem linear_equiv.dual_map_symm {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] {f : M₁ ≃ₗ[R] M₂} :
theorem linear_equiv.dual_map_trans {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] {M₃ : Type u_4} [add_comm_group M₃] [ 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} [ M] [decidable_eq ι] (b : 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} [ M] [decidable_eq ι] (b : 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} [ M] [decidable_eq ι] (b : R M) (f : ι →₀ R) (i : ι) :
((b.to_dual) ( 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} [ M] [decidable_eq ι] (b : R M) (f : ι →₀ R) (i : ι) :
((b.to_dual) (b i)) ( M R b) f) = f i
theorem basis.to_dual_apply_left {R : Type u_1} {M : Type u_2} {ι : Type u_5} [ M] [decidable_eq ι] (b : 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} [ M] [decidable_eq ι] (b : 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} [ M] [decidable_eq ι] (b : 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} [ M] [decidable_eq ι] (b : 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} [ M] [decidable_eq ι] (b : 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} [ M] [decidable_eq ι] (b : 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} [ M] [decidable_eq ι] (b : 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} [ M] [decidable_eq ι] (b : 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} [ M] [decidable_eq ι] (b : R M) :
theorem basis.to_dual_range {R : Type u_1} {M : Type u_2} {ι : Type u_5} [ M] [decidable_eq ι] (b : R M) [finite ι] :
@[simp]
theorem basis.sum_dual_apply_smul_coord {R : Type u_1} {M : Type u_2} {ι : Type u_5} [ M] [fintype ι] (b : R M) (f : 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] [ M] [decidable_eq ι] (b : 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] [ M] [decidable_eq ι] (b : R M) [finite ι] (m : M) :
noncomputable def basis.dual_basis {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [ M] [decidable_eq ι] (b : R M) [finite ι] :
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] [ M] [decidable_eq ι] (b : 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] [ M] [decidable_eq ι] (b : R M) [finite ι] (f : ι →₀ R) (i : ι) :
( 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] [ M] [decidable_eq ι] (b : R M) [finite ι] (l : 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] [ M] [decidable_eq ι] (b : 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] [ M] [decidable_eq ι] (b : R M) [finite ι] :
@[simp]
theorem basis.to_dual_to_dual {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [ M] [decidable_eq ι] (b : R M) [finite ι] :
theorem basis.dual_basis_equiv_fun {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [ M] [decidable_eq ι] (b : R M) [fintype ι] (l : M) (i : ι) :
theorem basis.eval_ker {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {ι : Type u_3} (b : R M) :
theorem basis.eval_range {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {ι : Type u_3} [finite ι] (b : R M) :
noncomputable def basis.eval_equiv {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {ι : Type u_3} [finite ι] (b : R M) :
M ≃ₗ[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] [ M] {ι : Type u_3} [finite ι] (b : R M) :
@[protected, instance]
def basis.dual_free {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] [ M] [ M] [nontrivial R] :
M)
@[protected, instance]
def basis.dual_finite {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] [ M] [ M] [nontrivial R] :
M)
@[simp]
theorem basis.total_coord {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [ M] [finite ι] (b : R M) (f : ι →₀ R) (i : ι) :
( 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] [ V] [finite ι] (b : K V) :
V).lift = V)
theorem module.eval_ker (K : Type u_1) (V : Type u_2) [field K] [ V] :
theorem module.map_eval_injective (K : Type u_1) (V : Type u_2) [field K] [ V] :
theorem module.comap_eval_surjective (K : Type u_1) (V : Type u_2) [field K] [ V] :
theorem module.eval_apply_eq_zero_iff (K : Type u_1) {V : Type u_2} [field K] [ V] (v : V) :
V) v = 0 v = 0
theorem module.eval_apply_injective (K : Type u_1) {V : Type u_2} [field K] [ V] :
theorem module.forall_dual_apply_eq_zero_iff (K : Type u_1) {V : Type u_2} [field K] [ V] (v : V) :
( (φ : V), φ v = 0) v = 0
theorem module.dual_rank_eq {K : Type u_1} {V : Type u_2} [field K] [ V] [ V] :
V).lift = V)
theorem module.erange_coe {K : Type u_1} {V : Type u_2} [field K] [ V] [ V] :
noncomputable def module.eval_equiv (K : Type u_1) (V : Type u_2) [field K] [ V] [ V] :
V ≃ₗ[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] [ V] [ V] :
V ≃o V))

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

Equations
@[simp]
theorem module.eval_equiv_to_linear_map {K : Type u_1} {V : Type u_2} [field K] [ V] [ V] :
@[simp]
theorem module.map_eval_equiv_apply {K : Type u_1} {V : Type u_2} [field K] [ V] [ V] (W : V) :
W = W
@[simp]
theorem module.map_eval_equiv_symm_apply {K : Type u_1} {V : Type u_2} [field K] [ V] [ V] (W'' : V))) :
V).symm) W'' = W''
meta def use_finite_instance  :

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} [ M] [decidable_eq ι] (e : ι M) (ε : ι 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] [ M] {e : ι M} {ε : ι M} [decidable_eq ι] (h : ε) (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] [ M] {e : ι M} {ε : ι M} [decidable_eq ι] (h : ε) (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] [ 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
• = l.sum (λ (i : ι) (a : R), a e i)
theorem module.dual_bases.lc_def {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [ M] (e : ι M) (l : ι →₀ R) :
= M R e) l
theorem module.dual_bases.dual_lc {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [ M] {e : ι M} {ε : ι M} [decidable_eq ι] (h : ε) (l : ι →₀ R) (i : ι) :
(ε i) l) = l i
@[simp]
theorem module.dual_bases.coeffs_lc {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [ M] {e : ι M} {ε : ι M} [decidable_eq ι] (h : ε) (l : ι →₀ R) :
h.coeffs l) = l
@[simp]
theorem module.dual_bases.lc_coeffs {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [ M] {e : ι M} {ε : ι M} [decidable_eq ι] (h : ε) (m : M) :
(h.coeffs 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] [ M] {e : ι M} {ε : ι M} [decidable_eq ι] (h : ε) :
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] [ M] {e : ι M} {ε : ι M} [decidable_eq ι] (h : ε) (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] [ M] {e : ι M} {ε : ι M} [decidable_eq ι] (h : ε) (l : ι →₀ R) :
@[simp]
theorem module.dual_bases.coe_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [ M] {e : ι M} {ε : ι M} [decidable_eq ι] (h : ε) :
(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] [ M] {e : ι M} {ε : ι M} [decidable_eq ι] (h : ε) {H : set ι} {x : M} (hmem : x (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] [ M] {e : ι M} {ε : ι M} [decidable_eq ι] (h : ε) [fintype ι] :
def submodule.dual_restrict {R : Type u} {M : Type v} [ M] (W : 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
theorem submodule.dual_restrict_def {R : Type u} {M : Type v} [ M] (W : M) :
@[simp]
theorem submodule.dual_restrict_apply {R : Type u} {M : Type v} [ M] (W : M) (φ : M) (x : W) :
def submodule.dual_annihilator {R : Type u} {M : Type v} [ M] (W : M) :
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} [ M] {W : M} (φ : M) :
(w : M), w W φ w = 0
theorem submodule.dual_restrict_ker_eq_dual_annihilator {R : Type u} {M : Type v} [ M] (W : M) :

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} [ M] (Φ : M)) :
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} [ M] {Φ : M)} (x : M) :
(φ : M), φ Φ φ x = 0
theorem submodule.dual_annihilator_gc (R : Type u_1) (M : Type u_2) [ M] :
theorem submodule.le_dual_annihilator_iff_le_dual_coannihilator {R : Type u} {M : Type v} [ M] {U : M)} {V : M} :
@[simp]
theorem submodule.dual_annihilator_bot {R : Type u} {M : Type v} [ M] :
@[simp]
theorem submodule.dual_annihilator_top {R : Type u} {M : Type v} [ M] :
@[simp]
theorem submodule.dual_coannihilator_bot {R : Type u} {M : Type v} [ M] :
theorem submodule.dual_annihilator_anti {R : Type u} {M : Type v} [ M] {U V : M} (hUV : U V) :
theorem submodule.dual_coannihilator_anti {R : Type u} {M : Type v} [ M] {U V : M)} (hUV : U V) :
theorem submodule.le_dual_annihilator_dual_coannihilator {R : Type u} {M : Type v} [ M] (U : M) :
theorem submodule.le_dual_coannihilator_dual_annihilator {R : Type u} {M : Type v} [ M] (U : M)) :
theorem submodule.dual_annihilator_sup_eq {R : Type u} {M : Type v} [ M] (U V : M) :
theorem submodule.dual_coannihilator_sup_eq {R : Type u} {M : Type v} [ M] (U V : M)) :
theorem submodule.dual_annihilator_supr_eq {R : Type u} {M : Type v} [ M] {ι : Type u_1} (U : ι M) :
( (i : ι), U i).dual_annihilator = (i : ι), (U i).dual_annihilator
theorem submodule.dual_coannihilator_supr_eq {R : Type u} {M : Type v} [ M] {ι : Type u_1} (U : ι M)) :
( (i : ι), U i).dual_coannihilator = (i : ι), (U i).dual_coannihilator
theorem submodule.sup_dual_annihilator_le_inf {R : Type u} {M : Type v} [ M] (U V : M) :

See also subspace.dual_annihilator_inf_eq for vector subspaces.

theorem submodule.supr_dual_annihilator_le_infi {R : Type u} {M : Type v} [ M] {ι : Type u_1} (U : ι M) :
( (i : ι), (U i).dual_annihilator) ( (i : ι), U i).dual_annihilator

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

@[simp]
theorem subspace.dual_coannihilator_top {K : Type u} {V : Type v} [field K] [ V] (W : V) :
theorem subspace.dual_annihilator_dual_coannihilator_eq {K : Type u} {V : Type v} [field K] [ V] {W : V} :
theorem subspace.forall_mem_dual_annihilator_apply_eq_zero_iff {K : Type u} {V : Type v} [field K] [ V] (W : V) (v : V) :
( (φ : V), φ v = 0) v W
def subspace.dual_annihilator_gci (K : Type u_1) (V : Type u_2) [field K] [ V] :

submodule.dual_annihilator and submodule.dual_coannihilator form a Galois coinsertion.

Equations
theorem subspace.dual_annihilator_le_dual_annihilator_iff {K : Type u} {V : Type v} [field K] [ V] {W W' : V} :
theorem subspace.dual_annihilator_inj {K : Type u} {V : Type v} [field K] [ V] {W W' : V} :
noncomputable def subspace.dual_lift {K : Type u} {V : Type v} [field K] [ V] (W : 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] [ V] {W : V} {φ : W} (w : W) :
((W.dual_lift) φ) w = φ w
theorem subspace.dual_lift_of_mem {K : Type u} {V : Type v} [field K] [ V] {W : V} {φ : 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] [ V] (W : V) :
theorem subspace.dual_restrict_left_inverse {K : Type u} {V : Type v} [field K] [ V] (W : V) :
theorem subspace.dual_lift_right_inverse {K : Type u} {V : Type v} [field K] [ V] (W : V) :
theorem subspace.dual_restrict_surjective {K : Type u} {V : Type v} [field K] [ V] {W : V} :
theorem subspace.dual_lift_injective {K : Type u} {V : Type v} [field K] [ V] {W : V} :
noncomputable def subspace.quot_annihilator_equiv {K : Type u} {V : Type v} [field K] [ V] (W : V) :

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

Equations
@[simp]
theorem subspace.quot_annihilator_equiv_apply {K : Type u} {V : Type v} [field K] [ V] (W : V) (φ : V) :
noncomputable def subspace.dual_equiv_dual {K : Type u} {V : Type v} [field K] [ V] (W : V) :

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

Equations
theorem subspace.dual_equiv_dual_def {K : Type u} {V : Type v} [field K] [ V] (W : V) :
@[simp]
theorem subspace.dual_equiv_dual_apply {K : Type u} {V : Type v} [field K] [ V] {W : V} (φ : W) :
@[protected, instance]
def subspace.module.dual.finite_dimensional {K : Type u} {V : Type v} [field K] [ V] [H : V] :
V)
theorem subspace.dual_annihilator_dual_annihilator_eq {K : Type u} {V : Type v} [field K] [ V] [ V] (W : V) :
@[simp]
theorem subspace.dual_finrank_eq {K : Type u} {V : Type v} [field K] [ V] [ V] :
noncomputable def subspace.quot_dual_equiv_annihilator {K : Type u} {V : Type v} [field K] [ V] [ V] (W : V) :

The quotient by the dual is isomorphic to its dual annihilator.

Equations
noncomputable def subspace.quot_equiv_annihilator {K : Type u} {V : Type v} [field K] [ V] [ V] (W : V) :
(V W) ≃ₗ[K]

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

Equations
@[simp]
theorem subspace.finrank_dual_coannihilator_eq {K : Type u} {V : Type v} [field K] [ V] [ V] {Φ : V)} :
theorem subspace.finrank_add_finrank_dual_coannihilator_eq {K : Type u} {V : Type v} [field K] [ V] [ V] (W : V)) :
theorem linear_map.ker_dual_map_eq_dual_annihilator_range {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] (f : M₁ →ₗ[R] M₂) :
theorem linear_map.range_dual_map_le_dual_annihilator_ker {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] (f : M₁ →ₗ[R] M₂) :
def submodule.dual_copairing {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (W : 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] [ M] {W : M} (φ : (W.dual_annihilator)) (x : M) :
def submodule.dual_pairing {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (W : 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] [ M] {W : M} (φ : M) (x : W) :
theorem submodule.range_dual_map_mkq_eq {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (W : M) :

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

def submodule.dual_quot_equiv_dual_annihilator {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (W : M) :

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 submodule.dual_quot_equiv_dual_annihilator_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (W : M) (φ : (M W)) (x : M) :
x =
theorem submodule.dual_copairing_eq {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (W : M) :
@[simp]
theorem submodule.dual_quot_equiv_dual_annihilator_symm_apply_mk {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (W : M) (φ : (W.dual_annihilator)) (x : M) :
= φ x
theorem linear_map.range_dual_map_eq_dual_annihilator_ker_of_surjective {R : Type u_1} {M : Type u_2} {M' : Type u_3} [comm_ring R] [ M] [add_comm_group M'] [ M'] (f : M →ₗ[R] M') (hf : function.surjective f) :
theorem linear_map.dual_pairing_nondegenerate {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [ 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₁] [ V₁] [add_comm_group V₂] [ 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₁] [ V₁] [add_comm_group V₂] [ 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₁] [ V₁] [add_comm_group V₂] [ V₂] {f : V₁ →ₗ[K] V₂} :

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

theorem subspace.dual_pairing_eq {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [ V₁] (W : V₁) :
theorem subspace.dual_pairing_nondegenerate {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [ V₁] (W : V₁) :
theorem subspace.dual_copairing_nondegenerate {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [ V₁] (W : V₁) :
theorem subspace.dual_annihilator_inf_eq {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [ V₁] (W W' : V₁) :
theorem subspace.dual_annihilator_infi_eq {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [ V₁] {ι : Type u_3} [finite ι] (W : ι V₁) :
submodule.dual_annihilator ( (i : ι), W i) = (i : ι),
theorem subspace.is_compl_dual_annihilator {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [ V₁] {W W' : V₁} (h : 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₁] [ V₁] [ V₁] (W : V₁) :
(V₁ W) ≃ₗ[K]

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.finrank_range_dual_map_eq_finrank_range {K : Type u_1} [field K] {V₁ : Type u_2} {V₂ : Type u_3} [add_comm_group V₁] [ V₁] [add_comm_group V₂] [ V₂] [ V₂] (f : V₁ →ₗ[K] V₂) :
@[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₁] [ V₁] [add_comm_group V₂] [ V₂] [ 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₁] [ V₁] [add_comm_group V₂] [ V₂] [ V₂] {f : V₁ →ₗ[K] V₂} :

f.dual_map is bijective if and only if f is

def tensor_product.dual_distrib (R : Type u_1) (M : Type u_2) (N : Type u_3) [ M] [ N] :
M) N) →ₗ[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
• = R)
@[simp]
theorem tensor_product.dual_distrib_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [ M] [ N] (f : M) (g : N) (m : M) (n : N) :
( N) (f ⊗ₜ[R] g)) (m ⊗ₜ[R] n) = f m * g 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] [ M] [ N] (b : R M) (c : R N) :
M N) →ₗ[R] M) 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] [ M] [ N] (b : R M) (c : R N) (f : M N)) :
= 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] [ M] [ N] (b : R M) (c : R N) :
M) N) ≃ₗ[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] [ M] [ N] (b : R M) (c : R N) (ᾰ : M) N)) (ᾰ_1 : N) :
ᾰ_1 = 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] [ M] [ N] (b : R M) (c : R N) (ᾰ : M N)) :
= 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] [ M] [ N] [ M] [ N] [ M] [ N] [nontrivial R] :
M) N) ≃ₗ[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.

Equations