English
For a Free K-vector space V, V* is finite iff V is finite.
Русский
Пусть V — свободное векторное пространство над K. Его двойственный V* конечен тогда и только тогда, когда V конечен.
LaTeX
$$[Free K V] : Finite(K, V*) $\\iff$ Finite(K, V)$$
Lean4
/-- For an example of a non-free projective `K`-module `V` for which the forward implication
fails, see https://stacks.math.columbia.edu/tag/05WG#comment-9913. -/
theorem finite_dual_iff [Free K V] : Module.Finite K (Dual K V) ↔ Module.Finite K V :=
by
refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
have ⟨⟨ι, b⟩⟩ := Free.exists_basis (R := K) (M := V)
cases finite_or_infinite ι
· exact .of_basis b
nontriviality K
have ⟨n, hn⟩ := Module.Finite.exists_nat_not_surjective K (Dual K V)
let g := Finsupp.llift K K K ι ≪≫ₗ b.repr.dualMap
exact
hn (LinearMap.funLeft K K (Fin.valEmbedding.trans (Infinite.natEmbedding ι)) ∘ₗ _)
((Function.Embedding.injective _).surjective_comp_right.comp g.symm.surjective) |>.elim
