to_unramified

Mathlib.RingTheory.Etale.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

instance (priority := 100) to_unramified [h : FormallyEtale R A] : FormallyUnramified R A :=
  (FormallyEtale.iff_unramified_and_smooth.mp h).1

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

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

Разделы

Аффилиация

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