English
Let R be a commutative semiring and M an R-module which is finite and projective. Then its dual M* = Hom_R(M, R) is finite as an R-module.
Русский
Пусть R — коммутативное полугруппа, а M — модуль над R, который конечно порождается и проективен. Тогда его двойственный модуль M* = Hom_R(M, R) является конечным как R-модуль.
LaTeX
$$$M^{\\ast}$ is a finite $R$-module.$$
Lean4
instance dual_finite [Projective R M] : Module.Finite R (Dual R M) :=
have ⟨n, f, g, _, _, hfg⟩ := Finite.exists_comp_eq_id_of_projective R M
have := Finite.of_basis (Free.chooseBasis R <| Fin n → R).dualBasis
.of_surjective _ (surjective_of_comp_eq_id f.dualMap g.dualMap <| congr_arg dualMap hfg)
