ι_comp_isoColimitUncurryWhiskeringLeft₂_hom

English

Congruence lemma: congruence of isomorphism directions in the PreservesColimit₂ isoObjCoconePointsOfIsColimit

Русский

Лемма эквивалентности: конгруэнтность направлений изоморфизма в PreservesColimit₂ isoObjCoconePointsOfIsColimit

LaTeX

$$$\\text{Eq } \\text{PreservesColimit₂.isoObjCoconePointsOfIsColimit}(G) \\; \\text{cong}_1 \\; \\text{cong}_2$$$

Lean4

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

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