English
If C has an initial object and c is a Van Kampen cocone on a cofan F, then for any two distinct indices i ≠ j, the pullback of the two initial morphisms to X_i and X_j is realized as the pullback of the corresponding injections from the cocone.
Русский
Пусть в C есть начальный объект и c — когон ван-Кемпена на кофане F. Для любых i ≠ j, соответствующий пуллбак двух начальных отображений в X_i и X_j совпадает с пуллбаком иньекций cofano.
LaTeX
$$$\\mathrm{IsPullback}\\Bigl(P := (\\text{if } j=i \\text{ then } X_i \\text{ else } \\bot_C),\\; \\text{if } h:\\ j=i \\text{ then } \\mathrm{eqToHom}(\\text{if_pos } h) \\text{ else } \\mathrm{eqToHom}(\\text{if_neg } h) \\; \\overset{initial}{to}(X_i),\\; \\text{if } h:\\ j=i \\text{ then } \\mathrm{eqToHom}((\\text{if_pos } h).trans (\\congr_arg X h.symm)) \\text{ else } \\mathrm{eqToHom}(\\text{if_neg } h) \\; \\overset{initial}{to}(X_j)\\Bigr) $$
Lean4
theorem isPullback_initial_to_of_cofan_isVanKampen [HasInitial C] {ι : Type*} {F : Discrete ι ⥤ C} {c : Cocone F}
(hc : IsVanKampenColimit c) (i j : Discrete ι) (hi : i ≠ j) :
IsPullback (initial.to _) (initial.to _) (c.ι.app i) (c.ι.app j) := by
classical
let f : ι → C := F.obj ∘ Discrete.mk
have : F = Discrete.functor f := Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
clear_value f
subst this
have : ∀ i, Subsingleton (⊥_ C ⟶ (Discrete.functor f).obj i) := inferInstance
convert isPullback_of_cofan_isVanKampen hc i.as j.as
exact (if_neg (mt Discrete.ext hi.symm)).symm
