theorem Q2Presentation.Lifting.exists_dual_ne_zero {M : Type} [AddCommGroup M] [Module (ZMod 2) M] (x : M) (hx : x ≠ 0) : ∃ (θ : M →ₗ[ZMod 2] ZMod 2), θ x = 1

A nonzero vector of an F₂-module admits a functional hitting 1.

theorem Q2Presentation.Lifting.le_of_dual_vanish {M : Type} [AddCommGroup M] [Module (ZMod 2) M] [Finite M] (V W : Submodule (ZMod 2) M) (h : ∀ (θ : M →ₗ[ZMod 2] ZMod 2), (∀ v ∈ V, θ v = 0) → ∀ w ∈ W, θ w = 0) : W ≤ V

Dual criterion for inclusion: over a finite F₂-module, W ≤ V iff every functional killing V kills W.