English
If C is finitaryPreExtensive and has finite index inclusions, pullbacks along inclusions exist, and one can build the pullback from a coproduct decomposition.
Русский
Если C — конечнопредExtensive и есть включения с конечной индексной множеством, существуют пуллбэки вдоль включений, и их можно строить через разложение на копродукт.
LaTeX
$$$HasPullback\; g\; (c.\ι.app i)$ for all i$$
Lean4
theorem hasPullbacks_of_is_coproduct [FinitaryPreExtensive C] {ι : Type*} [Finite ι] {F : Discrete ι ⥤ C} {c : Cocone F}
(hc : IsColimit c) (i : Discrete ι) {X : C} (g : X ⟶ _) : HasPullback g (c.ι.app i) := 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
change Cofan f at c
obtain ⟨i⟩ := i
let e : ∐ f ≅ f i ⨿ (∐ fun j : ({ i }ᶜ : Set ι) ↦ f j) :=
{ hom :=
Sigma.desc
(fun j ↦
if h : j = i then eqToHom (congr_arg f h) ≫ coprod.inl
else Sigma.ι (fun j : ({ i }ᶜ : Set ι) ↦ f j) ⟨j, h⟩ ≫ coprod.inr)
inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun j ↦ Sigma.ι f j)
hom_inv_id := by cat_disch
inv_hom_id := by
ext j
· simp
· simp only [coprod.desc_comp, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app, eqToHom_refl, Category.id_comp,
dite_true, BinaryCofan.mk_pt, BinaryCofan.ι_app_right, BinaryCofan.mk_inr, colimit.ι_desc_assoc,
Discrete.functor_obj, Category.comp_id]
exact dif_neg j.prop }
let e' : c.pt ≅ f i ⨿ (∐ fun j : ({ i }ᶜ : Set ι) ↦ f j) := hc.coconePointUniqueUpToIso (getColimitCocone _).2 ≪≫ e
have : coprod.inl ≫ e'.inv = c.ι.app ⟨i⟩ :=
by
simp only [e, e', Iso.trans_inv, coprod.desc_comp, colimit.ι_desc, BinaryCofan.mk_pt, BinaryCofan.ι_app_left,
BinaryCofan.mk_inl]
exact colimit.comp_coconePointUniqueUpToIso_inv _ _
clear_value e'
rw [← this]
have : IsPullback (𝟙 _) (g ≫ e'.hom) g e'.inv := IsPullback.of_horiz_isIso ⟨by simp⟩
exact ⟨⟨⟨_, ((IsPullback.of_hasPullback (g ≫ e'.hom) coprod.inl).paste_horiz this).isLimit⟩⟩⟩
