English
If M is finitely generated and projective over R, then its dual Module.Dual(R,M) is also projective over R.
Русский
Если M существенно проектируемо над R и конечно порожден, то дуальное пространство M^* является проективным над R.
LaTeX
$$$ [\\text{Module.Finite } R M] \\;\\land\\; [\\text{Module.Projective } R M] \\Rightarrow [\\text{Projective } R (\\mathrm{Module.Dual} \\; R \\; M)] $$$
Lean4
/-- A vector space over a field is isomorphic to its dual if and only if it is finite-dimensional:
a consequence of the Erdős-Kaplansky theorem. -/
theorem linearEquiv_dual_iff_finiteDimensional [Field K] [AddCommGroup V] [Module K V] :
Nonempty (V ≃ₗ[K] Dual K V) ↔ FiniteDimensional K V :=
by
refine ⟨fun ⟨e⟩ ↦ ?_, fun h ↦ ⟨(Module.Free.chooseBasis K V).toDualEquiv⟩⟩
rw [FiniteDimensional, ← Module.rank_lt_aleph0_iff]
by_contra!
apply (lift_rank_lt_rank_dual this).ne
have := e.lift_rank_eq
rwa [lift_umax, lift_id'.{uV}] at this
