Etale

Mathlib.AlgebraicGeometry.Morphisms.Etale

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

English

The forgetful functor from objects with étale morphisms is full.

Русский

Функтор забывания из объектов с étale-морфизмами полон.

LaTeX

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

Lean4

/-- The category `Etale X` is the category of schemes étale over `X`. -/
def Etale (X : Scheme.{u}) : Type _ :=
  MorphismProperty.Over @IsEtale ⊤ X

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

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

Разделы

Аффилиация

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