forgetFullyFaithful

Mathlib.AlgebraicGeometry.Morphisms.Etale

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

← MathLib Explorer

English

The forgetful functor from Étale schemes is full and faithful.

Русский

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

LaTeX

$$$\\text{instFullEtaleOverForget} \\Rightarrow \\text{full and faithful}$$$

Lean4

/-- The forgetful functor from schemes étale over `X` to schemes over `X` is fully faithful. -/
def forgetFullyFaithful : (Etale.forget X).FullyFaithful :=
  MorphismProperty.Comma.forgetFullyFaithful _ _ _

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

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

Разделы

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

Аффилиация

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