evaluation_naturality — Mathlib

English

Natural compatibility of the evaluation with morphisms of schemes: the evaluation maps commute with the residue field maps up to pullback.

Русский

Естественная совместимость оценивания со спектрами отображений: оценки коммутируют с картами резидуемого поля через обратные отображения.

LaTeX

$$$$ Y.\mathrm{evaluation}(V, f.\mathrm{base} x, hx) \circ f.\mathrm{residueFieldMap}(x) = f.\mathrm{app}V \circ X.\mathrm{evaluation}(f^{-1}V, x, hx). $$$$

Lean4

@[reassoc]
theorem evaluation_naturality {V : Opens Y} (x : X) (hx : f.base x ∈ V) :
    Y.evaluation V (f.base x) hx ≫ f.residueFieldMap x = f.app V ≫ X.evaluation (f ⁻¹ᵁ V) x hx :=
  LocallyRingedSpace.evaluation_naturality f.1 ⟨x, hx⟩

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