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) [CommSemiring R] [AddCommMonoid M] [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

• Module.Dual R M = (M →ₗ[R] R)

Instances For

• Basis.dual_finite
• Basis.dual_free
• Module.Dual.instInhabitedDual
• Module.Dual.instIsReflecive
• Module.instNontrivialDual
• Module.instSubsingletonDual
• Subspace.instModuleDualFiniteDimensional

def Module.dualPairing (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Module.Dual R M →ₗ[R] M →ₗ[R] R

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

Equations

• Module.dualPairing R M = LinearMap.id

@[simp]

theorem Module.dualPairing_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (v : Module.Dual R M) (x : M) : ((Module.dualPairing R M) v) x = v x

instance Module.Dual.instInhabitedDual (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : Inhabited (Module.Dual R M)

Equations

• Module.Dual.instInhabitedDual R M = { default := 0 }

def Module.Dual.eval (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : M →ₗ[R] Module.Dual R (Module.Dual R M)

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

Equations

• Module.Dual.eval R M = LinearMap.flip LinearMap.id

@[simp]

theorem Module.Dual.eval_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (v : M) (a : Module.Dual R M) : ((Module.Dual.eval R M) v) a = a v

def Module.Dual.transpose {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type uM'} [AddCommMonoid M'] [Module R M'] : (M →ₗ[R] M') →ₗ[R] Module.Dual R M' →ₗ[R] Module.Dual R M

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

Equations

• Module.Dual.transpose = LinearMap.flip (LinearMap.llcomp R M M' R)

theorem Module.Dual.transpose_apply {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type uM'} [AddCommMonoid M'] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type uM'} [AddCommMonoid M'] [Module R M'] {M'' : Type uM''} [AddCommMonoid M''] [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) [CommSemiring R] [AddCommMonoid M] [Module R M] (M' : Type uM') [AddCommMonoid M'] [Module R M'] (f : M × M' →ₗ[R] R) : (LinearEquiv.symm (Module.dualProdDualEquivDual R M M')) f = (LinearMap.comp f (LinearMap.inl R M M'), LinearMap.comp f (LinearMap.inr R M M'))

@[simp]

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

def Module.dualProdDualEquivDual (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (M' : Type uM') [AddCommMonoid M'] [Module R M'] : (Module.Dual R M × Module.Dual R M') ≃ₗ[R] Module.Dual R (M × M')

Taking duals distributes over products.

Equations

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

@[simp]

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

def LinearMap.dualMap {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) : Module.Dual R M₂ →ₗ[R] Module.Dual R M₁

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

Equations

• LinearMap.dualMap f = Module.Dual.transpose f

theorem LinearMap.dualMap_eq_lcomp {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) : LinearMap.dualMap f = LinearMap.lcomp R R f

theorem LinearMap.dualMap_def {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) : LinearMap.dualMap f = Module.Dual.transpose f

theorem LinearMap.dualMap_apply' {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) (g : Module.Dual R M₂) : (LinearMap.dualMap f) g = g ∘ₗ f

@[simp]

theorem LinearMap.dualMap_apply {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) (g : Module.Dual R M₂) (x : M₁) : ((LinearMap.dualMap f) g) x = g (f x)

@[simp]

theorem LinearMap.dualMap_id {R : Type u} [CommSemiring R] {M₁ : Type v} [AddCommMonoid M₁] [Module R M₁] : LinearMap.dualMap LinearMap.id = LinearMap.id

theorem LinearMap.dualMap_comp_dualMap {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_1} [AddCommGroup M₃] [Module R M₃] (f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) : LinearMap.dualMap f ∘ₗ LinearMap.dualMap g = LinearMap.dualMap (g ∘ₗ f)

theorem LinearMap.dualMap_injective_of_surjective {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {f : M₁ →ₗ[R] M₂} (hf : Function.Surjective ⇑f) : Function.Injective ⇑(LinearMap.dualMap f)

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

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

The Linear_equiv version of LinearMap.dualMap.

Equations

• LinearEquiv.dualMap f = let __spread.0 := LinearMap.dualMap ↑f; { toLinearMap := __spread.0, invFun := ⇑(LinearMap.dualMap ↑(LinearEquiv.symm f)), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LinearEquiv.dualMap_apply {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ ≃ₗ[R] M₂) (g : Module.Dual R M₂) (x : M₁) : ((LinearEquiv.dualMap f) g) x = g (f x)

@[simp]

theorem LinearEquiv.dualMap_refl {R : Type u} [CommSemiring R] {M₁ : Type v} [AddCommMonoid M₁] [Module R M₁] : LinearEquiv.dualMap (LinearEquiv.refl R M₁) = LinearEquiv.refl R (Module.Dual R M₁)

@[simp]

theorem LinearEquiv.dualMap_symm {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {f : M₁ ≃ₗ[R] M₂} : LinearEquiv.symm (LinearEquiv.dualMap f) = LinearEquiv.dualMap (LinearEquiv.symm f)

theorem LinearEquiv.dualMap_trans {R : Type u} [CommSemiring R] {M₁ : Type v} {M₂ : Type v'} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_1} [AddCommGroup M₃] [Module R M₃] (f : M₁ ≃ₗ[R] M₂) (g : M₂ ≃ₗ[R] M₃) : LinearEquiv.dualMap g ≪≫ₗ LinearEquiv.dualMap f = LinearEquiv.dualMap (f ≪≫ₗ g)

@[simp]

theorem Dual.apply_one_mul_eq {R : Type u} [CommSemiring R] (f : Module.Dual R R) (r : R) : f 1 * r = f r

@[simp]

theorem LinearMap.range_dualMap_dual_eq_span_singleton {R : Type u} [CommSemiring R] {M₁ : Type v} [AddCommMonoid M₁] [Module R M₁] (f : Module.Dual R M₁) : LinearMap.range (LinearMap.dualMap f) = Submodule.span R {f}

def Basis.toDual {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) : M →ₗ[R] Module.Dual R M

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

Equations

• Basis.toDual b = (Basis.constr b ℕ) fun (v : ι) => (Basis.constr b ℕ) fun (w : ι) => if w = v then 1 else 0

theorem Basis.toDual_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (i : ι) (j : ι) : ((Basis.toDual b) (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ι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) : ((Basis.toDual b) ((Finsupp.total ι M R ⇑b) f)) (b i) = f i

@[simp]

theorem Basis.toDual_total_right {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) : ((Basis.toDual b) (b i)) ((Finsupp.total ι M R ⇑b) f) = f i

theorem Basis.toDual_apply_left {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) (i : ι) : ((Basis.toDual b) m) (b i) = (b.repr m) i

theorem Basis.toDual_apply_right {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (i : ι) (m : M) : ((Basis.toDual b) (b i)) m = (b.repr m) i

theorem Basis.coe_toDual_self {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (i : ι) : (Basis.toDual b) (b i) = Basis.coord b i

def Basis.toDualFlip {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) : M →ₗ[R] R

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

Equations

• Basis.toDualFlip b m = (LinearMap.flip (Basis.toDual b)) m

theorem Basis.toDualFlip_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m₁ : M) (m₂ : M) : (Basis.toDualFlip b m₁) m₂ = ((Basis.toDual b) m₂) m₁

theorem Basis.toDual_eq_repr {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) (i : ι) : ((Basis.toDual b) m) (b i) = (b.repr m) i

theorem Basis.toDual_eq_equivFun {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (m : M) (i : ι) : ((Basis.toDual b) m) (b i) = (Basis.equivFun b) m i

theorem Basis.toDual_injective {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) : Function.Injective ⇑(Basis.toDual b)

theorem Basis.toDual_inj {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) (m : M) (a : (Basis.toDual b) m = 0) : m = 0

theorem Basis.toDual_ker {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) : LinearMap.ker (Basis.toDual b) = ⊥

theorem Basis.toDual_range {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] : LinearMap.range (Basis.toDual b) = ⊤

@[simp]

theorem Basis.sum_dual_apply_smul_coord {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) (f : Module.Dual R M) : (Finset.sum Finset.univ fun (x : ι) => f (b x) • Basis.coord b x) = f

def Basis.toDualEquiv {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] : M ≃ₗ[R] Module.Dual R M

A vector space is linearly equivalent to its dual space.

Equations

• Basis.toDualEquiv b = LinearEquiv.ofBijective (Basis.toDual b) ⋯

@[simp]

theorem Basis.toDualEquiv_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (m : M) : (Basis.toDualEquiv b) m = (Basis.toDual b) m

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.

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

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

Equations

• Basis.dualBasis b = Basis.map b (Basis.toDualEquiv b)

theorem Basis.dualBasis_apply_self {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (i : ι) (j : ι) : ((Basis.dualBasis b) i) (b j) = if j = i then 1 else 0

theorem Basis.total_dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (f : ι →₀ R) (i : ι) : ((Finsupp.total ι (Module.Dual R M) R ⇑(Basis.dualBasis b)) f) (b i) = f i

theorem Basis.dualBasis_repr {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (l : Module.Dual R M) (i : ι) : ((Basis.dualBasis b).repr l) i = l (b i)

theorem Basis.dualBasis_apply {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (i : ι) (m : M) : ((Basis.dualBasis b) i) m = (b.repr m) i

@[simp]

theorem Basis.coe_dualBasis {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] : ⇑(Basis.dualBasis b) = Basis.coord b

@[simp]

theorem Basis.toDual_toDual {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] : Basis.toDual (Basis.dualBasis b) ∘ₗ Basis.toDual b = Module.Dual.eval R M

theorem Basis.dualBasis_equivFun {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] (l : Module.Dual R M) (i : ι) : (Basis.equivFun (Basis.dualBasis b)) l i = l (b i)

theorem Basis.eval_ker {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_1} (b : Basis ι R M) : LinearMap.ker (Module.Dual.eval R M) = ⊥

theorem Basis.eval_range {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_1} [Finite ι] (b : Basis ι R M) : LinearMap.range (Module.Dual.eval R M) = ⊤

instance Basis.dual_free {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] : Module.Free R (Module.Dual R M)

Equations

• ⋯ = ⋯

instance Basis.dual_finite {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] : Module.Finite R (Module.Dual R M)

Equations

• ⋯ = ⋯

@[simp]

theorem Basis.total_coord {R : Type uR} {M : Type uM} {ι : Type uι} [CommRing R] [AddCommGroup M] [Module R M] [Finite ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) : ((Finsupp.total ι (Module.Dual R M) R (Basis.coord b)) 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ι} [CommRing K] [AddCommGroup V] [Module K V] [Finite ι] (b : Basis ι K V) : Cardinal.lift.{uK, uV} (Module.rank K V) = Module.rank K (Module.Dual K V)

theorem Module.eval_ker (K : Type uK) (V : Type uV) [CommRing K] [AddCommGroup V] [Module K V] [Module.Free K V] : LinearMap.ker (Module.Dual.eval K V) = ⊥

theorem Module.map_eval_injective (K : Type uK) (V : Type uV) [CommRing K] [AddCommGroup V] [Module K V] [Module.Free K V] : Function.Injective (Submodule.map (Module.Dual.eval K V))

theorem Module.comap_eval_surjective (K : Type uK) (V : Type uV) [CommRing K] [AddCommGroup V] [Module K V] [Module.Free K V] : Function.Surjective (Submodule.comap (Module.Dual.eval K V))

theorem Module.eval_apply_eq_zero_iff (K : Type uK) {V : Type uV} [CommRing K] [AddCommGroup V] [Module K V] [Module.Free K V] (v : V) : (Module.Dual.eval K V) v = 0 ↔ v = 0

theorem Module.eval_apply_injective (K : Type uK) {V : Type uV} [CommRing K] [AddCommGroup V] [Module K V] [Module.Free K V] : Function.Injective ⇑(Module.Dual.eval K V)

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

@[simp]

theorem Module.subsingleton_dual_iff (K : Type uK) {V : Type uV} [CommRing K] [AddCommGroup V] [Module K V] [Module.Free K V] : Subsingleton (Module.Dual K V) ↔ Subsingleton V

instance Module.instSubsingletonDual (K : Type uK) {V : Type uV} [CommRing K] [AddCommGroup V] [Module K V] [Module.Free K V] [Subsingleton V] : Subsingleton (Module.Dual K V)

Equations

• ⋯ = ⋯

@[simp]

theorem Module.nontrivial_dual_iff (K : Type uK) {V : Type uV} [CommRing K] [AddCommGroup V] [Module K V] [Module.Free K V] : Nontrivial (Module.Dual K V) ↔ Nontrivial V

instance Module.instNontrivialDual (K : Type uK) {V : Type uV} [CommRing K] [AddCommGroup V] [Module K V] [Module.Free K V] [Nontrivial V] : Nontrivial (Module.Dual K V)

Equations

• ⋯ = ⋯

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

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

theorem Module.erange_coe {K : Type uK} {V : Type uV} [CommRing K] [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] : LinearMap.range (Module.Dual.eval K V) = ⊤

class Module.IsReflexive (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] : Prop

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' : Function.Bijective ⇑(Module.Dual.eval R M)

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

Instances

• Module.Dual.instIsReflecive
• Module.IsReflexive.of_finite_of_free
• MulOpposite.instModuleIsReflexive
• Prod.instModuleIsReflexive
• ULift.instModuleIsReflexive

theorem Module.bijective_dual_eval (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] : Function.Bijective ⇑(Module.Dual.eval R M)

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

Equations

• ⋯ = ⋯

def Module.evalEquiv (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] : M ≃ₗ[R] Module.Dual R (Module.Dual R M)

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

Equations

• Module.evalEquiv R M = LinearEquiv.ofBijective (Module.Dual.eval R M) ⋯

@[simp]

theorem Module.evalEquiv_toLinearMap (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] : ↑(Module.evalEquiv R M) = Module.Dual.eval R M

@[simp]

theorem Module.evalEquiv_apply (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] (m : M) : (Module.evalEquiv R M) m = (Module.Dual.eval R M) m

@[simp]

theorem Module.apply_evalEquiv_symm_apply (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] (f : Module.Dual R M) (g : Module.Dual R (Module.Dual R M)) : f ((LinearEquiv.symm (Module.evalEquiv R M)) g) = g f

@[simp]

theorem Module.symm_dualMap_evalEquiv (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] : ↑(LinearEquiv.dualMap (LinearEquiv.symm (Module.evalEquiv R M))) = Module.Dual.eval R (Module.Dual R M)

instance Module.Dual.instIsReflecive (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] : Module.IsReflexive R (Module.Dual R M)

The dual of a reflexive module is reflexive.

Equations

• ⋯ = ⋯

def Module.mapEvalEquiv (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] : Submodule R M ≃o Submodule R (Module.Dual R (Module.Dual R M))

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

Equations

• Module.mapEvalEquiv R M = Submodule.orderIsoMapComap (Module.evalEquiv R M)

@[simp]

theorem Module.mapEvalEquiv_apply (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] (W : Submodule R M) : (Module.mapEvalEquiv R M) W = Submodule.map (Module.Dual.eval R M) W

@[simp]

theorem Module.mapEvalEquiv_symm_apply (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] (W'' : Submodule R (Module.Dual R (Module.Dual R M))) : (OrderIso.symm (Module.mapEvalEquiv R M)) W'' = Submodule.comap (Module.Dual.eval R M) W''

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

Equations

• ⋯ = ⋯

theorem Module.equiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.IsReflexive R M] (e : M ≃ₗ[R] N) : Module.IsReflexive R N

instance MulOpposite.instModuleIsReflexive (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] : Module.IsReflexive R Mᵐᵒᵖ

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 ∧ Submodule.map f p = ⊥

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 ∧ Submodule.map f p = ⊥

def evalUseFiniteInstance : Lean.Elab.Tactic.TacticM Unit

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

Equations

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

def tacticUse_finite_instance : Lean.ParserDescr

Equations

• tacticUse_finite_instance = Lean.ParserDescr.node `tacticUse_finite_instance 1024 (Lean.ParserDescr.nonReservedSymbol "use_finite_instance" false)

structure Module.DualBases {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (e : ι → M) (ε : ι → Module.Dual R M) : Prop

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}

def Module.DualBases.coeffs {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ι → M} {ε : ι → Module.Dual R M} [DecidableEq ι] (h : Module.DualBases e ε) (m : M) : ι →₀ R

The coefficients of v on the basis e

Equations

• Module.DualBases.coeffs h m = { support := Set.Finite.toFinset ⋯, toFun := fun (i : ι) => (ε i) m, mem_support_toFun := ⋯ }

@[simp]

theorem Module.DualBases.coeffs_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ι → M} {ε : ι → Module.Dual R M} [DecidableEq ι] (h : Module.DualBases e ε) (m : M) (i : ι) : (Module.DualBases.coeffs h m) i = (ε i) m

def Module.DualBases.lc {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [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

• Module.DualBases.lc e l = Finsupp.sum l fun (i : ι) (a : R) => a • e i

theorem Module.DualBases.lc_def {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (e : ι → M) (l : ι →₀ R) : Module.DualBases.lc e l = (Finsupp.total ι M R e) l

theorem Module.DualBases.dual_lc {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ι → M} {ε : ι → Module.Dual R M} [DecidableEq ι] (h : Module.DualBases e ε) (l : ι →₀ R) (i : ι) : (ε i) (Module.DualBases.lc e l) = l i

@[simp]

theorem Module.DualBases.coeffs_lc {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ι → M} {ε : ι → Module.Dual R M} [DecidableEq ι] (h : Module.DualBases e ε) (l : ι →₀ R) : Module.DualBases.coeffs h (Module.DualBases.lc e l) = l

@[simp]

theorem Module.DualBases.lc_coeffs {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ι → M} {ε : ι → Module.Dual R M} [DecidableEq ι] (h : Module.DualBases e ε) (m : M) : Module.DualBases.lc e (Module.DualBases.coeffs 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} [CommRing R] [AddCommGroup M] [Module R M] {e : ι → M} {ε : ι → Module.Dual R M} [DecidableEq ι] (h : Module.DualBases e ε) (m : M) : (Module.DualBases.basis h).repr m = Module.DualBases.coeffs h m

@[simp]

theorem Module.DualBases.basis_repr_symm_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ι → M} {ε : ι → Module.Dual R M} [DecidableEq ι] (h : Module.DualBases e ε) (l : ι →₀ R) : (LinearEquiv.symm (Module.DualBases.basis h).repr) l = Module.DualBases.lc e l

def Module.DualBases.basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ι → M} {ε : ι → Module.Dual R M} [DecidableEq ι] (h : Module.DualBases e ε) : 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.

@[simp]

theorem Module.DualBases.coe_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ι → M} {ε : ι → Module.Dual R M} [DecidableEq ι] (h : Module.DualBases e ε) : ⇑(Module.DualBases.basis h) = e

theorem Module.DualBases.mem_of_mem_span {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ι → M} {ε : ι → Module.Dual R M} [DecidableEq ι] (h : Module.DualBases e ε) {H : Set ι} {x : M} (hmem : x ∈ Submodule.span R (e '' H)) (i : ι) : (ε i) x ≠ 0 → i ∈ H

theorem Module.DualBases.coe_dualBasis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {e : ι → M} {ε : ι → Module.Dual R M} [DecidableEq ι] (h : Module.DualBases e ε) [Finite ι] : ⇑(Basis.dualBasis (Module.DualBases.basis h)) = ε

def Submodule.dualRestrict {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (W : Submodule R M) : Module.Dual R M →ₗ[R] Module.Dual R ↥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

• Submodule.dualRestrict W = LinearMap.domRestrict' W

theorem Submodule.dualRestrict_def {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (W : Submodule R M) : Submodule.dualRestrict W = LinearMap.dualMap (Submodule.subtype W)

@[simp]

theorem Submodule.dualRestrict_apply {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (W : Submodule R M) (φ : Module.Dual R M) (x : ↥W) : ((Submodule.dualRestrict W) φ) x = φ ↑x

def Submodule.dualAnnihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (W : Submodule R M) : Submodule R (Module.Dual R M)

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

Equations

• Submodule.dualAnnihilator W = LinearMap.ker (Submodule.dualRestrict W)

@[simp]

theorem Submodule.mem_dualAnnihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {W : Submodule R M} (φ : Module.Dual R M) : φ ∈ Submodule.dualAnnihilator W ↔ ∀ w ∈ W, φ w = 0

theorem Submodule.dualRestrict_ker_eq_dualAnnihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (W : Submodule R M) : LinearMap.ker (Submodule.dualRestrict W) = Submodule.dualAnnihilator W

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

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

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

Equations

• Submodule.dualCoannihilator Φ = Submodule.comap (Module.Dual.eval R M) (Submodule.dualAnnihilator Φ)

@[simp]

theorem Submodule.mem_dualCoannihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {Φ : Submodule R (Module.Dual R M)} (x : M) : x ∈ Submodule.dualCoannihilator Φ ↔ ∀ φ ∈ Φ, φ x = 0

theorem Submodule.comap_dualAnnihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (Φ : Submodule R (Module.Dual R M)) : Submodule.comap (Module.Dual.eval R M) (Submodule.dualAnnihilator Φ) = Submodule.dualCoannihilator Φ

theorem Submodule.map_dualCoannihilator_le {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (Φ : Submodule R (Module.Dual R M)) : Submodule.map (Module.Dual.eval R M) (Submodule.dualCoannihilator Φ) ≤ Submodule.dualAnnihilator Φ

theorem Submodule.dualAnnihilator_gc (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] {U : Submodule R (Module.Dual R M)} {V : Submodule R M} : U ≤ Submodule.dualAnnihilator V ↔ V ≤ Submodule.dualCoannihilator U

@[simp]

theorem Submodule.dualAnnihilator_bot {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] : Submodule.dualAnnihilator ⊥ = ⊤

@[simp]

theorem Submodule.dualAnnihilator_top {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] : Submodule.dualAnnihilator ⊤ = ⊥

@[simp]

theorem Submodule.dualCoannihilator_bot {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] : Submodule.dualCoannihilator ⊥ = ⊤

theorem Submodule.dualAnnihilator_anti {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {U : Submodule R M} {V : Submodule R M} (hUV : U ≤ V) : Submodule.dualAnnihilator V ≤ Submodule.dualAnnihilator U

theorem Submodule.dualCoannihilator_anti {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {U : Submodule R (Module.Dual R M)} {V : Submodule R (Module.Dual R M)} (hUV : U ≤ V) : Submodule.dualCoannihilator V ≤ Submodule.dualCoannihilator U

theorem Submodule.le_dualAnnihilator_dualCoannihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (U : Submodule R M) : U ≤ Submodule.dualCoannihilator (Submodule.dualAnnihilator U)

theorem Submodule.le_dualCoannihilator_dualAnnihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (U : Submodule R (Module.Dual R M)) : U ≤ Submodule.dualAnnihilator (Submodule.dualCoannihilator U)

theorem Submodule.dualAnnihilator_dualCoannihilator_dualAnnihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (U : Submodule R M) : Submodule.dualAnnihilator (Submodule.dualCoannihilator (Submodule.dualAnnihilator U)) = Submodule.dualAnnihilator U

theorem Submodule.dualCoannihilator_dualAnnihilator_dualCoannihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (U : Submodule R (Module.Dual R M)) : Submodule.dualCoannihilator (Submodule.dualAnnihilator (Submodule.dualCoannihilator U)) = Submodule.dualCoannihilator U

theorem Submodule.dualAnnihilator_sup_eq {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (U : Submodule R M) (V : Submodule R M) : Submodule.dualAnnihilator (U ⊔ V) = Submodule.dualAnnihilator U ⊓ Submodule.dualAnnihilator V

theorem Submodule.dualCoannihilator_sup_eq {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (U : Submodule R (Module.Dual R M)) (V : Submodule R (Module.Dual R M)) : Submodule.dualCoannihilator (U ⊔ V) = Submodule.dualCoannihilator U ⊓ Submodule.dualCoannihilator V

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

theorem Submodule.dualCoannihilator_iSup_eq {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_1} (U : ι → Submodule R (Module.Dual R M)) : Submodule.dualCoannihilator (⨆ (i : ι), U i) = ⨅ (i : ι), Submodule.dualCoannihilator (U i)

theorem Submodule.sup_dualAnnihilator_le_inf {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (U : Submodule R M) (V : Submodule R M) : Submodule.dualAnnihilator U ⊔ Submodule.dualAnnihilator V ≤ Submodule.dualAnnihilator (U ⊓ V)

See also Subspace.dualAnnihilator_inf_eq for vector subspaces.

theorem Submodule.iSup_dualAnnihilator_le_iInf {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_1} (U : ι → Submodule R M) : ⨆ (i : ι), Submodule.dualAnnihilator (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} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) : Submodule.dualCoannihilator ⊤ = ⊥

@[simp]

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

theorem Subspace.forall_mem_dualAnnihilator_apply_eq_zero_iff {K : Type u} {V : Type v} [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} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) : Submodule.comap (Module.Dual.eval K V) (Submodule.dualAnnihilator (Submodule.dualAnnihilator W)) = W

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

def Subspace.dualAnnihilatorGci (K : Type u_1) (V : Type u_2) [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} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K V} {W' : Subspace K V} : Submodule.dualAnnihilator W ≤ Submodule.dualAnnihilator W' ↔ W' ≤ W

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

noncomputable def Subspace.dualLift {K : Type u} {V : Type v} [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

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

@[simp]

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

theorem Subspace.dualLift_of_mem {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K V} {φ : Module.Dual K ↥W} {w : V} (hw : w ∈ W) : ((Subspace.dualLift W) φ) w = φ { val := w, property := hw }

@[simp]

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

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

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

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

theorem Subspace.dualLift_injective {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K V} : Function.Injective ⇑(Subspace.dualLift W)

noncomputable def Subspace.quotAnnihilatorEquiv {K : Type u} {V : Type v} [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

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

@[simp]

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

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

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

Equations

• Subspace.dualEquivDual W = LinearEquiv.ofInjective (Subspace.dualLift W) ⋯

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

@[simp]

theorem Subspace.dualEquivDual_apply {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K V} (φ : Module.Dual K ↥W) : (Subspace.dualEquivDual W) φ = { val := (Subspace.dualLift W) φ, property := ⋯ }

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

Equations

• ⋯ = ⋯

@[simp]

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

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

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

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

Equations

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

noncomputable def Subspace.quotEquivAnnihilator {K : Type u} {V : Type v} [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.

@[simp]

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

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

theorem LinearMap.ker_dualMap_eq_dualAnnihilator_range {R : Type uR} [CommSemiring R] {M₁ : Type uM₁} {M₂ : Type uM₂} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) : LinearMap.ker (LinearMap.dualMap f) = Submodule.dualAnnihilator (LinearMap.range f)

theorem LinearMap.range_dualMap_le_dualAnnihilator_ker {R : Type uR} [CommSemiring R] {M₁ : Type uM₁} {M₂ : Type uM₂} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) : LinearMap.range (LinearMap.dualMap f) ≤ Submodule.dualAnnihilator (LinearMap.ker f)

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

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

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

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} [CommRing R] [AddCommGroup M] [Module R M] {W : Submodule R M} (φ : ↥(Submodule.dualAnnihilator W)) (x : M) : ((Submodule.dualCopairing W) φ) (Submodule.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 ⧸ Submodule.dualAnnihilator 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

• Submodule.dualPairing W = Submodule.liftQ (Submodule.dualAnnihilator W) (Submodule.dualRestrict W) ⋯

@[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) : ((Submodule.dualPairing W) (Submodule.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 (LinearMap.dualMap (Submodule.mkQ W)) = Submodule.dualAnnihilator W

That $\mathrm{im}(q^{\ast }:(V/W{)}^{\ast }\to V^{\ast })=\mathrm{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] ↥(Submodule.dualAnnihilator W)

Equivalence $(M/W{)}^{\ast }\cong \mathrm{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

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

@[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) : ((Submodule.dualQuotEquivDualAnnihilator W) φ) x = φ (Submodule.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) : Submodule.dualCopairing W = ↑(LinearEquiv.symm (Submodule.dualQuotEquivDualAnnihilator W))

@[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) (φ : ↥(Submodule.dualAnnihilator W)) (x : M) : ((LinearEquiv.symm (Submodule.dualQuotEquivDualAnnihilator W)) φ) (Submodule.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 ↥(Submodule.dualAnnihilator W) ↔ Module.Finite R (M ⧸ 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 ⧸ Submodule.dualCoannihilator W →ₗ[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

• Submodule.quotDualCoannihilatorToDual W = Submodule.liftQ (Submodule.dualCoannihilator W) (LinearMap.flip (Submodule.subtype W)) ⋯

@[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) : ((Submodule.quotDualCoannihilatorToDual W) (Submodule.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 ⇑(Submodule.quotDualCoannihilatorToDual W)

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 ⇑(LinearMap.flip (Submodule.quotDualCoannihilatorToDual W))

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)) : LinearMap.Nondegenerate (Submodule.quotDualCoannihilatorToDual W)

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) : LinearMap.range (LinearMap.dualMap f) = Submodule.dualAnnihilator (LinearMap.ker f)

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 ⇑(LinearMap.dualMap (Submodule.subtype (LinearMap.range f)))) : LinearMap.range (LinearMap.dualMap f) = Submodule.dualAnnihilator (LinearMap.ker f)

theorem LinearMap.ker_dualMap_eq_dualCoannihilator_range {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') : LinearMap.ker (LinearMap.dualMap f) = Submodule.dualCoannihilator (LinearMap.range (Module.Dual.eval R M' ∘ₗ f))

@[simp]

theorem LinearMap.dualCoannihilator_range_eq_ker_flip {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (B : M →ₗ[R] M' →ₗ[R] R) : Submodule.dualCoannihilator (LinearMap.range B) = LinearMap.ker (LinearMap.flip B)

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

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

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

@[simp]

theorem LinearMap.dualMap_surjective_iff {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {f : V₁ →ₗ[K] V₂} : Function.Surjective ⇑(LinearMap.dualMap f) ↔ Function.Injective ⇑f

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

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

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

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

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

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

theorem Subspace.isCompl_dualAnnihilator {K : Type uK} [Field K] {V₁ : Type uV₁} [AddCommGroup V₁] [Module K V₁] {W : Subspace K V₁} {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 uK} [Field K] {V₁ : Type uV₁} [AddCommGroup V₁] [Module K V₁] [FiniteDimensional K V₁] (W : Subspace K V₁) : Module.Dual K (V₁ ⧸ W) ≃ₗ[K] Module.Dual K V₁ ⧸ LinearMap.range (Subspace.dualLift W)

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

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

@[simp]

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

@[simp]

theorem LinearMap.dualMap_injective_iff {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {f : V₁ →ₗ[K] V₂} : Function.Injective ⇑(LinearMap.dualMap f) ↔ Function.Surjective ⇑f

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

@[simp]

theorem LinearMap.dualMap_bijective_iff {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {f : V₁ →ₗ[K] V₂} : Function.Bijective ⇑(LinearMap.dualMap f) ↔ Function.Bijective ⇑f

f.dualMap is bijective if and only if f is

@[simp]

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

theorem LinearMap.flip_injective_iff₁ {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₁] : Function.Injective ⇑(LinearMap.flip B) ↔ Function.Surjective ⇑B

theorem LinearMap.flip_injective_iff₂ {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₂] : Function.Injective ⇑(LinearMap.flip B) ↔ Function.Surjective ⇑B

theorem LinearMap.flip_surjective_iff₁ {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₁] : Function.Surjective ⇑(LinearMap.flip B) ↔ Function.Injective ⇑B

theorem LinearMap.flip_surjective_iff₂ {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₂] : Function.Surjective ⇑(LinearMap.flip B) ↔ Function.Injective ⇑B

theorem LinearMap.flip_bijective_iff₁ {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₁] : Function.Bijective ⇑(LinearMap.flip B) ↔ Function.Bijective ⇑B

theorem LinearMap.flip_bijective_iff₂ {K : Type uK} [Field K] {V₁ : Type uV₁} {V₂ : Type uV₂} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₂] : Function.Bijective ⇑(LinearMap.flip B) ↔ Function.Bijective ⇑B

theorem Subspace.quotDualCoannihilatorToDual_bijective {K : Type u_1} {V : Type u_2} [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_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K (Module.Dual K V)) [FiniteDimensional K ↥W] : Function.Bijective ⇑(LinearMap.flip (Submodule.quotDualCoannihilatorToDual W))

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

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

def Subspace.orderIsoFiniteCodimDim {K : Type u_1} {V : Type u_2} [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_1} {V : Type u_2} [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_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) [FiniteDimensional K ↥W] : Submodule.dualAnnihilator (Submodule.dualAnnihilator W) = Submodule.map (Module.Dual.eval K V) W

theorem Subspace.map_dualCoannihilator {K : Type u_1} {V : Type u_2} [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

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.comp (LinearMap.compRight ↑(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) : ((TensorProduct.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

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

@[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) : ((TensorProduct.AlgebraTensorModule.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 κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (b : Basis ι R M) (c : 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 κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) (f : Module.Dual R (TensorProduct R M N)) : (TensorProduct.dualDistribInvOfBasis b c) f = Finset.sum Finset.univ fun (i : ι) => Finset.sum Finset.univ fun (j : κ) => f (b i ⊗ₜ[R] c j) • (Basis.dualBasis b) i ⊗ₜ[R] (Basis.dualBasis c) 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 κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) : TensorProduct.dualDistrib R M N ∘ₗ TensorProduct.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 κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) : TensorProduct.dualDistribInvOfBasis b c ∘ₗ TensorProduct.dualDistrib R M N = LinearMap.id

@[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 κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) (a : Module.Dual R (TensorProduct R M N)) : (LinearEquiv.symm (TensorProduct.dualDistribEquivOfBasis b c)) a = Finset.sum Finset.univ fun (x : ι) => Finset.sum Finset.univ fun (x_1 : κ) => a (b x ⊗ₜ[R] c x_1) • Basis.coord b x ⊗ₜ[R] Basis.coord c x_1

@[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 κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) : ∀ (a : TensorProduct R (Module.Dual R M) (Module.Dual R N)) (a_1 : TensorProduct R M N), ((TensorProduct.dualDistribEquivOfBasis b c) a) a_1 = (TensorProduct.lid R R) (((TensorProduct.homTensorHomMap R M N R R) a) a_1)

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 κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (b : Basis ι R M) (c : 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) ⋯ ⋯

noncomputable def TensorProduct.dualDistribEquiv (R : Type u_1) (M : Type u_3) (N : Type u_4) [CommRing R] [AddCommGroup M] [AddCommGroup 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)