English
There exists a finitely generated submodule K of a finite free module L such that M is isomorphic to the quotient L/K.
Русский
Существует конечно порожденный подпроимодуль K под конечной свободной модулем L так, что M ~ L/K.
LaTeX
$$$\exists L\; (\text{AddCommGroup } L)\; (\text{Module } R L)\; (K : Submodule R L)\; (M \simeq_R L / K),\; \ Module.Free R L \land Module.Finite R L \land K.FG$$$
Lean4
theorem exists_fin [fp : Module.FinitePresentation R M] :
∃ (n : ℕ) (K : Submodule R (Fin n → R)) (_ : M ≃ₗ[R] (Fin n → R) ⧸ K), K.FG :=
by
have ⟨ι, ⟨hι₁, hι₂⟩⟩ := fp
refine
⟨_,
LinearMap.ker
(linearCombination R Subtype.val ∘ₗ
(lcongr ι.equivFin (.refl ..) ≪≫ₗ linearEquivFunOnFinite R R _).symm.toLinearMap),
(LinearMap.quotKerEquivOfSurjective _ <| LinearMap.range_eq_top.mp ?_).symm, ?_⟩
· simpa [range_linearCombination] using hι₁
· simpa [LinearMap.ker_comp, Submodule.comap_equiv_eq_map_symm] using hι₂.map _
