instFaithfulEtaleOverForget

Mathlib.AlgebraicGeometry.Morphisms.Etale

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

English

The forgetful functor from étale schemes is faithful (reiterated).

Русский

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

LaTeX

$$$\\text{instFaithfulEtaleOverForget}$$$

Lean4

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

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

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

Разделы

Аффилиация

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