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.
• 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.dualPairing W is the canonical pairing between Dual R M ⧸ W.dualAnnihilator and W. It is nondegenerate for vector spaces (Subspace.dualPairing_nondegenerate).

Main results

• Annihilators:
  • Module.dualAnnihilator_gc R M is the antitone Galois correspondence between Submodule.dualAnnihilator and Submodule.dualCoannihilator.
• 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).

@[reducible, inline]

abbrev Module.Dual (R : Type u_1) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] : Type (max u_3 u_1)

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

Equations

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

def Module.dualPairing (R : Type u_4) (M : Type u_5) [CommSemiring R] [AddCommMonoid M] [Module R M] : 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 u_1) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] (v : Dual R M) (x : M) : ((dualPairing R M) v) x = v x

instance Module.Dual.instInhabited (R : Type u_1) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] : Inhabited (Dual R M)

Equations

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

def Module.Dual.eval (R : Type u_1) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] : M →ₗ[R] Dual R (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.id.flip

@[simp]

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

def Module.Dual.transpose {R : Type u_1} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_4} [AddCommMonoid M'] [Module R M'] : (M →ₗ[R] M') →ₗ[R] Dual R M' →ₗ[R] 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.llcomp R M M' R).flip

theorem Module.Dual.transpose_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'] (u : M →ₗ[R] M') (l : Dual R M') : (transpose u) l = l ∘ₗ u

theorem Module.Dual.transpose_comp {R : Type u_1} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_4} [AddCommMonoid M'] [Module R M'] {M'' : Type u_5} [AddCommMonoid M''] [Module R M''] (u : M' →ₗ[R] M'') (v : M →ₗ[R] M') : transpose (u ∘ₗ v) = transpose v ∘ₗ transpose u

def LinearMap.dualMap {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommSemiring R] [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

• f.dualMap = Module.Dual.transpose f

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

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

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

@[simp]

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

@[simp]

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

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

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

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

def LinearEquiv.dualMap {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommSemiring R] [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

• f.dualMap = { toLinearMap := (↑f).dualMap, invFun := ⇑(↑f.symm).dualMap, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem LinearEquiv.dualMap_symm {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {f : M₁ ≃ₗ[R] M₂} : f.dualMap.symm = f.symm.dualMap

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

theorem Module.Dual.eval_naturality {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) : f.dualMap.dualMap ∘ₗ eval R M₁ = eval R M₂ ∘ₗ f

@[simp]

theorem Dual.apply_one_mul_eq {R : Type u_1} [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_1} {M₁ : Type u_2} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] (f : Module.Dual R M₁) : range (dualMap f) = Submodule.span R {f}

class Module.IsReflexive (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid 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 projective module (and thus any finite-dimensional vector space) is reflexive. See Module.instIsReflexiveOfFiniteOfProjective.

• bijective_dual_eval' : Function.Bijective ⇑(Dual.eval R M)

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

theorem Module.bijective_dual_eval (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [IsReflexive R M] : Function.Bijective ⇑(Dual.eval R M)

theorem Module.erange_coe (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [IsReflexive R M] : LinearMap.range (Dual.eval R M) = ⊤

def Module.evalEquiv (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [IsReflexive R M] : M ≃ₗ[R] Dual R (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_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [IsReflexive R M] : ↑(evalEquiv R M) = Dual.eval R M

@[simp]

theorem Module.evalEquiv_apply (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [IsReflexive R M] (m : M) : (evalEquiv R M) m = (Dual.eval R M) m

@[simp]

theorem Module.apply_evalEquiv_symm_apply (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [IsReflexive R M] (f : Dual R M) (g : Dual R (Dual R M)) : f ((evalEquiv R M).symm g) = g f

@[simp]

theorem Module.symm_dualMap_evalEquiv (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [IsReflexive R M] : ↑(evalEquiv R M).symm.dualMap = Dual.eval R (Dual R M)

@[simp]

theorem Module.Dual.eval_comp_comp_evalEquiv_eq (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [IsReflexive R M] {M' : Type u_6} [AddCommMonoid M'] [Module R M'] {f : M →ₗ[R] M'} : eval R M' ∘ₗ f ∘ₗ ↑(evalEquiv R M).symm = f.dualMap.dualMap

theorem Module.dualMap_dualMap_eq_iff_of_injective (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [IsReflexive R M] {M' : Type u_6} [AddCommMonoid M'] [Module R M'] {f g : M →ₗ[R] M'} (h : Function.Injective ⇑(Dual.eval R M')) : f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g

@[simp]

theorem Module.dualMap_dualMap_eq_iff (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [IsReflexive R M] {M' : Type u_6} [AddCommMonoid M'] [Module R M'] [IsReflexive R M'] {f g : M →ₗ[R] M'} : f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g

instance Module.Dual.instIsReflecive (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [IsReflexive R M] : IsReflexive R (Dual R M)

The dual of a reflexive module is reflexive.

theorem Module.IsReflexive.of_split {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [IsReflexive R M] (i : N →ₗ[R] M) (s : M →ₗ[R] N) (H : s ∘ₗ i = LinearMap.id) : IsReflexive R N

A direct summand of a reflexive module is reflexive.

def Module.mapEvalEquiv (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [IsReflexive R M] : Submodule R M ≃o Submodule R (Dual R (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_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [IsReflexive R M] (W : Submodule R M) : (mapEvalEquiv R M) W = Submodule.map (Dual.eval R M) W

@[simp]

theorem Module.mapEvalEquiv_symm_apply (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [IsReflexive R M] (W'' : Submodule R (Dual R (Dual R M))) : (mapEvalEquiv R M).symm W'' = Submodule.comap (Dual.eval R M) W''

theorem Module.equiv {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [IsReflexive R M] (e : M ≃ₗ[R] N) : IsReflexive R N

instance MulOpposite.instModuleIsReflexive (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.IsReflexive R M] : Module.IsReflexive R Mᵐᵒᵖ

@[instance 100]

instance Module.instNoZeroSMulDivisorsOfIsDomain (R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [IsReflexive R M] [IsDomain R] : NoZeroSMulDivisors R M

def Submodule.dualRestrict {R : Type u_1} {M : Type u_2} [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

• W.dualRestrict = LinearMap.domRestrict' W

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

@[simp]

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

def Submodule.dualAnnihilator {R : Type u_3} {M : Type u_4} [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

• W.dualAnnihilator = LinearMap.ker W.dualRestrict

@[simp]

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

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

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

def Submodule.dualCoannihilator {R : Type u_1} {M : Type u_2} [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

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

@[simp]

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

theorem Submodule.dualAnnihilator_map_dualMap_le {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (W : Submodule R M) (f : N →ₗ[R] M) : map f.dualMap W.dualAnnihilator ≤ (comap f W).dualAnnihilator

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

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

theorem Submodule.dualAnnihilator_gc (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : GaloisConnection (⇑OrderDual.toDual ∘ dualAnnihilator) (dualCoannihilator ∘ ⇑OrderDual.ofDual)

theorem Submodule.le_dualAnnihilator_iff_le_dualCoannihilator {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {U : Submodule R (Module.Dual R M)} {V : Submodule R M} : U ≤ V.dualAnnihilator ↔ V ≤ U.dualCoannihilator

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

See also Subspace.dualAnnihilator_inf_eq for vector subspaces.

theorem Submodule.iSup_dualAnnihilator_le_iInf {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_3} (U : ι → Submodule R M) : ⨆ (i : ι), (U i).dualAnnihilator ≤ (⨅ (i : ι), U i).dualAnnihilator

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

@[simp]

theorem Submodule.coe_dualAnnihilator_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set M) : ↑(span R s).dualAnnihilator = {f : Module.Dual R M | s ⊆ ↑(LinearMap.ker f)}

@[simp]

theorem Submodule.coe_dualCoannihilator_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set (Module.Dual R M)) : ↑(span R s).dualCoannihilator = {x : M | ∀ f ∈ s, f x = 0}

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

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

theorem LinearMap.ker_dualMap_eq_dualCoannihilator_range {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') : ker f.dualMap = (range (Module.Dual.eval R M' ∘ₗ f)).dualCoannihilator

@[simp]

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