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.

source

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

module.dual R M = (M →ₗ[R] R)

source

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

module.dual_pairing R M = linear_map.id

source

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

source

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

module.dual.inhabited R M = linear_map.inhabited

source

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

module.dual.has_coe_to_fun R M = {coe := linear_map.to_fun semiring.to_module}

source

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

module.dual.eval R M = linear_map.id.flip

source

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

source

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

source

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

source

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)

source

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

⇑((module.dual_prod_dual_equiv_dual R M M').symm) f = (f.comp (linear_map.inl R M M'), f.comp (linear_map.inr R M M'))

source

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'] :

(module.dual R M × module.dual R M') ≃ₗ[R] module.dual R (M × M')

Taking duals distributes over products.

Equations

module.dual_prod_dual_equiv_dual R M M' = linear_map.coprod_equiv R

source

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

source

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

⇑(module.dual_prod_dual_equiv_dual R M M') (φ, ψ) = linear_map.coprod φ ψ

source

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 = ⇑module.dual.transpose f

source

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

f.dual_map = ⇑module.dual.transpose f

source

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

⇑(f.dual_map) g = linear_map.comp g f

source

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

source

@[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₁] :

linear_map.id.dual_map = linear_map.id

source

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

f.dual_map.comp g.dual_map = (g.comp f).dual_map

source

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

function.injective ⇑(f.dual_map)

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

source

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.

Equations

f.dual_map = {to_fun := f.to_linear_map.dual_map.to_fun, map_add' := _, map_smul' := _, inv_fun := ⇑(f.symm.to_linear_map.dual_map), left_inv := _, right_inv := _}

source

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

source

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

source

@[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₂} :

f.dual_map.symm = f.symm.dual_map

source

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

g.dual_map.trans f.dual_map = (f.trans g).dual_map

source

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.

Equations

b.to_dual = ⇑(b.constr ℕ) (λ (v : ι), ⇑(b.constr ℕ) (λ (w : ι), ite (w = v) 1 0))

source

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

source

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

source

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

source

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

source

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

source

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

source

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

M →ₗ[R] R

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

source

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₁

source

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

source

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

source

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

source

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

linear_map.ker b.to_dual = ⊥

source

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 ι] :

linear_map.range b.to_dual = ⊤

source

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

source

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 ι] :

M ≃ₗ[R] module.dual R M

A vector space is linearly equivalent to its dual space.

Equations

b.to_dual_equiv = linear_equiv.of_bijective b.to_dual _

source

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

⇑(b.to_dual_equiv) m = ⇑(b.to_dual) m

source

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

b.dual_basis = b.map b.to_dual_equiv

source

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

source

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

source

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)

source

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

source

@[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 ι] :

⇑(b.dual_basis) = b.coord

source

@[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 ι] :

b.dual_basis.to_dual.comp b.to_dual = module.dual.eval R M

source

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

⇑(b.dual_basis.equiv_fun) l i = ⇑l (⇑b i)

source

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) = ⊥

source

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

linear_map.range (module.dual.eval R M) = ⊤

source

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

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

source

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

b.eval_equiv.to_linear_map = module.dual.eval R M

source

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

source

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

source

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

source

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

(module.rank K V).lift = module.rank K (module.dual K V)

source

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) = ⊥

source

theorem module.map_eval_injective (K : Type u_1) (V : Type u_2) [field K] [add_comm_group V] [module K V] :

function.injective (submodule.map (module.dual.eval K V))

source

theorem module.comap_eval_surjective (K : Type u_1) (V : Type u_2) [field K] [add_comm_group V] [module K V] :

function.surjective (submodule.comap (module.dual.eval K V))

source

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

source

theorem module.eval_apply_injective (K : Type u_1) {V : Type u_2} [field K] [add_comm_group V] [module K V] :

function.injective ⇑(module.dual.eval K V)

source

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

source

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

(module.rank K V).lift = module.rank K (module.dual K V)

source

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) = ⊤

source

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

source

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

subspace K V ≃o subspace K (module.dual K (module.dual K V))

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

Equations

module.map_eval_equiv K V = submodule.order_iso_map_comap (module.eval_equiv K V)

source

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

source

@[simp]

theorem module.map_eval_equiv_apply {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] (W : subspace K V) :

⇑(module.map_eval_equiv K V) W = submodule.map (module.dual.eval K V) W

source

@[simp]

theorem module.map_eval_equiv_symm_apply {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] (W'' : subspace K (module.dual K (module.dual K V))) :

⇑((module.map_eval_equiv K V).symm) W'' = submodule.comap (module.dual.eval K V) W''

source

meta def use_finite_instance :

tactic unit

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

source

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

source

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

h.coeffs m = {support := _.to_finset, to_fun := λ (i : ι), ⇑(ε i) m, mem_support_to_fun := _}

source

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

source

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

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

Equations

module.dual_bases.lc e l = l.sum (λ (i : ι) (a : R), a • e i)

source

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

module.dual_bases.lc e l = ⇑(finsupp.total ι M R e) l

source

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

source

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

h.coeffs (module.dual_bases.lc e l) = l

source

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

module.dual_bases.lc e (h.coeffs m) = m

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

source

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

h.basis = {repr := {to_fun := h.coeffs, map_add' := _, map_smul' := _, inv_fun := module.dual_bases.lc e, left_inv := _, right_inv := _}}

source

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

source

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

⇑(h.basis.repr.symm) l = module.dual_bases.lc e l

source

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

source

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

source

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 ι] :

⇑(h.basis.dual_basis) = ε

source

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

W.dual_restrict = linear_map.dom_restrict' W

source

theorem submodule.dual_restrict_def {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (W : submodule R M) :

W.dual_restrict = W.subtype.dual_map

source

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

⇑(⇑(W.dual_restrict) φ) x = ⇑φ ↑x

source

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

W.dual_annihilator = linear_map.ker W.dual_restrict

source

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

source

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

linear_map.ker W.dual_restrict = W.dual_annihilator

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

source

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

submodule R M

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

Equations

Φ.dual_coannihilator = submodule.comap (module.dual.eval R M) Φ.dual_annihilator

source

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

source

theorem submodule.dual_annihilator_gc (R : Type u_1) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [module R M] :

galois_connection (⇑order_dual.to_dual ∘ submodule.dual_annihilator) (submodule.dual_coannihilator ∘ ⇑order_dual.of_dual)

source

theorem submodule.le_dual_annihilator_iff_le_dual_coannihilator {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {U : submodule R (module.dual R M)} {V : submodule R M} :

U ≤ V.dual_annihilator ↔ V ≤ U.dual_coannihilator

source

@[simp]

theorem submodule.dual_annihilator_bot {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] :

⊥.dual_annihilator = ⊤

source

@[simp]

theorem submodule.dual_annihilator_top {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] :

⊤.dual_annihilator = ⊥

source

@[simp]

theorem submodule.dual_coannihilator_bot {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] :

⊥.dual_coannihilator = ⊤

source

theorem submodule.dual_annihilator_anti {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {U V : submodule R M} (hUV : U ≤ V) :

V.dual_annihilator ≤ U.dual_annihilator

source

theorem submodule.dual_coannihilator_anti {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {U V : submodule R (module.dual R M)} (hUV : U ≤ V) :

V.dual_coannihilator ≤ U.dual_coannihilator

source

theorem submodule.le_dual_annihilator_dual_coannihilator {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (U : submodule R M) :

U ≤ U.dual_annihilator.dual_coannihilator

source

theorem submodule.le_dual_coannihilator_dual_annihilator {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (U : submodule R (module.dual R M)) :

U ≤ U.dual_coannihilator.dual_annihilator

source

theorem submodule.dual_annihilator_dual_coannihilator_dual_annihilator {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (U : submodule R M) :

U.dual_annihilator.dual_coannihilator.dual_annihilator = U.dual_annihilator

source

theorem submodule.dual_coannihilator_dual_annihilator_dual_coannihilator {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (U : submodule R (module.dual R M)) :

U.dual_coannihilator.dual_annihilator.dual_coannihilator = U.dual_coannihilator

source

theorem submodule.dual_annihilator_sup_eq {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

source

theorem submodule.dual_coannihilator_sup_eq {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (U V : submodule R (module.dual R M)) :

(U ⊔ V).dual_coannihilator = U.dual_coannihilator ⊓ V.dual_coannihilator

source

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

source

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

source

theorem submodule.sup_dual_annihilator_le_inf {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] (U V : submodule R M) :

U.dual_annihilator ⊔ V.dual_annihilator ≤ (U ⊓ V).dual_annihilator

See also subspace.dual_annihilator_inf_eq for vector subspaces.

source

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.

source

@[simp]

theorem subspace.dual_coannihilator_top {K : Type u} {V : Type v} [field K] [add_comm_group V] [module K V] (W : subspace K V) :

submodule.dual_coannihilator ⊤ = ⊥

source

theorem subspace.dual_annihilator_dual_coannihilator_eq {K : Type u} {V : Type v} [field K] [add_comm_group V] [module K V] {W : subspace K V} :

(submodule.dual_annihilator W).dual_coannihilator = W

source

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

(∀ (φ : module.dual K V), φ ∈ submodule.dual_annihilator W → ⇑φ v = 0) ↔ v ∈ W

source

def subspace.dual_annihilator_gci (K : Type u_1) (V : Type u_2) [field K] [add_comm_group V] [module K V] :

galois_coinsertion (⇑order_dual.to_dual ∘ submodule.dual_annihilator) (submodule.dual_coannihilator ∘ ⇑order_dual.of_dual)

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

Equations

subspace.dual_annihilator_gci K V = {choice := λ (W : (submodule K (module.dual K V))ᵒᵈ) (h : W ≤ (⇑order_dual.to_dual ∘ submodule.dual_annihilator) ((submodule.dual_coannihilator ∘ ⇑order_dual.of_dual) W)), submodule.dual_coannihilator W, gc := _, u_l_le := _, choice_eq := _}

source

theorem subspace.dual_annihilator_le_dual_annihilator_iff {K : Type u} {V : Type v} [field K] [add_comm_group V] [module K V] {W W' : subspace K V} :

submodule.dual_annihilator W ≤ submodule.dual_annihilator W' ↔ W' ≤ W

source

theorem subspace.dual_annihilator_inj {K : Type u} {V : Type v} [field K] [add_comm_group V] [module K V] {W W' : subspace K V} :

submodule.dual_annihilator W = submodule.dual_annihilator W' ↔ W = W'

source

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

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

source

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

source

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⟩

source

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

source

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

function.left_inverse ⇑(submodule.dual_restrict W) ⇑(W.dual_lift)

source

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

function.right_inverse ⇑(W.dual_lift) ⇑(submodule.dual_restrict W)

source

theorem subspace.dual_restrict_surjective {K : Type u} {V : Type v} [field K] [add_comm_group V] [module K V] {W : subspace K V} :

function.surjective ⇑(submodule.dual_restrict W)

source

theorem subspace.dual_lift_injective {K : Type u} {V : Type v} [field K] [add_comm_group V] [module K V] {W : subspace K V} :

function.injective ⇑(W.dual_lift)

source

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.

Equations

W.quot_annihilator_equiv = ((linear_map.ker (submodule.dual_restrict W)).quot_equiv_of_eq (submodule.dual_annihilator W) _).symm.trans ((submodule.dual_restrict W).quot_ker_equiv_of_surjective subspace.dual_restrict_surjective)

source

@[simp]

theorem subspace.quot_annihilator_equiv_apply {K : Type u} {V : Type v} [field K] [add_comm_group V] [module K V] (W : subspace K V) (φ : module.dual K V) :

⇑(W.quot_annihilator_equiv) (submodule.quotient.mk φ) = ⇑(submodule.dual_restrict W) φ

source

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 from the dual of a subspace W to W.dual_lift.range.

Equations

W.dual_equiv_dual = linear_equiv.of_injective W.dual_lift subspace.dual_lift_injective

source

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

W.dual_equiv_dual.to_linear_map = W.dual_lift.range_restrict

source

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

⇑(W.dual_equiv_dual) φ = ⟨⇑(W.dual_lift) φ, _⟩

source

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

source

theorem subspace.dual_annihilator_dual_annihilator_eq {K : Type u} {V : Type v} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] (W : subspace K V) :

(submodule.dual_annihilator W).dual_annihilator = ⇑(module.map_eval_equiv K V) W

source

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

finite_dimensional.finrank K (module.dual K V) = finite_dimensional.finrank K V

source

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.

Equations

W.quot_dual_equiv_annihilator = finite_dimensional.linear_equiv.quot_equiv_of_quot_equiv (W.quot_annihilator_equiv.trans W.dual_equiv_dual)

source

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.

Equations

W.quot_equiv_annihilator = (finite_dimensional.linear_equiv.quot_equiv_of_equiv ((basis.of_vector_space K ↥W).to_dual_equiv.trans W.dual_equiv_dual) (basis.of_vector_space K V).to_dual_equiv).trans W.quot_dual_equiv_annihilator

source

@[simp]

theorem subspace.finrank_dual_coannihilator_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)} :

finite_dimensional.finrank K ↥(submodule.dual_coannihilator Φ) = finite_dimensional.finrank K ↥(submodule.dual_annihilator Φ)

source

theorem subspace.finrank_add_finrank_dual_coannihilator_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)) :

finite_dimensional.finrank K ↥W + finite_dimensional.finrank K ↥(submodule.dual_coannihilator W) = finite_dimensional.finrank K V

source

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

linear_map.ker f.dual_map = (linear_map.range f).dual_annihilator

source

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

linear_map.range f.dual_map ≤ (linear_map.ker f).dual_annihilator

source

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

↥(W.dual_annihilator) →ₗ[R] M ⧸ W →ₗ[R] R

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

See subspace.dual_copairing_nondegenerate.

Equations

W.dual_copairing = (W.liftq ((module.dual_pairing R M).dom_restrict W.dual_annihilator).flip _).flip

source

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

⇑(⇑(W.dual_copairing) φ) (submodule.quotient.mk x) = ⇑φ x

source

def submodule.dual_pairing {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 ⧸ W.dual_annihilator →ₗ[R] ↥W →ₗ[R] R

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

W.dual_pairing = W.dual_annihilator.liftq W.dual_restrict _

source

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

⇑(⇑(W.dual_pairing) (submodule.quotient.mk φ)) x = ⇑φ ↑x

source

theorem submodule.range_dual_map_mkq_eq {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (W : submodule R M) :

linear_map.range W.mkq.dual_map = W.dual_annihilator

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

source

def submodule.dual_quot_equiv_dual_annihilator {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 ⧸ W) ≃ₗ[R] ↥(W.dual_annihilator)

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

W.dual_quot_equiv_dual_annihilator = linear_equiv.of_linear (linear_map.cod_restrict W.dual_annihilator W.mkq.dual_map _) W.dual_copairing _ _

source

@[simp]

theorem submodule.dual_quot_equiv_dual_annihilator_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 ⧸ W)) (x : M) :

⇑(⇑(W.dual_quot_equiv_dual_annihilator) φ) x = ⇑φ (submodule.quotient.mk x)

source

theorem submodule.dual_copairing_eq {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (W : submodule R M) :

W.dual_copairing = W.dual_quot_equiv_dual_annihilator.symm.to_linear_map

source

@[simp]

theorem submodule.dual_quot_equiv_dual_annihilator_symm_apply_mk {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) :

⇑(⇑(W.dual_quot_equiv_dual_annihilator.symm) φ) (submodule.quotient.mk x) = ⇑φ x

source

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] [add_comm_group M] [module R M] [add_comm_group M'] [module R M'] (f : M →ₗ[R] M') (hf : function.surjective ⇑f) :

linear_map.range f.dual_map = (linear_map.ker f).dual_annihilator

source

theorem linear_map.range_dual_map_eq_dual_annihilator_ker_of_subtype_range_surjective {R : Type u_1} {M : Type u_2} {M' : Type u_3} [comm_ring R] [add_comm_group M] [module R M] [add_comm_group M'] [module R M'] (f : M →ₗ[R] M') (hf : function.surjective ⇑((linear_map.range f).subtype.dual_map)) :

linear_map.range f.dual_map = (linear_map.ker f).dual_annihilator

source

theorem linear_map.dual_pairing_nondegenerate {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [module K V₁] :

(module.dual_pairing K V₁).nondegenerate

source

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

function.surjective ⇑(f.dual_map)

source

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

linear_map.range f.dual_map = (linear_map.ker f).dual_annihilator

source

@[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₂} :

function.surjective ⇑(f.dual_map) ↔ function.injective ⇑f

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

source

theorem subspace.dual_pairing_eq {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [module K V₁] (W : subspace K V₁) :

submodule.dual_pairing W = W.quot_annihilator_equiv.to_linear_map

source

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

(submodule.dual_pairing W).nondegenerate

source

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

(submodule.dual_copairing W).nondegenerate

source

theorem subspace.dual_annihilator_inf_eq {K : Type u_1} [field K] {V₁ : Type u_2} [add_comm_group V₁] [module K V₁] (W W' : subspace K V₁) :

submodule.dual_annihilator (W ⊓ W') = submodule.dual_annihilator W ⊔ submodule.dual_annihilator W'

source

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

submodule.dual_annihilator (⨅ (i : ι), W i) = ⨆ (i : ι), submodule.dual_annihilator (W i)

source

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

is_compl (submodule.dual_annihilator W) (submodule.dual_annihilator W')

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

source

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

module.dual K (V₁ ⧸ W) ≃ₗ[K] module.dual K V₁ ⧸ linear_map.range W.dual_lift

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

W.dual_quot_distrib = (submodule.dual_quot_equiv_dual_annihilator W).trans W.quot_dual_equiv_annihilator.symm

source

@[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₁] [module K V₁] [add_comm_group V₂] [module K V₂] [finite_dimensional K V₂] (f : V₁ →ₗ[K] V₂) :

finite_dimensional.finrank K ↥(linear_map.range f.dual_map) = finite_dimensional.finrank K ↥(linear_map.range f)

source

@[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₂} :

function.injective ⇑(f.dual_map) ↔ function.surjective ⇑f

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

source

@[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₂} :

function.bijective ⇑(f.dual_map) ↔ function.bijective ⇑f

f.dual_map is bijective if and only if f is

source

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)

source

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

⇑(⇑(tensor_product.dual_distrib R M N) (f ⊗ₜ[R] g)) (m ⊗ₜ[R] n) = ⇑f m * ⇑g n

source

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

source

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

source

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

tensor_product.dual_distrib_equiv_of_basis b c = linear_equiv.of_linear (tensor_product.dual_distrib R M N) (tensor_product.dual_distrib_inv_of_basis b c) _ _

source

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

source

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

source

@[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.

Equations

tensor_product.dual_distrib_equiv R M N = tensor_product.dual_distrib_equiv_of_basis (module.free.choose_basis R M) (module.free.choose_basis R N)