projective_of_finitePresentation — Mathlib

English

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

Русский

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

LaTeX

$$[Flat(R,M)] ∧ [FinitePresentation(R,M)] ⇒ Projective(R,M)$$

Lean4

@[stacks 00NX "(1) → (2)"]
theorem projective_of_finitePresentation [Flat R M] [FinitePresentation R M] : Projective R M :=
  have ⟨_, f, g, eq⟩ := exists_factorization_of_isFinitelyPresented (.id (R := R) (M := M))
  .of_split f g eq.symm

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