isStandardSmoothOfRelativeDimension_isStableUnderBaseChange

English

IsStableUnderBaseChange (@IsStandardSmoothOfRelativeDimension n).

Русский

IsStableUnderBaseChange для @IsStandardSmoothOfRelativeDimension n.

LaTeX

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

Lean4

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

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