evaluation_naturality — Mathlib

English

For a morphism f: X→Y of LocallyRingedSpaces and an open V in Y, the evaluation map commutes with the residue-field map: the evaluation at the image equals the pullback of evaluation along f.

Русский

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

LaTeX

$$$Y.evaluation\langle f.base x, x.property\rangle \; \gg\; residueFieldMap f x.val = f.c.app (op V) \; \gg\; X.evaluation x$$$

Lean4

@[reassoc]
theorem evaluation_naturality {V : Opens Y} (x : (Opens.map f.base).obj V) :
    Y.evaluation ⟨f.base x, x.property⟩ ≫ residueFieldMap f x.val = f.c.app (op V) ≫ X.evaluation x :=
  by
  dsimp only [LocallyRingedSpace.evaluation, LocallyRingedSpace.residueFieldMap]
  rw [Category.assoc]
  ext a
  simp only [CommRingCat.comp_apply]
  erw [IsLocalRing.ResidueField.map_residue]
  rw [LocallyRingedSpace.stalkMap_germ_apply]
  rfl

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