ofFork — Mathlib

Lean4
/-- This is a helper construction that can be useful when verifying that a category has all
equalizers. Given `F : WalkingParallelPair ⥤ C`, which is really the same as
`parallelPair (F.map left) (F.map right)`, and a fork on `F.map left` and `F.map right`,
we get a cone on `F`.

If you're thinking about using this, have a look at `hasEqualizers_of_hasLimit_parallelPair`,
which you may find to be an easier way of achieving your goal. -/
def ofFork {F : WalkingParallelPair ⥤ C} (t : Fork (F.map left) (F.map right)) : Cone F
    where
  pt := t.pt
  π :=
    { app := fun X => t.π.app X ≫ eqToHom (by simp)
      naturality := by rintro _ _ (_ | _ | _) <;> simp [t.condition] }
Похожие утверждения