baseChange — Mathlib

English

An instance showing that base change respects standard smoothness with localization for modules.

Русский

Инстанс демонстрирует сохранение стандартной гладкости при базовом изменении с локализацией модулей.

LaTeX

$$$[IsStandardSmooth R S] \Rightarrow [IsStandardSmooth R (S \otimes_R T)]$$$

Lean4

instance baseChange [IsStandardSmooth R S] : IsStandardSmooth T (T ⊗[R] S) where
  out := by
    obtain ⟨ι, σ, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
    exact ⟨ι, σ, _, inferInstance, ⟨P.baseChange T⟩⟩

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