Gluing and extending linear functionals

This file isolates the linear-algebra step used by the cotrace construction of a Weil functional. A functional on a subspace U which vanishes on U ∩ V glues with the zero functional on V; over a field the glued functional then extends to the ambient vector space.

theorem BGS.HasseWeil.exists_linearMap_extending_eq_zero_on {k : Type u_1} {E : Type u_2} {F : Type u_3} [Field k] [AddCommGroup E] [Module k E] [AddCommGroup F] [Module k F] (U V : Submodule k E) (f : ↥U →ₗ[k] F) (hUV : ∀ (x : ↥U), ↑x ∈ V → f x = 0) : ∃ (g : E →ₗ[k] F), g ∘ₗ U.subtype = f ∧ V ≤ g.ker

A linear map on U which vanishes whenever its argument also lies in V extends to the ambient space while vanishing on all of V.

theorem BGS.HasseWeil.exists_linearMap_extending_eq_zero_on_inf {k : Type u_1} {E : Type u_2} {F : Type u_3} [Field k] [AddCommGroup E] [Module k E] [AddCommGroup F] [Module k F] (U V : Submodule k E) (f : ↥U →ₗ[k] F) (hUV : ∀ (x : ↥(U ⊓ V)), f ⟨↑x, ⋯⟩ = 0) : ∃ (g : E →ₗ[k] F), g ∘ₗ U.subtype = f ∧ V ≤ g.ker

Intersection-subtype form of exists_linearMap_extending_eq_zero_on.

theorem BGS.HasseWeil.exists_ne_zero_linearMap_extending_eq_zero_on_inf {k : Type u_1} {E : Type u_2} {F : Type u_3} [Field k] [AddCommGroup E] [Module k E] [AddCommGroup F] [Module k F] (U V : Submodule k E) (f : ↥U →ₗ[k] F) (hUV : ∀ (x : ↥(U ⊓ V)), f ⟨↑x, ⋯⟩ = 0) (hf : f ≠ 0) : ∃ (g : E →ₗ[k] F), g ∘ₗ U.subtype = f ∧ V ≤ g.ker ∧ g ≠ 0

If the original functional is nonzero, the ambient extension can be chosen nonzero as well.