colimitPresheafObjIsoComponentwiseLimit_inv_ι_app

English

The inverse of the componentwise colimit is compatible with the injections from the diagram.

Русский

Обратный элемент кокомпонентному колимиту совместим с инъекциями диаграммы.

LaTeX

$$$(\operatorname{colimitPresheafObjIsoComponentwiseLimit} F U)^{-1} \circ (\operatorname{colimit}.\iota F j)_{c.app(\mathrm{op} U)} = \lim (\mathrm{π})$$$

Lean4

@[simp]
theorem colimitPresheafObjIsoComponentwiseLimit_inv_ι_app (F : J ⥤ PresheafedSpace.{_, _, v} C)
    (U : Opens (Limits.colimit F).carrier) (j : J) :
    (colimitPresheafObjIsoComponentwiseLimit F U).inv ≫ (colimit.ι F j).c.app (op U) = limit.π _ (op j) :=
  by
  delta colimitPresheafObjIsoComponentwiseLimit
  rw [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)]
  dsimp
  rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc,
    congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc]
  erw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc]
  simp

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