Γevaluation_naturality_apply — Mathlib

English

A more explicit version of naturality for Γ-evaluation applied to a specific element, expressing compatibility across functorial actions and residue fields.

Русский

Более явная формулировка натуральности Γ-оценки при конкретном элементе, выражающая совместимость между действием функторов и остаточными полями.

LaTeX

$$$ (f, x, a) \\mapsto\\; \\text{compatibility relation between } a \\text{ under } f \\text{ and } x $$$

Lean4

theorem Γevaluation_naturality_apply (x : X) (a : Y.presheaf.obj (op ⊤)) :
    residueFieldMap f x (Y.Γevaluation (f.base x) a) = X.Γevaluation x (f.c.app (op ⊤) a) :=
  evaluation_naturality_apply f ⟨x, by simp only [Opens.map_top]; trivial⟩ a

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