isStandardSmooth_isStableUnderBaseChange

English

IsStandardSmoothOfRelativeDimension n is stable under base change.

Русский

IsStandardSmoothOfRelativeDimension n устойчива к базовым изменениям.

LaTeX

$$$$ \operatorname{IsStableUnderBaseChange}(\operatorname{IsStandardSmoothOfRelativeDimension}(n)). $$$$

Lean4

theorem isStandardSmooth_isStableUnderBaseChange : IsStableUnderBaseChange @IsStandardSmooth :=
  by
  apply IsStableUnderBaseChange.mk
  · exact isStandardSmooth_respectsIso
  · introv h
    replace h : Algebra.IsStandardSmooth R T := by rw [RingHom.IsStandardSmooth] at h; convert h; ext;
      simp_rw [Algebra.smul_def]; rfl
    suffices Algebra.IsStandardSmooth S (S ⊗[R] T) by rw [RingHom.IsStandardSmooth]; convert this; ext;
      simp_rw [Algebra.smul_def]; rfl
    infer_instance

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