English
If f: M → N exhibits a base change along A, and M is finitely presented over R, then N is finitely presented over A.
Русский
Если существует базисное изменение вдоль A для отображения f: M → N и M FP над R, тогда N FP над A.
LaTeX
$$$\text{FinitePresentation } R M \wedge IsBaseChange A f \Rightarrow Module.FinitePresentation A N$$$
Lean4
instance {A} [CommRing A] [Algebra R A] [Module.FinitePresentation R M] : Module.FinitePresentation A (A ⊗[R] M) := by
classical
obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
have inst := Module.finitePresentation_of_projective A (A ⊗[R] (Fin n → R))
apply Module.finitePresentation_of_surjective (f.baseChange A) (LinearMap.lTensor_surjective A hf)
have : Function.Exact ((LinearMap.ker f).subtype.baseChange A) (f.baseChange A) :=
lTensor_exact A f.exact_subtype_ker_map hf
rw [LinearMap.exact_iff] at this
rw [this, ← Submodule.map_top]
apply Submodule.FG.map
have : Module.Finite R (LinearMap.ker f) := ⟨(Submodule.fg_top _).mpr (Module.FinitePresentation.fg_ker f hf)⟩
exact Module.Finite.fg_top (R := A) (M := A ⊗[R] LinearMap.ker f)
