Pulling back annihilators

Over a field, pulling back functionals that annihilate a subspace gives exactly the annihilator of its inverse image. This is the extension-of-functionals statement needed when a Hom cocycle space is computed using an embedding into an injective module.

Equivalently, every functional on V vanishing on the inverse image of S is the pullback of a functional on the quotient W ⧸ S. Conversely, over any commutative ring, a functional factoring through a quotient V ⧸ U annihilates U (Submodule.comp_mkQ_mem_dualAnnihilator).

For complementary submodules p and q, over any commutative ring, restriction to p identifies the annihilator of q with the dual of p (Submodule.dualAnnihilatorEquivOfIsCompl); the inverse extends a functional by zero on q.

The dual map f^* : N^* → M^* of a linear map f : M → N exchanges kernel and cokernel up to duality. Over any commutative ring, ker f^* is the space of functionals vanishing on range f, which is (coker f)^* (LinearMap.kerDualMapEquiv). Over a field, coker f^* = M^* ⧸ range f^* is (ker f)^* by restriction (LinearMap.cokerDualMapEquiv).

The linear algebra of Lagrange multipliers follows over a field: if DF does not map ker D onto its codomain, then some nonzero functional f makes f ∘ DF a pullback g ∘ D (LinearMap.exists_ne_zero_comp_eq_comp_of_map_ker_ne_top).

theorem Submodule.comp_mkQ_mem_dualAnnihilator {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (U : Submodule R V) (ψ : Module.Dual R (V ⧸ U)) : ψ ∘ₗ U.mkQ ∈ U.dualAnnihilator

A functional factoring through the quotient V ⧸ U annihilates U.

noncomputable def Submodule.dualAnnihilatorEquivOfIsCompl {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (p q : Submodule R V) (h : IsCompl p q) : ↥q.dualAnnihilator ≃ₗ[R] Module.Dual R ↥p

For complementary submodules p and q, restriction to p identifies the functionals annihilating q with the functionals on p. The inverse extends a functional on p by zero on q.

@[simp]

theorem Submodule.dualAnnihilatorEquivOfIsCompl_apply {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (p q : Submodule R V) (h : IsCompl p q) (φ : ↥q.dualAnnihilator) (x : ↥p) : ((p.dualAnnihilatorEquivOfIsCompl q h) φ) x = ↑φ ↑x

The identification of q.dualAnnihilator with Module.Dual R p restricts a functional to p.

@[simp]

theorem Submodule.coe_dualAnnihilatorEquivOfIsCompl_symm_apply {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (p q : Submodule R V) (h : IsCompl p q) (ψ : Module.Dual R ↥p) : ↑((p.dualAnnihilatorEquivOfIsCompl q h).symm ψ) = LinearMap.ofIsCompl h ψ 0

The inverse of Submodule.dualAnnihilatorEquivOfIsCompl extends a functional on p by zero on q.

@[simp]

theorem Submodule.dualAnnihilator_map_dualMap_eq {k : Type u_1} {V : Type u_2} {W : Type u_3} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (S : Submodule k W) (f : V →ₗ[k] W) : map f.dualMap S.dualAnnihilator = (comap f S).dualAnnihilator

Pullback of functionals annihilating S gives all functionals annihilating its inverse image. Neither the map nor either vector space needs to be finite-dimensional.

noncomputable def LinearMap.kerDualMapEquiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : ↥f.dualMap.ker ≃ₗ[R] Module.Dual R (N ⧸ f.range)

The kernel of the dual map f^* is the dual of the cokernel of f: a functional on N vanishing on range f is a functional on N ⧸ range f.

@[simp]

theorem LinearMap.kerDualMapEquiv_apply_mk {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (φ : ↥f.dualMap.ker) (n : N) : (f.kerDualMapEquiv φ) (Submodule.Quotient.mk n) = ↑φ n

@[simp]

theorem LinearMap.coe_kerDualMapEquiv_symm {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (ψ : Module.Dual R (N ⧸ f.range)) : ↑(f.kerDualMapEquiv.symm ψ) = ψ ∘ₗ f.range.mkQ

noncomputable def LinearMap.cokerDualMapEquiv {K : Type u_1} {M : Type u_2} {N : Type u_3} [Field K] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] (f : M →ₗ[K] N) : (Module.Dual K M ⧸ f.dualMap.range) ≃ₗ[K] Module.Dual K ↥f.ker

The cokernel of the dual map f^* is the dual of the kernel of f: the class of a functional on M modulo range f^* is its restriction to ker f.

@[simp]

theorem LinearMap.cokerDualMapEquiv_mk_apply {K : Type u_1} {M : Type u_2} {N : Type u_3} [Field K] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] (f : M →ₗ[K] N) (θ : Module.Dual K M) (u : ↥f.ker) : (f.cokerDualMapEquiv (Submodule.Quotient.mk θ)) u = θ ↑u

theorem LinearMap.finrank_ker_dualMap_eq_finrank_quotient_range {K : Type u_1} {M : Type u_2} {N : Type u_3} [Field K] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] (f : M →ₗ[K] N) : Module.finrank K ↥f.dualMap.ker = Module.finrank K (N ⧸ f.range)

The finrank of the kernel of f^* equals the finrank of the cokernel of f. When the cokernel is finite-dimensional this says the two spaces have the same dimension.

@[simp]

theorem LinearMap.finrank_quotient_range_dualMap {K : Type u_1} {M : Type u_2} {N : Type u_3} [Field K] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] (f : M →ₗ[K] N) : Module.finrank K (Module.Dual K M ⧸ f.dualMap.range) = Module.finrank K ↥f.ker

The finrank of the cokernel of f^* equals the finrank of the kernel of f. When the kernel is finite-dimensional this says the two spaces have the same dimension.

theorem LinearMap.exists_ne_zero_comp_eq_comp_of_map_ker_ne_top {k : Type u_1} {V : Type u_2} {W : Type u_3} {U : Type u_4} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] [AddCommGroup U] [Module k U] {D : V →ₗ[k] W} {DF : V →ₗ[k] U} (h : Submodule.map DF D.ker ≠ ⊤) : ∃ (f : Module.Dual k U), f ≠ 0 ∧ ∃ (g : Module.Dual k W), f ∘ₗ DF = g ∘ₗ D

Lagrange multipliers, linear-algebra form. If DF does not map the kernel of D onto its codomain, then some nonzero functional f and some functional g satisfy f ∘ DF = g ∘ D.