IsStandardSmoothOfRelativeDimension

English

RingHom.IsStandardSmoothOfRelativeDimension n f is defined as StandardSmoothOfRelativeDimension n for the R-algebra f.toAlgebra.

Русский

RingHom.IsStandardSmoothOfRelativeDimension n f задаётся как стандартная гладкость относительной размерности n для R-алгебры f.toAlgebra.

LaTeX

$$$\mathrm{IsStandardSmoothOfRelativeDimension}(n)(f) \coloneqq \mathrm{Algebra.IsStandardSmoothOfRelativeDimension}(n)(f^{\text{algebra}})$$$

Lean4

/-- A ring homomorphism `R →+* S` is standard smooth of relative dimension `n` if
`S` is standard smooth of relative dimension `n` as `R`-algebra. -/
@[algebraize RingHom.IsStandardSmoothOfRelativeDimension.toAlgebra]
def IsStandardSmoothOfRelativeDimension (f : R →+* S) : Prop :=
  @Algebra.IsStandardSmoothOfRelativeDimension n _ _ _ _ f.toAlgebra

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