yoneda_toGlued_yonedaGluedToSheaf

English

The Yoneda image of the glued map factors to the original open immersion data, i.e., the Yoneda image of toGlued composed with the glue-to-sheaf map equals f_i.

Русский

Образ по Янове склейки факторизуется по данным открытого вложения: yoneda.map(toGlued hf i) затем glue-to-sheaf равно f_i.

LaTeX

$$$\\yoneda.map (toGlued\\;hf\\;i) \\;\\gg\\; (\\yonedaGluedToSheaf\\;hf).val = f_i$$$

Lean4

@[reassoc (attr := simp)]
theorem yoneda_toGlued_yonedaGluedToSheaf (i : ι) : yoneda.map (toGlued hf i) ≫ (yonedaGluedToSheaf hf).val = f i :=
  by
  apply yonedaEquiv.injective
  rw [yonedaGluedToSheaf, yonedaEquiv_apply, yonedaEquiv_apply, FunctorToTypes.comp, yoneda_map_app, id_comp,
    yonedaEquiv_symm_app_apply]
  apply GlueData.sheafValGluedMk_val

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