mathlibdocumentation

linear_algebra.dual

Dual vector spaces #

The dual space of an R-module M is the R-module of linear maps M → R.

Main definitions #

• dual R M defines the dual space of M over R.
• Given a basis for an R-module M, basis.to_dual produces a map from M to dual R M.
• Given families of vectors e and ε, dual_pair e ε states that these families have the characteristic properties of a basis and a dual.
• dual_annihilator W is the submodule of dual R M where every element annihilates W.

Main results #

• to_dual_equiv : the linear equivalence between the dual module and primal module, given a finite basis.
• dual_pair.basis and dual_pair.eq_dual: if e and ε form a dual pair, e is a basis and ε is its dual basis.
• quot_equiv_annihilator: the quotient by a subspace is isomorphic to its dual annihilator.

Notation #

We sometimes use V' as local notation for dual K V.

TODO #

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

@[protected, instance]
def module.dual.module (R : Type u_1) (M : Type u_2) [ M] :
M)
@[protected, instance]
def module.dual.add_comm_monoid (R : Type u_1) (M : Type u_2) [ M] :
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
Instances for module.dual
@[protected, instance]
def module.dual.add_comm_group {S : Type u_1} [comm_ring S] {N : Type u_2} [ N] :
Equations
@[protected, instance]
def module.linear_map_class (R : Type u_1) (M : Type u_2) [ M] :
R 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') :
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) [fin : fintype ι] :
@[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) [fintype ι] :

A vector space is linearly equivalent to its dual space.

Equations
@[simp]
theorem basis.to_dual_equiv_symm_apply {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [ M] [decidable_eq ι] (b : R M) [fintype ι] (ᾰ : M) :
@[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) [fintype ι] (ᾰ : M) :
(b.to_dual_equiv) ᾰ = (b.to_dual) ᾰ
noncomputable def basis.dual_basis {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [ M] [decidable_eq ι] (b : R M) [fintype ι] :
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) [fintype ι] (i j : ι) :
((b.dual_basis) i) (b j) = ite (j = i) 1 0
theorem basis.total_dual_basis {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [ M] [decidable_eq ι] (b : R M) [fintype ι] (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) [fintype ι] (l : M) (i : ι) :
((b.dual_basis.repr) l) i = l (b i)
theorem basis.dual_basis_equiv_fun {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [ M] [decidable_eq ι] (b : R M) [fintype ι] (l : M) (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) [fintype ι] (i : ι) (m : M) :
((b.dual_basis) i) m = ((b.repr) m) i
@[simp]
theorem basis.coe_dual_basis {R : Type u_1} {M : Type u_2} {ι : Type u_5} [comm_ring R] [ M] [decidable_eq ι] (b : R M) [fintype ι] :
@[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) [fintype ι] :
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} [fintype ι] (b : R M) :
noncomputable def basis.eval_equiv {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {ι : Type u_3} [fintype ι] (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} [fintype ι] (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] [fintype ι] (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_dim_eq {K : Type u_3} {V : Type u_4} {ι : Type u_5} [field K] [ V] [fintype ι] (b : K V) :
V).lift = V)
theorem module.eval_ker {K : Type u_1} {V : Type u_2} [field K] [ V] :
theorem module.dual_dim_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
@[simp]
theorem module.eval_equiv_to_linear_map {K : Type u_1} {V : Type u_2} [field K] [ V] [ V] :
@[nolint]
structure dual_pair {R : Type u_1} {M : Type u_2} {ι : Type u_3} [ M] [decidable_eq ι] (e : ι → M) (ε : ι → M) :
Type (max u_2 u_3)
• eval : ∀ (i j : ι), (ε i) (e j) = ite (i = j) 1 0
• total : ∀ {m : M}, (∀ (i : ι), (ε i) m = 0)m = 0
• finite : Π (m : M), fintype {i : ι | (ε i) m 0}

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

Instances for dual_pair
• dual_pair.has_sizeof_inst
def dual_pair.coeffs {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [ M] {e : ι → M} {ε : ι → M} [decidable_eq ι] (h : ε) (m : M) :
ι →₀ R

The coefficients of v on the basis e

Equations
@[simp]
theorem dual_pair.coeffs_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [ M] {e : ι → M} {ε : ι → M} [decidable_eq ι] (h : ε) (m : M) (i : ι) :
(h.coeffs m) i = (ε i) m
def dual_pair.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 = l.sum (λ (i : ι) (a : R), a e i)
theorem dual_pair.lc_def {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [ M] (e : ι → M) (l : ι →₀ R) :
l = M R e) l
theorem dual_pair.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 dual_pair.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 dual_pair.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

@[simp]
theorem dual_pair.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 dual_pair.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
def dual_pair.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_pair e ε).basis shows the family of vectors e forms a basis.

Equations
@[simp]
theorem dual_pair.coe_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [ M] {e : ι → M} {ε : ι → M} [decidable_eq ι] (h : ε) :
(h.basis) = e
theorem dual_pair.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 0i H
theorem dual_pair.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
@[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) :
theorem submodule.dual_annihilator_sup_eq_inf_dual_annihilator {R : Type u} {M : Type v} [ M] (U V : M) :
def submodule.dual_annihilator_comap {R : Type u} {M : Type v} [ M] (Φ : M)) :
M

The pullback of a submodule in the dual space along the evaluation map.

Equations
theorem submodule.mem_dual_annihilator_comap_iff {R : Type u} {M : Type v} [ M] {Φ : M)} (x : M) :
∀ (φ : M), φ Φφ x = 0
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 the natural extension of φ to an element of the dual of V. That is, dual_lift W φ sends w ∈ W to φ x and x in the complement of W to 0.

Equations
@[simp]
theorem subspace.dual_lift_of_subtype {K : Type u} {V : Type v} [field K] [ 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
noncomputable def subspace.dual_equiv_dual {K : Type u} {V : Type v} [field K] [ V] (W : V) :

The natural isomorphism forom 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)
@[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_annihilator_comap_eq {K : Type u} {V : Type v} [field K] [ V] [ V] {Φ : V)} :
theorem subspace.finrank_add_finrank_dual_annihilator_comap_eq {K : Type u} {V : Type v} [field K] [ V] [ V] (W : V)) :
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
@[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₃) :
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₃) :
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₂) :
@[simp]
theorem linear_map.finrank_range_dual_map_eq_finrank_range {K : Type u_4} [field K] {V₁ : Type u_5} {V₂ : Type u_6} [add_comm_group V₁] [ V₁] [add_comm_group V₂] [ V₂] [ V₂] (f : V₁ →ₗ[K] V₂) :
theorem linear_map.range_dual_map_eq_dual_annihilator_ker {K : Type u_4} [field K] {V₁ : Type u_5} {V₂ : Type u_6} [add_comm_group V₁] [ V₁] [add_comm_group V₂] [ V₂] [ V₂] [ V₁] (f : V₁ →ₗ[K] V₂) :
theorem linear_map.dual_pairing_nondegenerate {K : Type u_4} {V : Type u_5} [field K] [ V] :
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