English
For a surjective linear map l: M → N, kernel FG iff N is finitely presented.
Русский
Для сюръективного линейного отображения l: M → N, Ker(l) FG ↔ N FP.
LaTeX
$$$[Module.FinitePresentation R M] (l : M \to N) (hl : Function.Surjective l) : Submodule.FG (LinearMap.ker l) \iff Module.FinitePresentation R N$$$
Lean4
theorem trans (S : Type*) [CommRing S] [Algebra R S] [Module S M] [IsScalarTower R S M] [Module.FinitePresentation R S]
[Module.FinitePresentation S M] : Module.FinitePresentation R M :=
by
obtain ⟨n, K, e, hK⟩ := Module.FinitePresentation.exists_fin S M
let f : (Fin n → S) →ₗ[R] M := (e.symm ∘ₗ K.mkQ).restrictScalars R
refine Module.finitePresentation_of_surjective f (fun m ↦ ?_) ?_
· obtain ⟨a, ha⟩ := K.mkQ_surjective (e m)
exact ⟨a, by simp [f, ha]⟩
· have : Module.Finite S (Submodule.restrictScalars R (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ))) :=
by
change Module.Finite S (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ))
simpa [Finite.iff_fg]
simp only [f, LinearMap.ker_restrictScalars, ← Module.Finite.iff_fg]
exact Module.Finite.trans S _
