faithful — Mathlib

English

Naturality of toSpecΓ with respect to morphisms: for f: X ⟶ Y, f ≫ Y.toSpecΓ = X.toSpecΓ ≫ Spec.map (f.appTop).

Русский

Натуральность toSpecΓ по отношению к морфизмам: для f: X ⟶ Y выполняется f ≫ Y.toSpecΓ = X.toSpecΓ ≫ Spec.map (f.appTop).

LaTeX

$$f ≫ Y.toSpecΓ = X.toSpecΓ ≫ Spec.map (f.appTop)$$

Lean4

/-- Spec is a faithful functor. -/
instance faithful : Scheme.Spec.Faithful :=
  Spec.fullyFaithful.faithful

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