IsStandardSmooth — Mathlib

English

A ring homomorphism f is standard smooth if S is standard smooth as R-algebra.

Русский

Гомоморфизм колец гладок по определению, если S является стандартно гладким как R-алгебра.

LaTeX

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

Lean4

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

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