germ_res — Mathlib

English

Compatibility of germ maps under composition of morphisms yields the expected commutativity relation.

Русский

Совместимость отображений герм под композициями отображений дает ожидаемое соотношение коммутативности.

LaTeX

$$$$ germ\_res (F) \;: \; F.map i^{op} \circ germ = germ \circ F.map i^{op}.$$$$

Lean4

@[reassoc]
theorem germ_res (F : X.Presheaf C) {U V : Opens X} (i : U ⟶ V) (x : X) (hx : x ∈ U) :
    F.map i.op ≫ F.germ U x hx = F.germ V x (i.le hx) :=
  let i' : (⟨U, hx⟩ : OpenNhds x) ⟶ ⟨V, i.le hx⟩ := i
  colimit.w ((OpenNhds.inclusion x).op ⋙ F) i'.op

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