FormallySmooth — Mathlib

English

A ring homomorphism f: R → S is formally smooth exactly when S, with its natural R-algebra structure, is formally smooth as an R-algebra.

Русский

Гомоморфизм колец f: R → S формально гладок тогда, когда S, рассматриваемое как R-алгебра, формально гладко над R.

LaTeX

$$$\mathrm{FormallySmooth}(f) \;\coloneqq\; \mathrm{Algebra.FormallySmooth}(R,S)$$$

Lean4

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

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