formallySmooth_algebraMap — Mathlib

English

For rings R,S with an algebra structure, the map algebraMap R S is formally smooth if and only if S is formally smooth as an R-algebra.

Русский

Пусть есть алгебраическая структура R→S; тогда algebraMap R S формально гладок тогда и только тогда, когда S формально гладко над R.

LaTeX

$$$\big( \text{algebraMap } R S \big).\mathrm{FormallySmooth} \iff \mathrm{Algebra.FormallySmooth}(R,S)$$$

Lean4

theorem formallySmooth_algebraMap [Algebra R S] : (algebraMap R S).FormallySmooth ↔ Algebra.FormallySmooth R S := by
  rw [FormallySmooth, toAlgebra_algebraMap]

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