isPullback_initial_to_binaryCofan

English

In a finitary extensive category, for any binary cocone c on objects X and Y that is a colimit, the square formed by the two canonical maps from X and Y to the apex is a pullback square with the two legs given by c.inl and c.inr.

Русский

В конечной расширяющейся категории квадрат, образованный двумя каноническими отображениями X → c.pt и Y → c.pt к вершине c.pt, является пуллбек-квадратом с ножками c.inl и c.inr.

LaTeX

$$$IsPullback\bigl( initial.to X\bigr)\;\;\bigl( initial.to Y\bigr)\;\; c.inl\; c.inr$$$

Lean4

theorem isPullback_initial_to_binaryCofan [FinitaryExtensive C] {c : BinaryCofan X Y} (hc : IsColimit c) :
    IsPullback (initial.to _) (initial.to _) c.inl c.inr :=
  BinaryCofan.isPullback_initial_to_of_isVanKampen (FinitaryExtensive.vanKampen c hc)

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