# Dual vector spaces #

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.dualPairing 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.
• LinearMap.dualMap is Module.Dual.transpose of a given linear map, for dot notation.
• LinearEquiv.dualMap is for the dual of an equivalence.
• Bases:
• Basis.toDual produces the map M →ₗ[R] Dual R M associated to a basis for an R-module M.
• Basis.toDual_equiv is the equivalence M ≃ₗ[R] Dual R M associated to a finite basis.
• Basis.dualBasis 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.dualRestrict W is the transpose Dual R M →ₗ[R] Dual R W of the inclusion map.
• Submodule.dualAnnihilator W is the kernel of W.dualRestrict. That is, it is the submodule of dual R M whose elements all annihilate W.
• Submodule.dualRestrict_comap W' is the dual annihilator of W' : Submodule R (Dual R M), pulled back along Module.Dual.eval R M.
• Submodule.dualCopairing W is the canonical pairing between W.dualAnnihilator and M ⧸ W. It is nondegenerate for vector spaces (subspace.dualCopairing_nondegenerate).
• Submodule.dualPairing W is the canonical pairing between Dual R M ⧸ W.dualAnnihilator and W. It is nondegenerate for vector spaces (Subspace.dualPairing_nondegenerate).
• Vector spaces:
• Subspace.dualLift W is an arbitrary section (using choice) of Submodule.dualRestrict W.

## Main results #

• Bases:
• Module.dualBasis.basis and Module.dualBasis.coe_basis: if e and ε form a dual pair, then e is a basis.
• Module.dualBasis.coe_dualBasis: if e and ε form a dual pair, then ε is a basis.
• Annihilators:
• Module.dualAnnihilator_gc R M is the antitone Galois correspondence between Submodule.dualAnnihilator and Submodule.dualConnihilator.
• LinearMap.ker_dual_map_eq_dualAnnihilator_range says that f.dual_map.ker = f.range.dualAnnihilator
• LinearMap.range_dual_map_eq_dualAnnihilator_ker_of_subtype_range_surjective says that f.dual_map.range = f.ker.dualAnnihilator; this is specialized to vector spaces in LinearMap.range_dual_map_eq_dualAnnihilator_ker.
• Submodule.dualQuotEquivDualAnnihilator is the equivalence Dual R (M ⧸ W) ≃ₗ[R] W.dualAnnihilator
• Submodule.quotDualCoannihilatorToDual is the nondegenerate pairing M ⧸ W.dualCoannihilator →ₗ[R] Dual R W. It is an perfect pairing when R is a field and W is finite-dimensional.
• Vector spaces:
• Subspace.dualAnnihilator_dualConnihilator_eq says that the double dual annihilator, pulled back ground Module.Dual.eval, is the original submodule.
• Subspace.dualAnnihilator_gci says that module.dualAnnihilator_gc R M is an antitone Galois coinsertion.
• Subspace.quotAnnihilatorEquiv is the equivalence Dual K V ⧸ W.dualAnnihilator ≃ₗ[K] Dual K W.
• LinearMap.dualPairing_nondegenerate says that Module.dualPairing is nondegenerate.
• Subspace.is_compl_dualAnnihilator says that the dual annihilator carries complementary subspaces to complementary subspaces.
• Finite-dimensional vector spaces:
• Module.evalEquiv is the equivalence V ≃ₗ[K] Dual K (Dual K V)
• Module.mapEvalEquiv is the order isomorphism between subspaces of V and subspaces of Dual K (Dual K V).
• Subspace.orderIsoFiniteCodimDim is the antitone order isomorphism between finite-codimensional subspaces of V and finite-dimensional subspaces of Dual K V.
• Subspace.orderIsoFiniteDimensional is the antitone order isomorphism between subspaces of a finite-dimensional vector space V and subspaces of its dual.
• Subspace.quotDualEquivAnnihilator W is the equivalence (Dual K V ⧸ W.dualLift.range) ≃ₗ[K] W.dualAnnihilator, where W.dualLift.range is a copy of Dual K W inside Dual K V.
• Subspace.quotEquivAnnihilator W is the equivalence (V ⧸ W) ≃ₗ[K] W.dualAnnihilator
• Subspace.dualQuotDistrib W is an equivalence Dual K (V₁ ⧸ W) ≃ₗ[K] Dual K V₁ ⧸ W.dualLift.range from an arbitrary choice of splitting of V₁.
@[reducible]
def Module.Dual (R : Type uR) (M : Type uM) [] [] [Module R M] :
Type (max uM uR)

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

Equations
Instances For
def Module.dualPairing (R : Type u_1) (M : Type u_2) [] [] [Module R M] :

The canonical pairing of a vector space and its algebraic dual.

Equations
• = LinearMap.id
Instances For
@[simp]
theorem Module.dualPairing_apply (R : Type uR) (M : Type uM) [] [] [Module R M] (v : ) (x : M) :
(() v) x = v x
instance Module.Dual.instInhabitedDual (R : Type uR) (M : Type uM) [] [] [Module R M] :
Equations
• = { default := 0 }
def Module.Dual.eval (R : Type uR) (M : Type uM) [] [] [Module R M] :

Maps a module M to the dual of the dual of M. See Module.erange_coe and Module.evalEquiv.

Equations
Instances For
@[simp]
theorem Module.Dual.eval_apply (R : Type uR) (M : Type uM) [] [] [Module R M] (v : M) (a : ) :
(() v) a = a v
def Module.Dual.transpose {R : Type uR} {M : Type uM} [] [] [Module R M] {M' : Type uM'} [] [Module R M'] :

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

Equations
Instances For
theorem Module.Dual.transpose_apply {R : Type uR} {M : Type uM} [] [] [Module R M] {M' : Type uM'} [] [Module R M'] (u : M →ₗ[R] M') (l : Module.Dual R M') :
(Module.Dual.transpose u) l = l ∘ₗ u
theorem Module.Dual.transpose_comp {R : Type uR} {M : Type uM} [] [] [Module R M] {M' : Type uM'} [] [Module R M'] {M'' : Type uM''} [] [Module R M''] (u : M' →ₗ[R] M'') (v : M →ₗ[R] M') :
Module.Dual.transpose (u ∘ₗ v) = Module.Dual.transpose v ∘ₗ Module.Dual.transpose u
@[simp]
theorem Module.dualProdDualEquivDual_symm_apply (R : Type uR) (M : Type uM) [] [] [Module R M] (M' : Type uM') [] [Module R M'] (f : M × M' →ₗ[R] R) :
() f = (f ∘ₗ LinearMap.inl R M M', f ∘ₗ LinearMap.inr R M M')
@[simp]
theorem Module.dualProdDualEquivDual_apply_apply (R : Type uR) (M : Type uM) [] [] [Module R M] (M' : Type uM') [] [Module R M'] (f : (M →ₗ[R] R) × (M' →ₗ[R] R)) (a : M × M') :
(() f) a = f.1 a.1 + f.2 a.2
def Module.dualProdDualEquivDual (R : Type uR) (M : Type uM) [] [] [Module R M] (M' : Type uM') [] [Module R M'] :

Taking duals distributes over products.

Equations
Instances For
@[simp]
theorem Module.dualProdDualEquivDual_apply (R : Type uR) (M : Type uM) [] [] [Module R M] (M' : Type uM') [] [Module R M'] (φ : ) (ψ : Module.Dual R M') :
() (φ, ψ) =
def LinearMap.dualMap {R : Type u} [] {M₁ : Type v} {M₂ : Type v'} [] [Module R M₁] [] [Module R M₂] (f : M₁ →ₗ[R] M₂) :

Given a linear map f : M₁ →ₗ[R] M₂, f.dualMap is the linear map between the dual of M₂ and M₁ such that it maps the functional φ to φ ∘ f.

Equations
• = Module.Dual.transpose f
Instances For
theorem LinearMap.dualMap_eq_lcomp {R : Type u} [] {M₁ : Type v} {M₂ : Type v'} [] [Module R M₁] [] [Module R M₂] (f : M₁ →ₗ[R] M₂) :
theorem LinearMap.dualMap_def {R : Type u} [] {M₁ : Type v} {M₂ : Type v'} [] [Module R M₁] [] [Module R M₂] (f : M₁ →ₗ[R] M₂) :
= Module.Dual.transpose f
theorem LinearMap.dualMap_apply' {R : Type u} [] {M₁ : Type v} {M₂ : Type v'} [] [Module R M₁] [] [Module R M₂] (f : M₁ →ₗ[R] M₂) (g : Module.Dual R M₂) :
g = g ∘ₗ f
@[simp]
theorem LinearMap.dualMap_apply {R : Type u} [] {M₁ : Type v} {M₂ : Type v'} [] [Module R M₁] [] [Module R M₂] (f : M₁ →ₗ[R] M₂) (g : Module.Dual R M₂) (x : M₁) :
( g) x = g (f x)
@[simp]
theorem LinearMap.dualMap_id {R : Type u} [] {M₁ : Type v} [] [Module R M₁] :
LinearMap.dualMap LinearMap.id = LinearMap.id
theorem LinearMap.dualMap_comp_dualMap {R : Type u} [] {M₁ : Type v} {M₂ : Type v'} [] [Module R M₁] [] [Module R M₂] {M₃ : Type u_1} [] [Module R M₃] (f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
= LinearMap.dualMap (g ∘ₗ f)
theorem LinearMap.dualMap_injective_of_surjective {R : Type u} [] {M₁ : Type v} {M₂ : Type v'} [] [Module R M₁] [] [Module R M₂] {f : M₁ →ₗ[R] M₂} (hf : ) :

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

def LinearEquiv.dualMap {R : Type u} [] {M₁ : Type v} {M₂ : Type v'} [] [Module R M₁] [] [Module R M₂] (f : M₁ ≃ₗ[R] M₂) :

The Linear_equiv version of LinearMap.dualMap.

Equations
• = let __spread.0 := ; { toLinearMap := __spread.0, invFun := , left_inv := , right_inv := }
Instances For
@[simp]
theorem LinearEquiv.dualMap_apply {R : Type u} [] {M₁ : Type v} {M₂ : Type v'} [] [Module R M₁] [] [Module R M₂] (f : M₁ ≃ₗ[R] M₂) (g : Module.Dual R M₂) (x : M₁) :
( g) x = g (f x)
@[simp]
theorem LinearEquiv.dualMap_refl {R : Type u} [] {M₁ : Type v} [] [Module R M₁] :
@[simp]
theorem LinearEquiv.dualMap_symm {R : Type u} [] {M₁ : Type v} {M₂ : Type v'} [] [Module R M₁] [] [Module R M₂] {f : M₁ ≃ₗ[R] M₂} :
theorem LinearEquiv.dualMap_trans {R : Type u} [] {M₁ : Type v} {M₂ : Type v'} [] [Module R M₁] [] [Module R M₂] {M₃ : Type u_1} [] [Module R M₃] (f : M₁ ≃ₗ[R] M₂) (g : M₂ ≃ₗ[R] M₃) :
= LinearEquiv.dualMap (f ≪≫ₗ g)
@[simp]
theorem Dual.apply_one_mul_eq {R : Type u} [] (f : ) (r : R) :
f 1 * r = f r
@[simp]
theorem LinearMap.range_dualMap_dual_eq_span_singleton {R : Type u} [] {M₁ : Type v} [] [Module R M₁] (f : Module.Dual R M₁) :
def Basis.toDual {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) :

The linear map from a vector space equipped with basis to its dual vector space, taking basis elements to corresponding dual basis elements.

Equations
• = () fun (v : ι) => () fun (w : ι) => if w = v then 1 else 0
Instances For
theorem Basis.toDual_apply {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) (i : ι) (j : ι) :
(() (b i)) (b j) = if i = j then 1 else 0
@[simp]
theorem Basis.toDual_total_left {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) (f : ι →₀ R) (i : ι) :
(() ((Finsupp.total ι M R b) f)) (b i) = f i
@[simp]
theorem Basis.toDual_total_right {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) (f : ι →₀ R) (i : ι) :
(() (b i)) ((Finsupp.total ι M R b) f) = f i
theorem Basis.toDual_apply_left {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) (m : M) (i : ι) :
(() m) (b i) = (b.repr m) i
theorem Basis.toDual_apply_right {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) (i : ι) (m : M) :
(() (b i)) m = (b.repr m) i
theorem Basis.coe_toDual_self {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) (i : ι) :
() (b i) =
def Basis.toDualFlip {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) (m : M) :

h.toDual_flip v is the linear map sending w to h.toDual w v.

Equations
• = () m
Instances For
theorem Basis.toDualFlip_apply {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) (m₁ : M) (m₂ : M) :
() m₂ = (() m₂) m₁
theorem Basis.toDual_eq_repr {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) (m : M) (i : ι) :
(() m) (b i) = (b.repr m) i
theorem Basis.toDual_eq_equivFun {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) [] (m : M) (i : ι) :
(() m) (b i) = () m i
theorem Basis.toDual_injective {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) :
theorem Basis.toDual_inj {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) (m : M) (a : () m = 0) :
m = 0
theorem Basis.toDual_ker {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) :
theorem Basis.toDual_range {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) [] :
@[simp]
theorem Basis.sum_dual_apply_smul_coord {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) (f : ) :
(Finset.sum Finset.univ fun (x : ι) => f (b x) ) = f
def Basis.toDualEquiv {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) [] :

A vector space is linearly equivalent to its dual space.

Equations
Instances For
@[simp]
theorem Basis.toDualEquiv_apply {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) [] (m : M) :
m = () m
theorem Basis.linearEquiv_dual_iff_finiteDimensional {K : Type uK} {V : Type uV} [] [] [Module K V] :

A vector space over a field is isomorphic to its dual if and only if it is finite-dimensional: a consequence of the Erdős-Kaplansky theorem.

def Basis.dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) [] :
Basis ι R ()

Maps a basis for V to a basis for the dual space.

Equations
Instances For
theorem Basis.dualBasis_apply_self {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) [] (i : ι) (j : ι) :
(() i) (b j) = if j = i then 1 else 0
theorem Basis.total_dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) [] (f : ι →₀ R) (i : ι) :
((Finsupp.total ι () R ()) f) (b i) = f i
theorem Basis.dualBasis_repr {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) [] (l : ) (i : ι) :
(().repr l) i = l (b i)
theorem Basis.dualBasis_apply {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) [] (i : ι) (m : M) :
(() i) m = (b.repr m) i
@[simp]
theorem Basis.coe_dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) [] :
() =
@[simp]
theorem Basis.toDual_toDual {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) [] :
=
theorem Basis.dualBasis_equivFun {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) [] (l : ) (i : ι) :
l i = l (b i)
theorem Basis.eval_ker {R : Type uR} {M : Type uM} [] [] [Module R M] {ι : Type u_1} (b : Basis ι R M) :
theorem Basis.eval_range {R : Type uR} {M : Type uM} [] [] [Module R M] {ι : Type u_1} [] (b : Basis ι R M) :
instance Basis.dual_free {R : Type uR} {M : Type uM} [] [] [Module R M] [] [] :
Equations
• =
instance Basis.dual_finite {R : Type uR} {M : Type uM} [] [] [Module R M] [] [] :
Equations
• =
@[simp]
theorem Basis.total_coord {R : Type uR} {M : Type uM} {ι : Type uι} [] [] [Module R M] [] (b : Basis ι R M) (f : ι →₀ R) (i : ι) :
((Finsupp.total ι () R ()) f) (b i) = f i

simp normal form version of total_dualBasis

theorem Basis.dual_rank_eq {K : Type uK} {V : Type uV} {ι : Type uι} [] [] [Module K V] [] (b : Basis ι K V) :
theorem Module.eval_ker (K : Type uK) (V : Type uV) [] [] [Module K V] [] :
theorem Module.map_eval_injective (K : Type uK) (V : Type uV) [] [] [Module K V] [] :
theorem Module.comap_eval_surjective (K : Type uK) (V : Type uV) [] [] [Module K V] [] :
theorem Module.eval_apply_eq_zero_iff (K : Type uK) {V : Type uV} [] [] [Module K V] [] (v : V) :
() v = 0 v = 0
theorem Module.eval_apply_injective (K : Type uK) {V : Type uV} [] [] [Module K V] [] :
theorem Module.forall_dual_apply_eq_zero_iff (K : Type uK) {V : Type uV} [] [] [Module K V] [] (v : V) :
(∀ (φ : ), φ v = 0) v = 0
@[simp]
theorem Module.subsingleton_dual_iff (K : Type uK) {V : Type uV} [] [] [Module K V] [] :
instance Module.instSubsingletonDual (K : Type uK) {V : Type uV} [] [] [Module K V] [] [] :
Equations
• =
@[simp]
theorem Module.nontrivial_dual_iff (K : Type uK) {V : Type uV} [] [] [Module K V] [] :
instance Module.instNontrivialDual (K : Type uK) {V : Type uV} [] [] [Module K V] [] [] :
Equations
• =
theorem Module.finite_dual_iff (K : Type uK) {V : Type uV} [] [] [Module K V] [] :
theorem Module.dual_rank_eq {K : Type uK} {V : Type uV} [] [] [Module K V] [] [] :
theorem Module.erange_coe {K : Type uK} {V : Type uV} [] [] [Module K V] [] [] :
class Module.IsReflexive (R : Type u_1) (M : Type u_2) [] [] [Module R M] :

A reflexive module is one for which the natural map to its double dual is a bijection.

Any finitely-generated free module (and thus any finite-dimensional vector space) is reflexive. See Module.IsReflexive.of_finite_of_free.

• bijective_dual_eval' :

A reflexive module is one for which the natural map to its double dual is a bijection.

Instances
theorem Module.bijective_dual_eval (R : Type u_1) (M : Type u_2) [] [] [Module R M] [] :
instance Module.IsReflexive.of_finite_of_free (R : Type u_1) (M : Type u_2) [] [] [Module R M] [] [] :
Equations
• =
def Module.evalEquiv (R : Type u_1) (M : Type u_2) [] [] [Module R M] [] :

The bijection between a reflexive module and its double dual, bundled as a LinearEquiv.

Equations
Instances For
@[simp]
theorem Module.evalEquiv_toLinearMap (R : Type u_1) (M : Type u_2) [] [] [Module R M] [] :
() =
@[simp]
theorem Module.evalEquiv_apply (R : Type u_1) (M : Type u_2) [] [] [Module R M] [] (m : M) :
() m = () m
@[simp]
theorem Module.apply_evalEquiv_symm_apply (R : Type u_1) (M : Type u_2) [] [] [Module R M] [] (f : ) (g : Module.Dual R ()) :
f (() g) = g f
@[simp]
theorem Module.symm_dualMap_evalEquiv (R : Type u_1) (M : Type u_2) [] [] [Module R M] [] :
instance Module.Dual.instIsReflecive (R : Type u_1) (M : Type u_2) [] [] [Module R M] [] :

The dual of a reflexive module is reflexive.

Equations
• =
def Module.mapEvalEquiv (R : Type u_1) (M : Type u_2) [] [] [Module R M] [] :

The isomorphism Module.evalEquiv induces an order isomorphism on subspaces.

Equations
Instances For
@[simp]
theorem Module.mapEvalEquiv_apply (R : Type u_1) (M : Type u_2) [] [] [Module R M] [] (W : ) :
() W =
@[simp]
theorem Module.mapEvalEquiv_symm_apply (R : Type u_1) (M : Type u_2) [] [] [Module R M] [] (W'' : Submodule R (Module.Dual R ())) :
() W'' = Submodule.comap () W''
instance Prod.instModuleIsReflexive (R : Type u_1) (M : Type u_2) (N : Type u_3) [] [] [] [Module R M] [Module R N] [] [] :
Equations
• =
theorem Module.equiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [Module R M] [Module R N] [] (e : M ≃ₗ[R] N) :
instance MulOpposite.instModuleIsReflexive (R : Type u_1) (M : Type u_2) [] [] [Module R M] [] :
Equations
• =
instance ULift.instModuleIsReflexive (R : Type u_1) (M : Type u_2) [] [] [Module R M] [] :
Equations
• =
theorem Submodule.exists_dual_map_eq_bot_of_nmem {R : Type u_1} {M : Type u_2} [] [] [Module R M] {p : } {x : M} (hx : xp) (hp' : Module.Free R (M p)) :
∃ (f : ), f x 0 =
theorem Submodule.exists_dual_map_eq_bot_of_lt_top {R : Type u_1} {M : Type u_2} [] [] [Module R M] {p : } (hp : p < ) (hp' : Module.Free R (M p)) :
∃ (f : ), f 0 =

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
structure Module.DualBases {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] [] (e : ιM) (ε : ι) :

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

• eval : ∀ (i j : ι), (ε i) (e j) = if i = j then 1 else 0
• total : ∀ {m : M}, (∀ (i : ι), (ε i) m = 0)m = 0
• finite : ∀ (m : M), Set.Finite {i : ι | (ε i) m 0}
Instances For
def Module.DualBases.coeffs {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] {e : ιM} {ε : ι} [] (h : ) (m : M) :
ι →₀ R

The coefficients of v on the basis e

Equations
• = { support := , toFun := fun (i : ι) => (ε i) m, mem_support_toFun := }
Instances For
@[simp]
theorem Module.DualBases.coeffs_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] {e : ιM} {ε : ι} [] (h : ) (m : M) (i : ι) :
() i = (ε i) m
def Module.DualBases.lc {R : Type u_1} {M : Type u_2} [] [] [Module R M] {ι : Type u_4} (e : ιM) (l : ι →₀ R) :
M

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

Equations
Instances For
theorem Module.DualBases.lc_def {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] (e : ιM) (l : ι →₀ R) :
= (Finsupp.total ι M R e) l
theorem Module.DualBases.dual_lc {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] {e : ιM} {ε : ι} [] (h : ) (l : ι →₀ R) (i : ι) :
(ε i) () = l i
@[simp]
theorem Module.DualBases.coeffs_lc {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] {e : ιM} {ε : ι} [] (h : ) (l : ι →₀ R) :
@[simp]
theorem Module.DualBases.lc_coeffs {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] {e : ιM} {ε : ι} [] (h : ) (m : M) :

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

@[simp]
theorem Module.DualBases.basis_repr_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] {e : ιM} {ε : ι} [] (h : ) (m : M) :
.repr m =
@[simp]
theorem Module.DualBases.basis_repr_symm_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] {e : ιM} {ε : ι} [] (h : ) (l : ι →₀ R) :
() l =
def Module.DualBases.basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] {e : ιM} {ε : ι} [] (h : ) :
Basis ι R M

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Module.DualBases.coe_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] {e : ιM} {ε : ι} [] (h : ) :
= e
theorem Module.DualBases.mem_of_mem_span {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] {e : ιM} {ε : ι} [] (h : ) {H : Set ι} {x : M} (hmem : x Submodule.span R (e '' H)) (i : ι) :
(ε i) x 0i H
theorem Module.DualBases.coe_dualBasis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] {e : ιM} {ε : ι} [] (h : ) [] :
def Submodule.dualRestrict {R : Type u} {M : Type v} [] [] [Module R M] (W : ) :

The dualRestrict 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
Instances For
theorem Submodule.dualRestrict_def {R : Type u} {M : Type v} [] [] [Module R M] (W : ) :
@[simp]
theorem Submodule.dualRestrict_apply {R : Type u} {M : Type v} [] [] [Module R M] (W : ) (φ : ) (x : W) :
() x = φ x
def Submodule.dualAnnihilator {R : Type u} {M : Type v} [] [] [Module R M] (W : ) :

The dualAnnihilator of a submodule W is the set of linear maps φ such that φ w = 0 for all w ∈ W.

Equations
Instances For
@[simp]
theorem Submodule.mem_dualAnnihilator {R : Type u} {M : Type v} [] [] [Module R M] {W : } (φ : ) :
wW, φ w = 0
theorem Submodule.dualRestrict_ker_eq_dualAnnihilator {R : Type u} {M : Type v} [] [] [Module R M] (W : ) :

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

def Submodule.dualCoannihilator {R : Type u} {M : Type v} [] [] [Module R M] (Φ : Submodule R ()) :

The dualAnnihilator of a submodule of the dual space pulled back along the evaluation map Module.Dual.eval.

Equations
Instances For
@[simp]
theorem Submodule.mem_dualCoannihilator {R : Type u} {M : Type v} [] [] [Module R M] {Φ : Submodule R ()} (x : M) :
φΦ, φ x = 0
theorem Submodule.comap_dualAnnihilator {R : Type u} {M : Type v} [] [] [Module R M] (Φ : Submodule R ()) :
theorem Submodule.map_dualCoannihilator_le {R : Type u} {M : Type v} [] [] [Module R M] (Φ : Submodule R ()) :
theorem Submodule.dualAnnihilator_gc (R : Type u) (M : Type v) [] [] [Module R M] :
GaloisConnection (OrderDual.toDual Submodule.dualAnnihilator) (Submodule.dualCoannihilator OrderDual.ofDual)
theorem Submodule.le_dualAnnihilator_iff_le_dualCoannihilator {R : Type u} {M : Type v} [] [] [Module R M] {U : Submodule R ()} {V : } :
@[simp]
theorem Submodule.dualAnnihilator_bot {R : Type u} {M : Type v} [] [] [Module R M] :
@[simp]
theorem Submodule.dualAnnihilator_top {R : Type u} {M : Type v} [] [] [Module R M] :
@[simp]
theorem Submodule.dualCoannihilator_bot {R : Type u} {M : Type v} [] [] [Module R M] :
theorem Submodule.dualAnnihilator_anti {R : Type u} {M : Type v} [] [] [Module R M] {U : } {V : } (hUV : U V) :
theorem Submodule.dualCoannihilator_anti {R : Type u} {M : Type v} [] [] [Module R M] {U : Submodule R ()} {V : Submodule R ()} (hUV : U V) :
theorem Submodule.le_dualAnnihilator_dualCoannihilator {R : Type u} {M : Type v} [] [] [Module R M] (U : ) :
theorem Submodule.le_dualCoannihilator_dualAnnihilator {R : Type u} {M : Type v} [] [] [Module R M] (U : Submodule R ()) :
theorem Submodule.dualAnnihilator_sup_eq {R : Type u} {M : Type v} [] [] [Module R M] (U : ) (V : ) :
theorem Submodule.dualCoannihilator_sup_eq {R : Type u} {M : Type v} [] [] [Module R M] (U : Submodule R ()) (V : Submodule R ()) :
theorem Submodule.dualAnnihilator_iSup_eq {R : Type u} {M : Type v} [] [] [Module R M] {ι : Type u_1} (U : ι) :
Submodule.dualAnnihilator (⨆ (i : ι), U i) = ⨅ (i : ι),
theorem Submodule.dualCoannihilator_iSup_eq {R : Type u} {M : Type v} [] [] [Module R M] {ι : Type u_1} (U : ιSubmodule R ()) :
Submodule.dualCoannihilator (⨆ (i : ι), U i) = ⨅ (i : ι),
theorem Submodule.sup_dualAnnihilator_le_inf {R : Type u} {M : Type v} [] [] [Module R M] (U : ) (V : ) :

See also Subspace.dualAnnihilator_inf_eq for vector subspaces.

theorem Submodule.iSup_dualAnnihilator_le_iInf {R : Type u} {M : Type v} [] [] [Module R M] {ι : Type u_1} (U : ι) :
⨆ (i : ι), Submodule.dualAnnihilator (⨅ (i : ι), U i)

See also Subspace.dualAnnihilator_iInf_eq for vector subspaces when ι is finite.

@[simp]
theorem Subspace.dualCoannihilator_top {K : Type u} {V : Type v} [] [] [Module K V] (W : Subspace K V) :
@[simp]
theorem Subspace.dualAnnihilator_dualCoannihilator_eq {K : Type u} {V : Type v} [] [] [Module K V] {W : Subspace K V} :
theorem Subspace.forall_mem_dualAnnihilator_apply_eq_zero_iff {K : Type u} {V : Type v} [] [] [Module K V] (W : Subspace K V) (v : V) :
(φ, φ v = 0) v W
theorem Subspace.comap_dualAnnihilator_dualAnnihilator {K : Type u} {V : Type v} [] [] [Module K V] (W : Subspace K V) :
theorem Subspace.map_le_dualAnnihilator_dualAnnihilator {K : Type u} {V : Type v} [] [] [Module K V] (W : Subspace K V) :
def Subspace.dualAnnihilatorGci (K : Type u_1) (V : Type u_2) [] [] [Module K V] :
GaloisCoinsertion (OrderDual.toDual Submodule.dualAnnihilator) (Submodule.dualCoannihilator OrderDual.ofDual)

Submodule.dualAnnihilator and Submodule.dualCoannihilator form a Galois coinsertion.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Subspace.dualAnnihilator_le_dualAnnihilator_iff {K : Type u} {V : Type v} [] [] [Module K V] {W : Subspace K V} {W' : Subspace K V} :
theorem Subspace.dualAnnihilator_inj {K : Type u} {V : Type v} [] [] [Module K V] {W : Subspace K V} {W' : Subspace K V} :
noncomputable def Subspace.dualLift {K : Type u} {V : Type v} [] [] [Module K V] (W : Subspace K V) :

Given a subspace W of V and an element of its dual φ, dualLift W φ is an arbitrary extension of φ to an element of the dual of V. That is, dualLift W φ sends w ∈ W to φ x and x in a chosen complement of W to 0.

Equations
Instances For
@[simp]
theorem Subspace.dualLift_of_subtype {K : Type u} {V : Type v} [] [] [Module K V] {W : Subspace K V} {φ : Module.Dual K W} (w : W) :
( φ) w = φ w
theorem Subspace.dualLift_of_mem {K : Type u} {V : Type v} [] [] [Module K V] {W : Subspace K V} {φ : Module.Dual K W} {w : V} (hw : w W) :
( φ) w = φ { val := w, property := hw }
@[simp]
theorem Subspace.dualRestrict_comp_dualLift {K : Type u} {V : Type v} [] [] [Module K V] (W : Subspace K V) :
theorem Subspace.dualRestrict_leftInverse {K : Type u} {V : Type v} [] [] [Module K V] (W : Subspace K V) :
theorem Subspace.dualLift_rightInverse {K : Type u} {V : Type v} [] [] [Module K V] (W : Subspace K V) :
theorem Subspace.dualRestrict_surjective {K : Type u} {V : Type v} [] [] [Module K V] {W : Subspace K V} :
theorem Subspace.dualLift_injective {K : Type u} {V : Type v} [] [] [Module K V] {W : Subspace K V} :
noncomputable def Subspace.quotAnnihilatorEquiv {K : Type u} {V : Type v} [] [] [Module K V] (W : Subspace K V) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Subspace.quotAnnihilatorEquiv_apply {K : Type u} {V : Type v} [] [] [Module K V] (W : Subspace K V) (φ : ) :
noncomputable def Subspace.dualEquivDual {K : Type u} {V : Type v} [] [] [Module K V] (W : Subspace K V) :
Module.Dual K W ≃ₗ[K]

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

Equations
Instances For
theorem Subspace.dualEquivDual_def {K : Type u} {V : Type v} [] [] [Module K V] (W : Subspace K V) :
@[simp]
theorem Subspace.dualEquivDual_apply {K : Type u} {V : Type v} [] [] [Module K V] {W : Subspace K V} (φ : Module.Dual K W) :
= { val := φ, property := }
instance Subspace.instModuleDualFiniteDimensional {K : Type u} {V : Type v} [] [] [Module K V] [] :
Equations
• =
@[simp]
theorem Subspace.dual_finrank_eq {K : Type u} {V : Type v} [] [] [Module K V] :
theorem Subspace.dualAnnihilator_dualAnnihilator_eq {K : Type u} {V : Type v} [] [] [Module K V] [] (W : Subspace K V) :
noncomputable def Subspace.quotDualEquivAnnihilator {K : Type u} {V : Type v} [] [] [Module K V] [] (W : Subspace K V) :

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

Equations
Instances For
noncomputable def Subspace.quotEquivAnnihilator {K : Type u} {V : Type v} [] [] [Module K V] [] (W : Subspace K V) :
(V W) ≃ₗ[K]

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Subspace.finrank_dualCoannihilator_eq {K : Type u} {V : Type v} [] [] [Module K V] [] {Φ : Subspace K ()} :
theorem Subspace.finrank_add_finrank_dualCoannihilator_eq {K : Type u} {V : Type v} [] [] [Module K V] [] (W : Subspace K ()) :
theorem LinearMap.ker_dualMap_eq_dualAnnihilator_range {R : Type uR} [] {M₁ : Type uM₁} {M₂ : Type uM₂} [] [Module R M₁] [] [Module R M₂] (f : M₁ →ₗ[R] M₂) :
theorem LinearMap.range_dualMap_le_dualAnnihilator_ker {R : Type uR} [] {M₁ : Type uM₁} {M₂ : Type uM₂} [] [Module R M₁] [] [Module R M₂] (f : M₁ →ₗ[R] M₂) :
def Submodule.dualCopairing {R : Type u_1} {M : Type u_2} [] [] [Module R M] (W : ) :

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

See Subspace.dualCopairing_nondegenerate.

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Submodule.dualCopairing_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] {W : } (φ : ) (x : M) :
() = φ x
def Submodule.dualPairing {R : Type u_1} {M : Type u_2} [] [] [Module R M] (W : ) :
→ₗ[R] W →ₗ[R] R

Given a submodule, restrict to the pairing on W by simultaneously corestricting to Module.Dual R M ⧸ W.dualAnnihilator. This is Submodule.dualRestrict factored through the quotient by its kernel (which is W.dualAnnihilator by definition).

See Subspace.dualPairing_nondegenerate.

Equations
Instances For
@[simp]
theorem Submodule.dualPairing_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] {W : } (φ : ) (x : W) :
() x = φ x
theorem Submodule.range_dualMap_mkQ_eq {R : Type u_1} {M : Type u_2} [] [] [Module R M] (W : ) :

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

def Submodule.dualQuotEquivDualAnnihilator {R : Type u_1} {M : Type u_2} [] [] [Module R M] (W : ) :

Equivalence $(M/W)^* \cong \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.dualCopairing.

Equations
Instances For
@[simp]
theorem Submodule.dualQuotEquivDualAnnihilator_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (W : ) (φ : Module.Dual R (M W)) (x : M) :
=
theorem Submodule.dualCopairing_eq {R : Type u_1} {M : Type u_2} [] [] [Module R M] (W : ) :
@[simp]
theorem Submodule.dualQuotEquivDualAnnihilator_symm_apply_mk {R : Type u_1} {M : Type u_2} [] [] [Module R M] (W : ) (φ : ) (x : M) :
= φ x
theorem Submodule.finite_dualAnnihilator_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] {W : } [Module.Free R (M W)] :
def Submodule.quotDualCoannihilatorToDual {R : Type u_1} {M : Type u_2} [] [] [Module R M] (W : Submodule R ()) :

The pairing between a submodule W of a dual module Dual R M and the quotient of M by the coannihilator of W, which is always nondegenerate.

Equations
Instances For
@[simp]
theorem Submodule.quotDualCoannihilatorToDual_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (W : Submodule R ()) (m : M) (w : W) :
= w m
theorem Submodule.quotDualCoannihilatorToDual_injective {R : Type u_1} {M : Type u_2} [] [] [Module R M] (W : Submodule R ()) :
theorem Submodule.flip_quotDualCoannihilatorToDual_injective {R : Type u_1} {M : Type u_2} [] [] [Module R M] (W : Submodule R ()) :
theorem Submodule.quotDualCoannihilatorToDual_nondegenerate {R : Type u_1} {M : Type u_2} [] [] [Module R M] (W : Submodule R ()) :
theorem LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_surjective {R : Type u_1} {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [] [Module R M'] (f : M →ₗ[R] M') (hf : ) :
theorem LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective {R : Type u_1} {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [] [Module R M'] (f : M →ₗ[R] M') (hf : ) :
theorem LinearMap.ker_dualMap_eq_dualCoannihilator_range {R : Type u_1} {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [] [Module R M'] (f : M →ₗ[R] M') :
@[simp]
theorem LinearMap.dualCoannihilator_range_eq_ker_flip {R : Type u_1} {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [] [Module R M'] (B : M →ₗ[R] M' →ₗ[R] R) :
theorem Module.Dual.range_eq_top_of_ne_zero {K : Type uK} [] {V₁ : Type uV₁} [] [Module K V₁] {f : Module.Dual K V₁} (hf : f 0) :
theorem Module.Dual.finrank_ker_add_one_of_ne_zero {K : Type uK} [] {V₁ : Type uV₁} [] [Module K V₁] [] {f : Module.Dual K V₁} (hf : f 0) :
theorem Module.Dual.isCompl_ker_of_disjoint_of_ne_bot {K : Type uK} [] {V₁ : Type uV₁} [] [Module K V₁] [] {f : Module.Dual K V₁} (hf : f 0) {p : Submodule K V₁} (hpf : ) (hp : p ) :
IsCompl () p
theorem LinearMap.dualPairing_nondegenerate {K : Type uK} [] {V₁ : Type uV₁} [] [Module K V₁] :
theorem LinearMap.dualMap_surjective_of_injective {K : Type uK} [] {V₁ : Type uV₁} {V₂ : Type uV₂} [] [Module K V₁] [] [Module K V₂] {f : V₁ →ₗ[K] V₂} (hf : ) :
theorem LinearMap.range_dualMap_eq_dualAnnihilator_ker {K : Type uK} [] {V₁ : Type uV₁} {V₂ : Type uV₂} [] [Module K V₁] [] [Module K V₂] (f : V₁ →ₗ[K] V₂) :
@[simp]
theorem LinearMap.dualMap_surjective_iff {K : Type uK} [] {V₁ : Type uV₁} {V₂ : Type uV₂} [] [Module K V₁] [] [Module K V₂] {f : V₁ →ₗ[K] V₂} :

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

theorem Subspace.dualPairing_eq {K : Type uK} [] {V₁ : Type uV₁} [] [Module K V₁] (W : Subspace K V₁) :
theorem Subspace.dualPairing_nondegenerate {K : Type uK} [] {V₁ : Type uV₁} [] [Module K V₁] (W : Subspace K V₁) :
theorem Subspace.dualCopairing_nondegenerate {K : Type uK} [] {V₁ : Type uV₁} [] [Module K V₁] (W : Subspace K V₁) :
theorem Subspace.dualAnnihilator_inf_eq {K : Type uK} [] {V₁ : Type uV₁} [] [Module K V₁] (W : Subspace K V₁) (W' : Subspace K V₁) :
theorem Subspace.dualAnnihilator_iInf_eq {K : Type uK} [] {V₁ : Type uV₁} [] [Module K V₁] {ι : Type u_1} [] (W : ιSubspace K V₁) :
Submodule.dualAnnihilator (⨅ (i : ι), W i) = ⨆ (i : ι),
theorem Subspace.isCompl_dualAnnihilator {K : Type uK} [] {V₁ : Type uV₁} [] [Module K V₁] {W : Subspace K V₁} {W' : Subspace K V₁} (h : IsCompl W W') :

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

def Subspace.dualQuotDistrib {K : Type uK} [] {V₁ : Type uV₁} [] [Module K V₁] [] (W : Subspace K V₁) :
Module.Dual K (V₁ W) ≃ₗ[K]

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

Equations
Instances For
@[simp]
theorem LinearMap.finrank_range_dualMap_eq_finrank_range {K : Type uK} [] {V₁ : Type uV₁} {V₂ : Type uV₂} [] [Module K V₁] [] [Module K V₂] (f : V₁ →ₗ[K] V₂) :
@[simp]
theorem LinearMap.dualMap_injective_iff {K : Type uK} [] {V₁ : Type uV₁} {V₂ : Type uV₂} [] [Module K V₁] [] [Module K V₂] {f : V₁ →ₗ[K] V₂} :

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

@[simp]
theorem LinearMap.dualMap_bijective_iff {K : Type uK} [] {V₁ : Type uV₁} {V₂ : Type uV₂} [] [Module K V₁] [] [Module K V₂] {f : V₁ →ₗ[K] V₂} :

f.dualMap is bijective if and only if f is

@[simp]
theorem LinearMap.dualAnnihilator_ker_eq_range_flip {K : Type uK} [] {V₁ : Type uV₁} {V₂ : Type uV₂} [] [Module K V₁] [] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [] :
theorem LinearMap.flip_injective_iff₁ {K : Type uK} [] {V₁ : Type uV₁} {V₂ : Type uV₂} [] [Module K V₁] [] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [] :
theorem LinearMap.flip_injective_iff₂ {K : Type uK} [] {V₁ : Type uV₁} {V₂ : Type uV₂} [] [Module K V₁] [] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [] :
theorem LinearMap.flip_surjective_iff₁ {K : Type uK} [] {V₁ : Type uV₁} {V₂ : Type uV₂} [] [Module K V₁] [] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [] :
theorem LinearMap.flip_surjective_iff₂ {K : Type uK} [] {V₁ : Type uV₁} {V₂ : Type uV₂} [] [Module K V₁] [] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [] :
theorem LinearMap.flip_bijective_iff₁ {K : Type uK} [] {V₁ : Type uV₁} {V₂ : Type uV₂} [] [Module K V₁] [] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [] :
theorem LinearMap.flip_bijective_iff₂ {K : Type uK} [] {V₁ : Type uV₁} {V₂ : Type uV₂} [] [Module K V₁] [] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [] :
theorem Subspace.quotDualCoannihilatorToDual_bijective {K : Type u_1} {V : Type u_2} [] [] [Module K V] (W : Subspace K ()) [] :
theorem Subspace.flip_quotDualCoannihilatorToDual_bijective {K : Type u_1} {V : Type u_2} [] [] [Module K V] (W : Subspace K ()) [] :
theorem Subspace.dualCoannihilator_dualAnnihilator_eq {K : Type u_1} {V : Type u_2} [] [] [Module K V] {W : Subspace K ()} [] :
theorem Subspace.finiteDimensional_quot_dualCoannihilator_iff {K : Type u_1} {V : Type u_2} [] [] [Module K V] {W : Submodule K ()} :
def Subspace.orderIsoFiniteCodimDim {K : Type u_1} {V : Type u_2} [] [] [Module K V] :
{ W : Subspace K V // FiniteDimensional K (V W) } ≃o { W : Subspace K () // }ᵒᵈ

For any vector space, dualAnnihilator and dualCoannihilator gives an antitone order isomorphism between the finite-codimensional subspaces in the vector space and the finite-dimensional subspaces in its dual.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Subspace.orderIsoFiniteDimensional {K : Type u_1} {V : Type u_2} [] [] [Module K V] [] :

For any finite-dimensional vector space, dualAnnihilator and dualCoannihilator give an antitone order isomorphism between the subspaces in the vector space and the subspaces in its dual.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Subspace.dualAnnihilator_dualAnnihilator_eq_map {K : Type u_1} {V : Type u_2} [] [] [Module K V] (W : Subspace K V) [] :
theorem Subspace.map_dualCoannihilator {K : Type u_1} {V : Type u_2} [] [] [Module K V] (W : Subspace K ()) [] :
def TensorProduct.dualDistrib (R : Type u_1) (M : Type u_3) (N : Type u_4) [] [] [] [Module R M] [Module R N] :

The canonical linear map from Dual M ⊗ Dual N to Dual (M ⊗ N), sending f ⊗ g to the composition of TensorProduct.map f g with the natural isomorphism R ⊗ R ≃ R.

Equations
• = ∘ₗ
Instances For
@[simp]
theorem TensorProduct.dualDistrib_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} [] [] [] [Module R M] [Module R N] (f : ) (g : ) (m : M) (n : N) :
(() (f ⊗ₜ[R] g)) (m ⊗ₜ[R] n) = f m * g n
def TensorProduct.AlgebraTensorModule.dualDistrib (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) [] [] [Algebra R A] [] [] [Module R M] [Module A M] [Module R N] [] :

Heterobasic version of TensorProduct.dualDistrib

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TensorProduct.AlgebraTensorModule.dualDistrib_apply {R : Type u_1} (A : Type u_2) {M : Type u_3} {N : Type u_4} [] [] [Algebra R A] [] [] [Module R M] [Module A M] [Module R N] [] (f : ) (g : ) (m : M) (n : N) :
( (f ⊗ₜ[R] g)) (m ⊗ₜ[R] n) = g n f m
noncomputable def TensorProduct.dualDistribInvOfBasis {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [] [] [] [] [] [] [] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) :

An inverse to TensorProduct.dualDistrib given bases.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TensorProduct.dualDistribInvOfBasis_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [] [] [] [] [] [] [] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) (f : Module.Dual R ()) :
= Finset.sum Finset.univ fun (i : ι) => Finset.sum Finset.univ fun (j : κ) => f (b i ⊗ₜ[R] c j) () i ⊗ₜ[R] () j
theorem TensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [] [] [] [] [] [] [] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) :
= LinearMap.id
theorem TensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [] [] [] [] [] [] [] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) :
= LinearMap.id
@[simp]
theorem TensorProduct.dualDistribEquivOfBasis_apply_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [] [] [] [] [] [] [] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) :
∀ (a : TensorProduct R () ()) (a_1 : ), () a_1 = () ((() a) a_1)
@[simp]
theorem TensorProduct.dualDistribEquivOfBasis_symm_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [] [] [] [] [] [] [] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) (a : Module.Dual R ()) :
= Finset.sum Finset.univ fun (x : ι) => Finset.sum Finset.univ fun (x_1 : κ) => a (b x ⊗ₜ[R] c x_1) ⊗ₜ[R] Basis.coord c x_1
noncomputable def TensorProduct.dualDistribEquivOfBasis {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [] [] [] [] [] [] [] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) :

A linear equivalence between Dual M ⊗ Dual N and Dual (M ⊗ N) given bases for M and N. It sends f ⊗ g to the composition of TensorProduct.map f g with the natural isomorphism R ⊗ R ≃ R.

Equations
Instances For
noncomputable def TensorProduct.dualDistribEquiv (R : Type u_1) (M : Type u_3) (N : Type u_4) [] [] [] [Module R M] [Module R 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 TensorProduct.map f g with the natural isomorphism R ⊗ R ≃ R.

Equations
Instances For