forget

Mathlib.AlgebraicGeometry.Morphisms.Etale

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

← MathLib Explorer

English

The category of étale morphisms over X has pullbacks along any map.

Русский

Категория étale-морфизмов над X имеет обратно-пересечения по любому отображению.

LaTeX

$$$\\forall X, HasPullbacks X.Etale$$$

Lean4

/-- The forgetful functor from schemes étale over `X` to schemes over `X`. -/
def forget : X.Etale ⥤ Over X :=
  MorphismProperty.Over.forget @IsEtale ⊤ X

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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