finitePresentation_of_projective — Mathlib

English

If a module M is projective and finitely generated, then M is finitely presented.

Русский

Если модуль M проектен и конечно порожден, то он конечнопредставим.

LaTeX

$$$[Module.Projective R M][Module.Finite R M] : FinitePresentation R M$$$

Lean4

theorem finitePresentation_of_projective [Projective R M] [Module.Finite R M] : FinitePresentation R M :=
  have ⟨_n, _f, _g, surj, _, hfg⟩ := Finite.exists_comp_eq_id_of_projective R M
  Module.finitePresentation_of_free_of_surjective _ surj
    (Finite.iff_fg.mp <| LinearMap.ker_eq_range_of_comp_eq_id hfg ▸ inferInstance)

Похожие утверждения