of_isBaseChange — Mathlib

English

If A is a commutative ring, R → A is a base change, and M is finitely presented over R, then A ⊗_R M is finitely presented over A.

Русский

Пусть A — коммутативное кольцо; базисное изменение по R в A; если M FP над R, то A ⊗_R M FP над A.

LaTeX

$$$\text{IsBaseChange } A f \Rightarrow \text{Module.FinitePresentation } R M \Rightarrow \text{Module.FinitePresentation } A (A \otimes_R M)$$$

Lean4

theorem of_isBaseChange {A} [CommRing A] [Algebra R A] [Module A N] [IsScalarTower R A N] (f : M →ₗ[R] N)
    (h : IsBaseChange A f) [Module.FinitePresentation R M] : Module.FinitePresentation A N :=
  Module.finitePresentation_of_surjective h.equiv.toLinearMap h.equiv.surjective (by simpa using Submodule.fg_bot)

Похожие утверждения