instFullEtaleOverForget

Mathlib.AlgebraicGeometry.Morphisms.Etale

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

English

For any X, the étale category over X has pullbacks.

Русский

Для любой X, категория Étale над X имеет пулабэки.

LaTeX

$$$\\forall X\\; HasPullbacks X.Etale$$$

Lean4

instance : (Etale.forget X).Full :=
  inferInstanceAs <| (MorphismProperty.Comma.forget _ _ _ _ _).Full

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

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

Разделы

Аффилиация

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