English
There exists a finitely presented quotient representation M ≅ L/K with L finite free and K finitely generated.
Русский
Существует запись M ≅ L/K, где L — конечно свободный модуль, а K — FG; то есть M finitely presented.
LaTeX
$$$\exists L\; (\text{AddCommGroup } L)\; (\text{Module } R L)\; (K : Submodule R L)\; (M \simeq_R L / K) \land (\text{Module.Free } R L) \land (\text{Module.Finite } R L) \land K.FG$$$
Lean4
/-- A finitely presented module is isomorphic to the quotient of a finite free module by a finitely
generated submodule. -/
theorem equiv_quotient [Module.FinitePresentation R M] [Small.{v} R] :
∃ (L : Type v) (_ : AddCommGroup L) (_ : Module R L) (K : Submodule R L) (_ : M ≃ₗ[R] L ⧸ K),
Module.Free R L ∧ Module.Finite R L ∧ K.FG :=
have ⟨_n, _K, e, fg⟩ := Module.FinitePresentation.exists_fin R M
let es := Shrink.linearEquiv
⟨_, inferInstance, inferInstance, _, e ≪≫ₗ Submodule.Quotient.equiv _ _ (es ..).symm rfl, .of_equiv (es ..).symm,
.equiv (es ..).symm, fg.map (es ..).symm.toLinearMap⟩
