evaluation_naturality_apply — Mathlib

English

The evaluation maps are natural in the base schemes: given a morphism f: X → Y and an appropriate open V in Y, the evaluation commutes with the base change along f.

Русский

Оценочные отображения натурализованы по базису: для гомоморфизма f: X → Y и подходящего открытого V в Y, равномерное отображение коммутирует с базовым изменением по f.

LaTeX

$$$ Y.\\mathrm{evaluation} \\circ (f.base) = f.c.app (op V) \\circ X.\\mathrm{evaluation} $$$

Lean4

theorem evaluation_naturality_apply {V : Opens Y} (x : (Opens.map f.base).obj V) (a : Y.presheaf.obj (op V)) :
    residueFieldMap f x.val (Y.evaluation ⟨f.base x, x.property⟩ a) = X.evaluation x (f.c.app (op V) a) := by
  simpa using congrFun (congrArg (DFunLike.coe ∘ CommRingCat.Hom.hom) <| evaluation_naturality f x) a

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