finitePresentation_isStableUnderBaseChange

English

Finitely presented is stable under base change: if a ring homomorphism is base-changed along another one, the finite-presentation property is preserved.

Русский

Свойство конечного презентирования стабильно при базовых изменениях: если перейти к основанию через другое кольцо, конечнопредставление сохраняется.

LaTeX

$$$\text{IsStableUnderBaseChange }\operatorname{FinitePresentation}.$$$

Lean4

/-- Being finitely-presented is stable under base change. -/
theorem finitePresentation_isStableUnderBaseChange : IsStableUnderBaseChange @FinitePresentation :=
  by
  apply IsStableUnderBaseChange.mk
  · exact finitePresentation_respectsIso
  · introv h
    rw [finitePresentation_algebraMap] at h
    suffices Algebra.FinitePresentation S (S ⊗[R] T) by rw [RingHom.FinitePresentation]; convert this; ext;
      simp_rw [Algebra.smul_def]; rfl
    infer_instance

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