colimitPointwiseProductToProductColimit_app

English

The colimit pointwise product to product colimit is an isomorphism in the isomorphic context of IsFiltered and Discrete index.

Русский

Изоморфизм colimitPointwiseProductToProductColimit существует в контексте IsFiltered и Discrete индексов.

LaTeX

$$IsIso (colimitPointwiseProductToProductColimit F)$$

Lean4

theorem colimitPointwiseProductToProductColimit_app (d : D) :
    (colimitPointwiseProductToProductColimit F).app d =
      (colimitObjIsoColimitCompEvaluation _ _).hom ≫
        (HasColimit.isoOfNatIso (pointwiseProductCompEvaluation F d)).hom ≫
          colimitPointwiseProductToProductColimit _ ≫
            (Pi.mapIso fun _ => (colimitObjIsoColimitCompEvaluation _ _).symm).hom ≫ (piObjIso _ _).inv :=
  by
  rw [← Iso.inv_comp_eq]
  simp only [← Category.assoc]
  rw [Iso.eq_comp_inv]
  refine Pi.hom_ext _ _ (fun s => colimit.hom_ext (fun k => ?_))
  simp [← NatTrans.comp_app]

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