finitePresentation — Mathlib

English

Under localization away from f, the standard smoothness property is preserved across the base-change.

Русский

При локализации Away от f свойство гладкости сохраняется при базовом изменении.

LaTeX

$$$\text{baseChange}(\text{IsStandardSmooth}, S, T) \Rightarrow \text{IsStandardSmooth}(T, T \otimes_R S)$$$

Lean4

instance (priority := 100) finitePresentation [IsStandardSmooth R S] : FinitePresentation R S :=
  by
  obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
  exact P.finitePresentation_of_isFinite

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