English
If 0 → M → N → P → 0 is exact, N is finitely presented, and P is projective, then M is finitely presented.
Русский
Если точная последовательность 0 → M → N → P → 0, N FP, и P проектен, тогда M FP.
LaTeX
$$$\text{If } f: M \to N,\ g: N \to P, \text{ with } 0\to M\to N\to P\to 0 \text{ exact and } P \text{ projective, then } M \text{ FP}$$$
Lean4
/-- Given an exact sequence `0 → M → N → P → 0`
with `N` finitely presented and `P` projective, then `M` is also finitely presented. -/
theorem finitePresentation_of_projective_of_exact {P : Type*} [AddCommGroup P] [Module R P]
[Module.FinitePresentation R N] [Module.Projective R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hf : Function.Injective f)
(hg : Function.Surjective g) (H : Function.Exact f g) : Module.FinitePresentation R M :=
have ⟨l, hl⟩ := Module.projective_lifting_property g .id hg
Module.finitePresentation_of_split_exact f g l hl hf H
