instCategoryEtale

Mathlib.AlgebraicGeometry.Morphisms.Etale

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.instCategoryEtale

English

The forgetful functor from étale schemes to schemes is faithful.

Русский

Функтор забывания из этиле-схем к схемам достоверен.

LaTeX

$$$\\text{(Etale.forget X).Faithful}$$$

Lean4

instance : Category X.Etale :=
  inferInstanceAs <| Category (MorphismProperty.Over @IsEtale ⊤ X)

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

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

Разделы

Аффилиация

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