ι_evalHom — Mathlib

English

A germ evaluation commutes with the colimit embedding: evaluating after passing to colimits equals evaluating directly on the open neighborhood.

Русский

Оценка эстанциирования совместима с предел-встраиванием: оценка после перехода к колимитам равна оценке непосредственно на открытом окне.

LaTeX

$$colimit.ι ⋯ ≡ smoothSheaf.evalAt$$

Lean4

@[simp, reassoc, elementwise]
theorem ι_evalHom (x : TopCat.of M) (U) :
    colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M N).val) U ≫ smoothSheaf.evalHom IM I N x =
      smoothSheaf.evalAt _ _ _ _ _ :=
  colimit.ι_desc _ _

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