colimitUncurryIsoColimitCompColim_ι_hom

English

The hom component of the flip-constructed limit iso respects the two projections.

Русский

Гом-компонент изоморфизма предела при перевороте соблюдает две проекции.

LaTeX

$$(limitFlipCompLimIsoLimitCompLim F).hom ∘ limit.π_j ∘ limit.π_k = limit.π_(j,k)$$

Lean4

@[simp, reassoc]
theorem colimitUncurryIsoColimitCompColim_ι_hom {j} {k} :
    colimit.ι _ (j, k) ≫ (colimitUncurryIsoColimitCompColim F).hom =
      (colimit.ι _ k ≫ colimit.ι (F ⋙ colim) j : _ ⟶ (colimit (F ⋙ colim))) :=
  by
  rw [← cancel_mono (colimitUncurryIsoColimitCompColim F).inv]
  simp

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