Dual vector spaces

The dual space of an $R$-module $M$ is the $R$-module of $R$-linear maps $M \to R$. This file contains basic results on dual vector spaces.

Main definitions

• Submodules:
  • 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).
• Vector spaces:
  • Subspace.dualLift W is an arbitrary section (using choice) of Submodule.dualRestrict W.

Main results

• Annihilators:
  • 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_dualCoannihilator_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:
  • 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₁.

def Module.dualProdDualEquivDual (R : Type u_1) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] (M' : Type u_4) [AddCommMonoid M'] [Module R M'] : (Dual R M × Dual R M') ≃ₗ[R] Dual R (M × M')

Taking duals distributes over products.

Equations

• Module.dualProdDualEquivDual R M M' = LinearMap.coprodEquiv R

@[simp]

theorem Module.dualProdDualEquivDual_symm_apply (R : Type u_1) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] (M' : Type u_4) [AddCommMonoid M'] [Module R M'] (f : M × M' →ₗ[R] R) : (dualProdDualEquivDual R M M').symm f = (f ∘ₗ LinearMap.inl R M M', f ∘ₗ LinearMap.inr R M M')

@[simp]

theorem Module.dualProdDualEquivDual_apply_apply (R : Type u_1) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] (M' : Type u_4) [AddCommMonoid M'] [Module R M'] (f : (M →ₗ[R] R) × (M' →ₗ[R] R)) (a : M × M') : ((dualProdDualEquivDual R M M') f) a = f.1 a.1 + f.2 a.2

@[simp]

theorem Module.dualProdDualEquivDual_apply (R : Type u_1) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] (M' : Type u_4) [AddCommMonoid M'] [Module R M'] (φ : Dual R M) (ψ : Dual R M') : (dualProdDualEquivDual R M M') (φ, ψ) = LinearMap.coprod φ ψ

theorem Basis.linearEquiv_dual_iff_finiteDimensional {K : Type uK} {V : Type uV} [Field K] [AddCommGroup V] [Module K V] : Nonempty (V ≃ₗ[K] Module.Dual K V) ↔ FiniteDimensional 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.

theorem Module.Basis.dual_rank_eq {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [Finite ι] (b : Basis ι R M) : Module.rank R (Dual R M) = Cardinal.lift.{uR, uM} (Module.rank R M)

instance Module.dual_free {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Free R M] : Free R (Dual R M)

instance Module.dual_projective {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Projective R M] : Projective R (Dual R M)

instance Module.dual_finite {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Projective R M] : Module.Finite R (Dual R M)

@[deprecated Module.dual_free (since := "2025-04-11")]

theorem Basis.dual_free {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Module.Free R M] : Module.Free R (Module.Dual R M)

Alias of Module.dual_free.

@[deprecated Module.dual_projective (since := "2025-04-11")]

theorem Basis.dual_projective {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Module.Projective R (Module.Dual R M)

Alias of Module.dual_projective.

@[deprecated Module.dual_finite (since := "2025-04-11")]

theorem Basis.dual_finite {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Module.Finite R (Module.Dual R M)

Alias of Module.dual_finite.

theorem Module.eval_apply_injective (K : Type uK) {V : Type uV} [CommSemiring K] [AddCommMonoid V] [Module K V] [Projective K V] : Function.Injective ⇑(Dual.eval K V)

theorem Module.eval_ker (K : Type uK) (V : Type uV) [CommSemiring K] [AddCommMonoid V] [Module K V] [Projective K V] : LinearMap.ker (Dual.eval K V) = ⊥

theorem Module.map_eval_injective (K : Type uK) (V : Type uV) [CommSemiring K] [AddCommMonoid V] [Module K V] [Projective K V] : Function.Injective (Submodule.map (Dual.eval K V))

theorem Module.comap_eval_surjective (K : Type uK) (V : Type uV) [CommSemiring K] [AddCommMonoid V] [Module K V] [Projective K V] : Function.Surjective (Submodule.comap (Dual.eval K V))

theorem Module.eval_apply_eq_zero_iff (K : Type uK) {V : Type uV} [CommSemiring K] [AddCommMonoid V] [Module K V] [Projective K V] (v : V) : (Dual.eval K V) v = 0 ↔ v = 0

theorem Module.forall_dual_apply_eq_zero_iff (K : Type uK) {V : Type uV} [CommSemiring K] [AddCommMonoid V] [Module K V] [Projective K V] (v : V) : (∀ (φ : Dual K V), φ v = 0) ↔ v = 0

@[simp]

theorem Module.subsingleton_dual_iff (K : Type uK) {V : Type uV} [CommSemiring K] [AddCommMonoid V] [Module K V] [Projective K V] : Subsingleton (Dual K V) ↔ Subsingleton V

@[simp]

theorem Module.nontrivial_dual_iff (K : Type uK) {V : Type uV} [CommSemiring K] [AddCommMonoid V] [Module K V] [Projective K V] : Nontrivial (Dual K V) ↔ Nontrivial V

instance Module.instNontrivialDual (K : Type uK) {V : Type uV} [CommSemiring K] [AddCommMonoid V] [Module K V] [Projective K V] [Nontrivial V] : Nontrivial (Dual K V)

theorem Module.finite_dual_iff (K : Type uK) {V : Type uV} [CommSemiring K] [AddCommMonoid V] [Module K V] [Free K V] : Module.Finite K (Dual K V) ↔ Module.Finite K V

For an example of a non-free projective K-module V for which the forward implication fails, see https://stacks.math.columbia.edu/tag/05WG#comment-9913.

theorem Module.dual_rank_eq {K : Type uK} {V : Type uV} [CommSemiring K] [AddCommMonoid V] [Module K V] [Free K V] [Module.Finite K V] : Module.rank K (Dual K V) = Cardinal.lift.{uK, uV} (Module.rank K V)

@[instance 900]

instance Module.IsReflexive.of_finite_of_free (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Free R M] : IsReflexive R M

See also Module.instFiniteDimensionalOfIsReflexive for the converse over a field.

@[instance 900]

instance Module.instIsReflexiveOfFiniteOfProjective (R : Type u_1) (N : Type u_3) [CommSemiring R] [AddCommMonoid N] [Module R N] [Module.Finite R N] [Projective R N] : IsReflexive R N

instance Prod.instModuleIsReflexive (R : Type u_1) (M : Type u_2) (N : Type u_3) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.IsReflexive R M] [Module.IsReflexive R N] : Module.IsReflexive R (M × N)

instance ULift.instModuleIsReflexive (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.IsReflexive R M] : Module.IsReflexive R (ULift.{w, u_2} M)

instance Module.instFiniteDimensionalOfIsReflexive (K : Type u_4) (V : Type u_5) [Field K] [AddCommGroup V] [Module K V] [IsReflexive K V] : FiniteDimensional K V

@[simp]

theorem Submodule.dualCoannihilator_top {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Projective R M] : ⊤.dualCoannihilator = ⊥

theorem Submodule.exists_dual_map_eq_bot_of_notMem {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : Submodule R M} {x : M} (hx : x ∉ p) (hp' : Module.Free R (M ⧸ p)) : ∃ (f : Module.Dual R M), f x ≠ 0 ∧ map f p = ⊥

@[deprecated Submodule.exists_dual_map_eq_bot_of_notMem (since := "2025-05-24")]

theorem Submodule.exists_dual_map_eq_bot_of_nmem {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : Submodule R M} {x : M} (hx : x ∉ p) (hp' : Module.Free R (M ⧸ p)) : ∃ (f : Module.Dual R M), f x ≠ 0 ∧ map f p = ⊥

Alias of Submodule.exists_dual_map_eq_bot_of_notMem.

theorem Submodule.exists_dual_map_eq_bot_of_lt_top {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : Submodule R M} (hp : p < ⊤) (hp' : Module.Free R (M ⧸ p)) : ∃ (f : Module.Dual R M), f ≠ 0 ∧ map f p = ⊥

theorem Submodule.span_eq_top_of_ne_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] {s : Set (M →ₗ[R] R)} [Module.Free R ((M →ₗ[R] R) ⧸ span R s)] (h : ∀ (z : M), z ≠ 0 → ∃ f ∈ s, f z ≠ 0) : span R s = ⊤

Consider a reflexive module and a set s of linear forms. If for any z ≠ 0 there exists f ∈ s such that f z ≠ 0, then s spans the whole dual space.

theorem FiniteDimensional.mem_span_of_iInf_ker_le_ker {ι : Type u_3} {𝕜 : Type u_4} {E : Type u_5} [Field 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] {L : ι → E →ₗ[𝕜] 𝕜} {K : E →ₗ[𝕜] 𝕜} (h : ⨅ (i : ι), LinearMap.ker (L i) ≤ LinearMap.ker K) : K ∈ Submodule.span 𝕜 (Set.range L)

theorem mem_span_of_iInf_ker_le_ker {ι : Type u_3} {𝕜 : Type u_4} {E : Type u_5} [Field 𝕜] [AddCommGroup E] [Module 𝕜 E] [Finite ι] {L : ι → E →ₗ[𝕜] 𝕜} {K : E →ₗ[𝕜] 𝕜} (h : ⨅ (i : ι), LinearMap.ker (L i) ≤ LinearMap.ker K) : K ∈ Submodule.span 𝕜 (Set.range L)

Given some linear forms $L_1, ..., L_n, K$ over a vector space $E$, if $\bigcap_{i=1}^n \mathrm{ker}(L_i) \subseteq \mathrm{ker}(K)$, then $K$ is in the space generated by $L_1, ..., L_n$.

@[simp]

theorem Subspace.dualAnnihilator_dualCoannihilator_eq {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K V} : (Submodule.dualAnnihilator W).dualCoannihilator = W

theorem Subspace.forall_mem_dualAnnihilator_apply_eq_zero_iff {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) (v : V) : (∀ φ ∈ Submodule.dualAnnihilator W, φ v = 0) ↔ v ∈ W

theorem Subspace.comap_dualAnnihilator_dualAnnihilator {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) : Submodule.comap (Module.Dual.eval K V) (Submodule.dualAnnihilator W).dualAnnihilator = W

theorem Subspace.map_le_dualAnnihilator_dualAnnihilator {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) : Submodule.map (Module.Dual.eval K V) W ≤ (Submodule.dualAnnihilator W).dualAnnihilator

def Subspace.dualAnnihilatorGci (K : Type u_3) (V : Type u_4) [Field K] [AddCommGroup V] [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.

theorem Subspace.dualAnnihilator_le_dualAnnihilator_iff {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {W W' : Subspace K V} : Submodule.dualAnnihilator W ≤ Submodule.dualAnnihilator W' ↔ W' ≤ W

theorem Subspace.dualAnnihilator_inj {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {W W' : Subspace K V} : Submodule.dualAnnihilator W = Submodule.dualAnnihilator W' ↔ W = W'

noncomputable def Subspace.dualLift {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup 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 φ, 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

• W.dualLift = (Classical.choose ⋯).dualMap

@[simp]

theorem Subspace.dualLift_of_subtype {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K V} {φ : Module.Dual K ↥W} (w : ↥W) : (W.dualLift φ) ↑w = φ w

theorem Subspace.dualLift_of_mem {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K V} {φ : Module.Dual K ↥W} {w : V} (hw : w ∈ W) : (W.dualLift φ) w = φ ⟨w, hw⟩

@[simp]

theorem Subspace.dualRestrict_comp_dualLift {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) : Submodule.dualRestrict W ∘ₗ W.dualLift = 1

theorem Subspace.dualRestrict_leftInverse {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) : Function.LeftInverse ⇑(Submodule.dualRestrict W) ⇑W.dualLift

theorem Subspace.dualLift_rightInverse {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) : Function.RightInverse ⇑W.dualLift ⇑(Submodule.dualRestrict W)

theorem Subspace.dualRestrict_surjective {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K V} : Function.Surjective ⇑(Submodule.dualRestrict W)

theorem Subspace.dualLift_injective {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K V} : Function.Injective ⇑W.dualLift

noncomputable def Subspace.quotAnnihilatorEquiv {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) : (Module.Dual K V ⧸ Submodule.dualAnnihilator W) ≃ₗ[K] Module.Dual K ↥W

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

Equations

• W.quotAnnihilatorEquiv = ((LinearMap.ker (Submodule.dualRestrict W)).quotEquivOfEq (Submodule.dualAnnihilator W) ⋯).symm.trans ((Submodule.dualRestrict W).quotKerEquivOfSurjective ⋯)

@[simp]

theorem Subspace.quotAnnihilatorEquiv_apply {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) (φ : Module.Dual K V) : W.quotAnnihilatorEquiv (Submodule.Quotient.mk φ) = (Submodule.dualRestrict W) φ

noncomputable def Subspace.dualEquivDual {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) : Module.Dual K ↥W ≃ₗ[K] ↥(LinearMap.range W.dualLift)

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

Equations

• W.dualEquivDual = LinearEquiv.ofInjective W.dualLift ⋯

theorem Subspace.dualEquivDual_def {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) : ↑W.dualEquivDual = W.dualLift.rangeRestrict

@[simp]

theorem Subspace.dualEquivDual_apply {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K V} (φ : Module.Dual K ↥W) : W.dualEquivDual φ = ⟨W.dualLift φ, ⋯⟩

instance Subspace.instModuleDualFiniteDimensional {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : FiniteDimensional K (Module.Dual K V)

@[simp]

theorem Subspace.dual_finrank_eq {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : Module.finrank K (Module.Dual K V) = Module.finrank K V

theorem Subspace.dualAnnihilator_dualAnnihilator_eq {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (W : Subspace K V) : (Submodule.dualAnnihilator W).dualAnnihilator = (Module.mapEvalEquiv K V) W

noncomputable def Subspace.quotDualEquivAnnihilator {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (W : Subspace K V) : (Module.Dual K V ⧸ LinearMap.range W.dualLift) ≃ₗ[K] ↥(Submodule.dualAnnihilator W)

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

Equations

• W.quotDualEquivAnnihilator = FiniteDimensional.LinearEquiv.quotEquivOfQuotEquiv (W.quotAnnihilatorEquiv.trans W.dualEquivDual)

noncomputable def Subspace.quotEquivAnnihilator {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (W : Subspace K V) : (V ⧸ W) ≃ₗ[K] ↥(Submodule.dualAnnihilator W)

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

Equations

• One or more equations did not get rendered due to their size.

theorem Subspace.finrank_add_finrank_dualAnnihilator_eq {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (W : Subspace K V) : Module.finrank K ↥W + Module.finrank K ↥(Submodule.dualAnnihilator W) = Module.finrank K V

@[simp]

theorem Subspace.finrank_dualCoannihilator_eq {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Φ : Subspace K (Module.Dual K V)} : Module.finrank K ↥(Submodule.dualCoannihilator Φ) = Module.finrank K ↥(Submodule.dualAnnihilator Φ)

theorem Subspace.finrank_add_finrank_dualCoannihilator_eq {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (W : Subspace K (Module.Dual K V)) : Module.finrank K ↥W + Module.finrank K ↥(Submodule.dualCoannihilator W) = Module.finrank K V

def Submodule.dualCopairing {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) : ↥W.dualAnnihilator →ₗ[R] M ⧸ W →ₗ[R] R

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

See Subspace.dualCopairing_nondegenerate.

Equations

• W.dualCopairing = (W.liftQ ((Module.dualPairing R M).domRestrict W.dualAnnihilator).flip ⋯).flip

instance Submodule.instFunLikeSubtypeDualMemDualAnnihilator {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) : FunLike (↥W.dualAnnihilator) M R

Equations

• W.instFunLikeSubtypeDualMemDualAnnihilator = { coe := fun (φ : ↥W.dualAnnihilator) => ⇑↑φ, coe_injective' := ⋯ }

@[simp]

theorem Submodule.dualCopairing_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {W : Submodule R M} (φ : ↥W.dualAnnihilator) (x : M) : (W.dualCopairing φ) (Quotient.mk x) = φ x

def Submodule.dualPairing {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) : Module.Dual R M ⧸ W.dualAnnihilator →ₗ[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

• W.dualPairing = W.dualAnnihilator.liftQ W.dualRestrict ⋯

@[simp]

theorem Submodule.dualPairing_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {W : Submodule R M} (φ : Module.Dual R M) (x : ↥W) : (W.dualPairing (Quotient.mk φ)) x = φ ↑x

theorem Submodule.range_dualMap_mkQ_eq {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) : LinearMap.range W.mkQ.dualMap = W.dualAnnihilator

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

def Submodule.dualQuotEquivDualAnnihilator {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) : Module.Dual R (M ⧸ W) ≃ₗ[R] ↥W.dualAnnihilator

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

• W.dualQuotEquivDualAnnihilator = LinearEquiv.ofLinear (LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap ⋯) W.dualCopairing ⋯ ⋯

@[simp]

theorem Submodule.dualQuotEquivDualAnnihilator_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) (φ : Module.Dual R (M ⧸ W)) (x : M) : (W.dualQuotEquivDualAnnihilator φ) x = φ (Quotient.mk x)

theorem Submodule.dualCopairing_eq {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) : W.dualCopairing = ↑W.dualQuotEquivDualAnnihilator.symm

@[simp]

theorem Submodule.dualQuotEquivDualAnnihilator_symm_apply_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) (φ : ↥W.dualAnnihilator) (x : M) : (W.dualQuotEquivDualAnnihilator.symm φ) (Quotient.mk x) = φ x

theorem Submodule.finite_dualAnnihilator_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {W : Submodule R M} [Module.Free R (M ⧸ W)] : Module.Finite R ↥W.dualAnnihilator ↔ Module.Finite R (M ⧸ W)

theorem Submodule.dualAnnihilator_eq_bot_iff' {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {W : Submodule R M} : W.dualAnnihilator = ⊥ ↔ Subsingleton (Module.Dual R (M ⧸ W))

@[simp]

theorem Submodule.dualAnnihilator_eq_bot_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {W : Submodule R M} [Module.Projective R (M ⧸ W)] : W.dualAnnihilator = ⊥ ↔ W = ⊤

@[simp]

theorem Submodule.dualAnnihilator_eq_top_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {W : Submodule R M} [Module.Projective R M] : W.dualAnnihilator = ⊤ ↔ W = ⊥

def Submodule.quotDualCoannihilatorToDual {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R (Module.Dual R M)) : M ⧸ W.dualCoannihilator →ₗ[R] Module.Dual R ↥W

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

• W.quotDualCoannihilatorToDual = W.dualCoannihilator.liftQ W.subtype.flip ⋯

@[simp]

theorem Submodule.quotDualCoannihilatorToDual_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R (Module.Dual R M)) (m : M) (w : ↥W) : (W.quotDualCoannihilatorToDual (Quotient.mk m)) w = ↑w m

theorem Submodule.quotDualCoannihilatorToDual_injective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R (Module.Dual R M)) : Function.Injective ⇑W.quotDualCoannihilatorToDual

theorem Submodule.flip_quotDualCoannihilatorToDual_injective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R (Module.Dual R M)) : Function.Injective ⇑W.quotDualCoannihilatorToDual.flip

theorem Submodule.quotDualCoannihilatorToDual_nondegenerate {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R (Module.Dual R M)) : W.quotDualCoannihilatorToDual.Nondegenerate

theorem LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_surjective {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (hf : Function.Surjective ⇑f) : range f.dualMap = (ker f).dualAnnihilator

theorem LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (hf : Function.Surjective ⇑(range f).subtype.dualMap) : range f.dualMap = (ker f).dualAnnihilator

theorem Module.Dual.range_eq_top_of_ne_zero {K : Type u_4} {V₁ : Type u_5} [Semifield K] [AddCommMonoid V₁] [Module K V₁] {f : Dual K V₁} (hf : f ≠ 0) : LinearMap.range f = ⊤

theorem Module.Dual.finrank_ker_add_one_of_ne_zero {K : Type u_1} {V₁ : Type u_2} [Field K] [AddCommGroup V₁] [Module K V₁] {f : Dual K V₁} (hf : f ≠ 0) [FiniteDimensional K V₁] : finrank K ↥(LinearMap.ker f) + 1 = finrank K V₁

theorem Module.Dual.isCompl_ker_of_disjoint_of_ne_bot {K : Type u_1} {V₁ : Type u_2} [Field K] [AddCommGroup V₁] [Module K V₁] {f : Dual K V₁} (hf : f ≠ 0) [FiniteDimensional K V₁] {p : Submodule K V₁} (hpf : Disjoint (LinearMap.ker f) p) (hp : p ≠ ⊥) : IsCompl (LinearMap.ker f) p

theorem Module.Dual.eq_of_ker_eq_of_apply_eq {K : Type u_1} {V₁ : Type u_2} [Field K] [AddCommGroup V₁] [Module K V₁] [FiniteDimensional K V₁] {f g : Dual K V₁} (x : V₁) (h : LinearMap.ker f = LinearMap.ker g) (h' : f x = g x) (hx : f x ≠ 0) : f = g

theorem LinearMap.dualPairing_nondegenerate {K : Type u_1} {V₁ : Type u_2} [Field K] [AddCommGroup V₁] [Module K V₁] : (Module.dualPairing K V₁).Nondegenerate

theorem LinearMap.dualMap_surjective_of_injective {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {f : V₁ →ₗ[K] V₂} (hf : Function.Injective ⇑f) : Function.Surjective ⇑f.dualMap

theorem LinearMap.range_dualMap_eq_dualAnnihilator_ker {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] (f : V₁ →ₗ[K] V₂) : range f.dualMap = (ker f).dualAnnihilator

@[simp]

theorem LinearMap.dualMap_surjective_iff {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {f : V₁ →ₗ[K] V₂} : Function.Surjective ⇑f.dualMap ↔ Function.Injective ⇑f

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

theorem Subspace.dualPairing_eq {K : Type u_1} {V₁ : Type u_2} [Field K] [AddCommGroup V₁] [Module K V₁] (W : Subspace K V₁) : Submodule.dualPairing W = ↑W.quotAnnihilatorEquiv

theorem Subspace.dualPairing_nondegenerate {K : Type u_1} {V₁ : Type u_2} [Field K] [AddCommGroup V₁] [Module K V₁] (W : Subspace K V₁) : (Submodule.dualPairing W).Nondegenerate

theorem Subspace.dualCopairing_nondegenerate {K : Type u_1} {V₁ : Type u_2} [Field K] [AddCommGroup V₁] [Module K V₁] (W : Subspace K V₁) : (Submodule.dualCopairing W).Nondegenerate

theorem Subspace.dualAnnihilator_inf_eq {K : Type u_1} {V₁ : Type u_2} [Field K] [AddCommGroup V₁] [Module K V₁] (W W' : Subspace K V₁) : Submodule.dualAnnihilator (W ⊓ W') = Submodule.dualAnnihilator W ⊔ Submodule.dualAnnihilator W'

theorem Subspace.dualAnnihilator_iInf_eq {K : Type u_1} {V₁ : Type u_2} [Field K] [AddCommGroup V₁] [Module K V₁] {ι : Type u_4} [Finite ι] (W : ι → Subspace K V₁) : Submodule.dualAnnihilator (⨅ (i : ι), W i) = ⨆ (i : ι), Submodule.dualAnnihilator (W i)

theorem Subspace.isCompl_dualAnnihilator {K : Type u_1} {V₁ : Type u_2} [Field K] [AddCommGroup V₁] [Module K V₁] {W W' : Subspace K V₁} (h : IsCompl W W') : IsCompl (Submodule.dualAnnihilator W) (Submodule.dualAnnihilator W')

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

def Subspace.dualQuotDistrib {K : Type u_1} {V₁ : Type u_2} [Field K] [AddCommGroup V₁] [Module K V₁] [FiniteDimensional K V₁] (W : Subspace K V₁) : Module.Dual K (V₁ ⧸ W) ≃ₗ[K] Module.Dual K V₁ ⧸ LinearMap.range W.dualLift

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

• W.dualQuotDistrib = (Submodule.dualQuotEquivDualAnnihilator W).trans W.quotDualEquivAnnihilator.symm

@[simp]

theorem LinearMap.finrank_range_dualMap_eq_finrank_range {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] (f : V₁ →ₗ[K] V₂) : Module.finrank K ↥(range f.dualMap) = Module.finrank K ↥(range f)

@[simp]

theorem LinearMap.dualMap_injective_iff {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {f : V₁ →ₗ[K] V₂} : Function.Injective ⇑f.dualMap ↔ Function.Surjective ⇑f

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

@[simp]

theorem LinearMap.dualMap_bijective_iff {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {f : V₁ →ₗ[K] V₂} : Function.Bijective ⇑f.dualMap ↔ Function.Bijective ⇑f

f.dualMap is bijective if and only if f is

@[simp]

theorem LinearMap.dualAnnihilator_ker_eq_range_flip {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [Module.IsReflexive K V₂] : (ker B).dualAnnihilator = range B.flip

theorem LinearMap.flip_injective_iff₁ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₁] : Function.Injective ⇑B.flip ↔ Function.Surjective ⇑B

theorem LinearMap.flip_injective_iff₂ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₂] : Function.Injective ⇑B.flip ↔ Function.Surjective ⇑B

theorem LinearMap.flip_surjective_iff₁ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₁] : Function.Surjective ⇑B.flip ↔ Function.Injective ⇑B

theorem LinearMap.flip_surjective_iff₂ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₂] : Function.Surjective ⇑B.flip ↔ Function.Injective ⇑B

theorem LinearMap.flip_bijective_iff₁ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₁] : Function.Bijective ⇑B.flip ↔ Function.Bijective ⇑B

theorem LinearMap.flip_bijective_iff₂ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₂] : Function.Bijective ⇑B.flip ↔ Function.Bijective ⇑B

theorem Subspace.quotDualCoannihilatorToDual_bijective {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K (Module.Dual K V)) [FiniteDimensional K ↥W] : Function.Bijective ⇑(Submodule.quotDualCoannihilatorToDual W)

theorem Subspace.flip_quotDualCoannihilatorToDual_bijective {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K (Module.Dual K V)) [FiniteDimensional K ↥W] : Function.Bijective ⇑(Submodule.quotDualCoannihilatorToDual W).flip

theorem Subspace.dualCoannihilator_dualAnnihilator_eq {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K (Module.Dual K V)} [FiniteDimensional K ↥W] : (Submodule.dualCoannihilator W).dualAnnihilator = W

theorem Subspace.finiteDimensional_quot_dualCoannihilator_iff {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] {W : Submodule K (Module.Dual K V)} : FiniteDimensional K (V ⧸ W.dualCoannihilator) ↔ FiniteDimensional K ↥W

def Subspace.orderIsoFiniteCodimDim {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] : { W : Subspace K V // FiniteDimensional K (V ⧸ W) } ≃o { W : Subspace K (Module.Dual K V) // FiniteDimensional K ↥W }ᵒᵈ

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.

def Subspace.orderIsoFiniteDimensional {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : Subspace K V ≃o (Subspace K (Module.Dual 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.

theorem Subspace.dualAnnihilator_dualAnnihilator_eq_map {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) [FiniteDimensional K ↥W] : (Submodule.dualAnnihilator W).dualAnnihilator = Submodule.map (Module.Dual.eval K V) W

theorem Subspace.map_dualCoannihilator {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K (Module.Dual K V)) [FiniteDimensional K V] : Submodule.map (Module.Dual.eval K V) (Submodule.dualCoannihilator W) = Submodule.dualAnnihilator W

theorem span_flip_eq_top_iff_linearIndependent {ι : Type u_1} {α : Type u_2} {F : Type u_3} [Finite ι] [Field F] {f : ι → α → F} : Submodule.span F (Set.range (flip f)) = ⊤ ↔ LinearIndependent F f

def TensorProduct.dualDistrib (R : Type u_1) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : TensorProduct R (Module.Dual R M) (Module.Dual R N) →ₗ[R] Module.Dual R (TensorProduct R M 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

• TensorProduct.dualDistrib R M N = LinearMap.compRight R ↑(TensorProduct.lid R R) ∘ₗ TensorProduct.homTensorHomMap R M N R R

@[simp]

theorem TensorProduct.dualDistrib_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : Module.Dual R M) (g : Module.Dual R N) (m : M) (n : N) : ((dualDistrib R M 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) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module A M] [Module R N] [IsScalarTower R A M] : TensorProduct R (Module.Dual A M) (Module.Dual R N) →ₗ[A] Module.Dual A (TensorProduct R M N)

Heterobasic version of TensorProduct.dualDistrib

Equations

• TensorProduct.AlgebraTensorModule.dualDistrib R A M N = LinearMap.compRight A (Algebra.TensorProduct.rid R A A).toLinearMap ∘ₗ TensorProduct.AlgebraTensorModule.homTensorHomMap R A A M N A R

@[simp]

theorem TensorProduct.AlgebraTensorModule.dualDistrib_apply {R : Type u_1} (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module A M] [Module R N] [IsScalarTower R A M] (f : Module.Dual A M) (g : Module.Dual R N) (m : M) (n : N) : ((dualDistrib R A M 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} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) (c : Module.Basis κ R N) : Module.Dual R (TensorProduct R M N) →ₗ[R] TensorProduct R (Module.Dual R M) (Module.Dual R N)

An inverse to TensorProduct.dualDistrib given bases.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TensorProduct.dualDistribInvOfBasis_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) (c : Module.Basis κ R N) (f : Module.Dual R (TensorProduct R M N)) : (dualDistribInvOfBasis b c) f = ∑ i : ι, ∑ j : κ, f (b i ⊗ₜ[R] c j) • b.dualBasis i ⊗ₜ[R] c.dualBasis 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} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) (c : Module.Basis κ R N) : dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c = 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} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) (c : Module.Basis κ R N) : dualDistribInvOfBasis b c ∘ₗ dualDistrib R M N = LinearMap.id

noncomputable def TensorProduct.dualDistribEquivOfBasis {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) (c : Module.Basis κ R N) : TensorProduct R (Module.Dual R M) (Module.Dual R N) ≃ₗ[R] Module.Dual R (TensorProduct 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 TensorProduct.map f g with the natural isomorphism R ⊗ R ≃ R.

Equations

• TensorProduct.dualDistribEquivOfBasis b c = LinearEquiv.ofLinear (TensorProduct.dualDistrib R M N) (TensorProduct.dualDistribInvOfBasis b c) ⋯ ⋯

@[simp]

theorem TensorProduct.dualDistribEquivOfBasis_apply_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) (c : Module.Basis κ R N) (a✝ : TensorProduct R (Module.Dual R M) (Module.Dual R N)) (a✝¹ : TensorProduct R M N) : ((dualDistribEquivOfBasis b c) a✝) a✝¹ = (TensorProduct.lid R R) (((homTensorHomMap R M N R R) a✝) a✝¹)

@[simp]

theorem TensorProduct.dualDistribEquivOfBasis_symm_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) (c : Module.Basis κ R N) (a : Module.Dual R (TensorProduct R M N)) : (dualDistribEquivOfBasis b c).symm a = ∑ x : ι, ∑ x_1 : κ, a (b x ⊗ₜ[R] c x_1) • b.coord x ⊗ₜ[R] c.coord x_1

noncomputable def TensorProduct.dualDistribEquiv (R : Type u_1) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Free R M] [Module.Free R N] : TensorProduct R (Module.Dual R M) (Module.Dual R N) ≃ₗ[R] Module.Dual R (TensorProduct 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 TensorProduct.map f g with the natural isomorphism R ⊗ R ≃ R.

Equations

• TensorProduct.dualDistribEquiv R M N = TensorProduct.dualDistribEquivOfBasis (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R N)