isPullback_initial_to — Mathlib

English

For a finitary extensive C, the pullback of initial maps along Sigma.ι is again a pullback square.

Русский

Для конечной расширяемой C вытягивание начальных отображений вдоль Sigma.ι образует пуллбек-квадрат.

LaTeX

$$$IsPullback(\mathrm{initial.to} (X i),\mathrm{initial.to} (X j), \Sigma.ι X i, \Sigma.ι X j)$$$

Lean4

theorem isPullback_initial_to [FinitaryExtensive C] {ι : Type*} [Finite ι] {F : Discrete ι ⥤ C} {c : Cocone F}
    (hc : IsColimit c) (i j : Discrete ι) (e : i ≠ j) :
    IsPullback (initial.to _) (initial.to _) (c.ι.app i) (c.ι.app j) :=
  isPullback_initial_to_of_cofan_isVanKampen (isVanKampen_finiteCoproducts hc) i j e

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