map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv

English

Forward congruence: if two colimit descriptors are equal, then their images under G are equal via isoObjCoconePointsOfIsColimit

Русский

Впереди конгруэнции: если два описателя колимита равны, то их образы под G равны через isoObjCoconePointsOfIsColimit

LaTeX

$$$\\forall c1,c2,c3 \\; (hc1 \\; hc2 \\; hc3) \\; Eq\\; (PreservesColimit₂.isoObjCoconePointsOfIsColimit G hc1 hc2 hc3) (PreservesColimit₂.isoObjCoconePointsOfIsColimit G hc1' hc2' hc3')$$$

Lean4

/-- Characterize the forward direction of the isomorphism
`PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂` w.r.t. the canonical maps to the colimit. -/
@[reassoc (attr := simp)]
theorem map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv (j : J₁ × J₂) :
    (G.map (colimit.ι K₁ j.1)).app (K₂.obj j.2) ≫
        (G.obj <| colimit K₁).map (colimit.ι K₂ j.2) ≫
          (PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ K₁ K₂ G).inv =
      colimit.ι (uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G)) j :=
  map_ι_comp_isoObjConePointsOfIsColimit_hom G (colimit.isColimit _) (colimit.isColimit _) (colimit.isColimit _) j

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