hasPullbackInr' — Mathlib

English

For F: C ⥤ D with HasBinaryCoproducts and HasPullbacksOfInclusions, the HasPullback along coprod.inl exists.

Русский

Для F: C → D с HasBinaryCoproducts и HasPullbacksOfInclusions существует вытянутый предел вдоль coprod.inl.

LaTeX

$$$\text{HasPullback } f\,\text{ coprod.inl}$$$

Lean4

instance hasPullbackInr' : HasPullback f coprod.inr :=
  by
  have : IsPullback (𝟙 _) (f ≫ (coprod.braiding X Y).hom) f (coprod.braiding Y X).hom :=
    IsPullback.of_horiz_isIso ⟨by simp⟩
  have := (IsPullback.of_hasPullback (f ≫ (coprod.braiding X Y).hom) coprod.inl).paste_horiz this
  simp only [coprod.braiding_hom, Category.comp_id, colimit.ι_desc, BinaryCofan.mk_pt, BinaryCofan.ι_app_left,
    BinaryCofan.mk_inl] at this
  exact ⟨⟨⟨_, this.isLimit⟩⟩⟩

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