Smooth — Mathlib

English

A ring homomorphism is smooth if the target is smooth as an algebra over the source.

Русский

Гомоморфизм колец гладок тогда, когда целое кольцо является гладким как алгебра над исходным кольцом.

LaTeX

$$$\mathrm{Smooth}(f) \;\Longleftrightarrow\; \mathrm{Algebra.Smooth}(R,S)$$$

Lean4

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

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