English
For any subspace W of V, the double annihilator in V** equals the image of W under the natural evaluation map ev_V: V → V**; i.e., (W⊥)⊥ = ev_V(W).
Русский
Для подпространства W пространства V двойной аннигилятор в V** совпадает с образом W через естественное отображение схождения ev_V: V → V**; тождество (W⊥)⊥ = ev_V(W).
LaTeX
$$$$ (W^{\\perp})^{\\perp} = \\mathrm{ev}_V(W) \\subseteq V^{**}. $$$$
Lean4
theorem dualAnnihilator_dualAnnihilator_eq_map (W : Subspace K V) [FiniteDimensional K W] :
W.dualAnnihilator.dualAnnihilator = W.map (Dual.eval K V) :=
by
let e1 := (Free.chooseBasis K W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
haveI := e1.finiteDimensional
let e2 := (Free.chooseBasis K _).toDualEquiv ≪≫ₗ W.dualAnnihilator.dualQuotEquivDualAnnihilator
haveI := LinearEquiv.finiteDimensional (V₂ := W.dualAnnihilator.dualAnnihilator) e2
rw [eq_of_le_of_finrank_eq (map_le_dualAnnihilator_dualAnnihilator W)]
rw [← (equivMapOfInjective _ (eval_apply_injective K (V := V)) W).finrank_eq, e1.finrank_eq]
exact e2.finrank_eq
