English
Let V be a vector space over a field K. There is a contravariant lattice isomorphism between the family of subspaces W ⊆ V with finite codimension (equivalently FiniteDimensional of V/W) and the family of finite-dimensional subspaces of the dual space V*, given by W ↦ W⊥ and the inverse sends U ⊆ V* to U⊥. This correspondence reverses inclusion.
Русский
Пусть V — векторное пространство над полем K. Существует антигомоморфная изоморфия решёток между множеством подпространств W ⊆ V конечной кодименности и множеством конечномерных подпространств в сопряжённом пространстве V*, задаваемая W ↦ W⊥, и обратная стрелка отправляет подпространство U ⊆ V* в U⊥. Взаимно включения обращаются.
LaTeX
$$$$\\{W \\le V \\mid \\operatorname{codim}(W) < \\infty\\} \\cong_o \\{U \\le V^* \\mid \\dim U < \\infty\\}^{op},\\quad W \\mapsto W^{\\perp},\\ U \\mapsto U^{\\perp}.$$$$
Lean4
/-- For any vector space, `dualAnnihilator` and `dualCoannihilator` gives an antitone order
isomorphism between the finite-codimensional subspaces in the vector space and the
finite-dimensional subspaces in its dual. -/
def orderIsoFiniteCodimDim :
{ W : Subspace K V // FiniteDimensional K (V ⧸ W) } ≃o { W : Subspace K (Dual K V) // FiniteDimensional K W }ᵒᵈ
where
toFun W := toDual ⟨W.1.dualAnnihilator, Submodule.finite_dualAnnihilator_iff.mpr W.2⟩
invFun W := ⟨(ofDual W).1.dualCoannihilator, finiteDimensional_quot_dualCoannihilator_iff.mpr (ofDual W).2⟩
left_inv _ := Subtype.ext dualAnnihilator_dualCoannihilator_eq
right_inv
W :=
have := (ofDual W).2;
Subtype.ext dualCoannihilator_dualAnnihilator_eq
map_rel_iff' := dualAnnihilator_le_dualAnnihilator_iff
