to_smooth

Mathlib.RingTheory.Etale.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.FormallyEtale.to_smooth

English

If a morphism is formally étale, then it is formally smooth.

Русский

Если отображение формально étale, то оно формально гладкое.

LaTeX

$$$\text{FormallyEtale}(R,A) \Rightarrow \text{FormallySmooth}(R,A)$$$

Lean4

instance (priority := 100) to_smooth [h : FormallyEtale R A] : FormallySmooth R A :=
  (FormallyEtale.iff_unramified_and_smooth.mp h).2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru