stalkMap_congr_point — Mathlib

English

For a morphism f of schemes, the stalk maps at points x, x' with x = x' satisfy a natural congruence with the residue-field isomorphisms.

Русский

Для морфизма схем выполняется естественное тождество стековых отображений в точках x и x', если x = x'.

LaTeX

$$f.stalkMap x ≫ (X.presheaf.stalkCongr (.of_eq hxx')).hom = (Y.presheaf.stalkCongr (.of_eq (| hxx' ▸ rfl))).hom ≫ f.stalkMap x'$$

Lean4

@[reassoc]
theorem stalkMap_congr_point (x x' : X) (hxx' : x = x') :
    f.stalkMap x ≫ (X.presheaf.stalkCongr (.of_eq hxx')).hom =
      (Y.presheaf.stalkCongr (.of_eq <| hxx' ▸ rfl)).hom ≫ f.stalkMap x' :=
  LocallyRingedSpace.stalkMap_congr_point f.toLRSHom x x' hxx'

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