evaluation_naturality_apply — Mathlib

English

A specialized form of naturality showing compatibility of residue field maps with evaluations on sections.

Русский

Уточненная форма естественности, демонстрирующая совместимость карт резидуум с оценками секций.

LaTeX

$$$$ f.\mathrm{residueFieldMap}(x) (Y.\mathrm{Γevaluation}(f. base x, a)) = X.\mathrm{evaluation}(f.^{-1}V, x, \text{?}) $$$$

Lean4

theorem evaluation_naturality_apply {V : Opens Y} (x : X) (hx : f.base x ∈ V) (s) :
    f.residueFieldMap x (Y.evaluation V (f.base x) hx s) = X.evaluation (f ⁻¹ᵁ V) x hx (f.app V s) :=
  LocallyRingedSpace.evaluation_naturality_apply f.1 ⟨x, hx⟩ s

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