# 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)`.

source
@[reducible, inline]
abbrev Module.Dual (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] :
Type (max u_5 u_4)

The left 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

source
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

Instances For

source
@[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
source
instance Module.Dual.instInhabited (M : Type u_3) [AddCommMonoid M] (R : Type u_4) [Semiring R] [Module R M] :
Inhabited (Dual R M)
Equations

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

source
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

Instances For

source
@[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
source
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

Instances For

source
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
source
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
source
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

Instances For

source
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
source
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
source
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
source
@[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)
source
@[simp]
theorem LinearMap.dualMap_id {R : Type u_1} {M₁ : Type u_2} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] :
id.dualMap = id
source
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
source
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.

source
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 `LinearEquiv` version of `LinearMap.dualMap`.

Equations

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

Instances For

source
@[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)
source
@[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₁)
source
@[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
source
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
source
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
source
@[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
source
@[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}
source
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.

Instances

source
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)
source
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) = ⊤
source
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) ⋯

Instances For

source
@[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
source
@[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
source
@[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
source
@[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)
source
@[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
source
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
source
@[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
source
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.

source
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.

source
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)

Instances For

source
@[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
source
@[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''
source
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
source
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 ᵐᵒᵖ
source
@[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
source
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

Instances For

source
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
source
@[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
source
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

Instances For

source
@[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
source
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$.

source
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

Instances For

source
@[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
source
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
source
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
source
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
source
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)
source
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
source
@[simp]
theorem Submodule.dualAnnihilator_bot {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
⊥.dualAnnihilator = ⊤
source
@[simp]
theorem Submodule.dualAnnihilator_top {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
⊤.dualAnnihilator = ⊥
source
@[simp]
theorem Submodule.dualCoannihilator_bot {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
⊥.dualCoannihilator = ⊤
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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.

source
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.

source
@[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)}
source
@[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}
source
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
source
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
source
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
source
@[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