ofCotrident — Mathlib

Lean4
/-- This is a helper construction that can be useful when verifying that a category has all
    coequalizers. Given `F : WalkingParallelFamily ⥤ C`, which is really the same as
    `parallelFamily (fun j ↦ F.map (line j))`, and a cotrident on `fun j ↦ F.map (line j)` we get a
    cocone on `F`.

    If you're thinking about using this, have a look at
    `hasWideCoequalizers_of_hasColimit_parallelFamily`, which you may find to be an easier way
    of achieving your goal. -/
def ofCotrident {F : WalkingParallelFamily J ⥤ C} (t : Cotrident fun j => F.map (line j)) : Cocone F
    where
  pt := t.pt
  ι :=
    { app := fun X => eqToHom (by cases X <;> cat_disch) ≫ t.ι.app X
      naturality := fun j j' g => by cases g <;> simp [Cotrident.app_one t] }
Похожие утверждения