forgetToScheme_faithful — Mathlib

English

The forgetful functor from affine schemes to schemes is faithful.

Русский

Функтор забывания из категории аффинных схем в категорию схем верен (веренность функтору).

LaTeX

$$$$ \forall X,Y\,\forall f,g: X\to Y,\ \operatorname{forgetToScheme}(f)=\operatorname{forgetToScheme}(g) \Rightarrow f=g. $$$$

Lean4

instance forgetToScheme_faithful : forgetToScheme.Faithful :=
  inferInstanceAs Scheme.Spec.essImage.ι.Faithful

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