colimitPresheafObjIsoComponentwiseLimit_hom_π

English

The hom component of the colimit iso maps to the corresponding projection, via π.

Русский

Гом-компонента колимитного изо отображает соответствующую проекцию через π.

LaTeX

$$$(\operatorname{colimitPresheafObjIsoComponentwiseLimit} F U) \!\!\!\!\!\!\!\! \circ \mathrm{limit}.\pi_{(op j)} = (\operatorname{colimit}.\iota F j).c.app(\mathrm{op} U)$$$

Lean4

@[simp]
theorem colimitPresheafObjIsoComponentwiseLimit_hom_π (F : J ⥤ PresheafedSpace.{_, _, v} C)
    (U : Opens (Limits.colimit F).carrier) (j : J) :
    (colimitPresheafObjIsoComponentwiseLimit F U).hom ≫ limit.π _ (op j) = (colimit.ι F j).c.app (op U) := by
  rw [← Iso.eq_inv_comp, colimitPresheafObjIsoComponentwiseLimit_inv_ι_app]

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