toCostructuredArrow — Mathlib

Lean4
/-- Given `F : C ⥤ D` and `X : D`, to upgrade a functor `G : E ⥤ C` to a functor
`E ⥤ CostructuredArrow F X`, it suffices to provide maps `F.obj (G.obj Y) ⟶ X` for all `Y`
making the obvious triangles involving all `F.map (G.map g)` commute.

This is of course the same as providing a cocone over `F ⋙ G` with cocone point `X`, see
`Functor.toCostructuredArrowIsoToCostructuredArrow`. -/
@[simps]
def toCostructuredArrow (G : E ⥤ C) (F : C ⥤ D) (X : D) (f : (Y : E) → F.obj (G.obj Y) ⟶ X)
    (h : ∀ {Y Z : E} (g : Y ⟶ Z), F.map (G.map g) ≫ f Z = f Y) : E ⥤ CostructuredArrow F X
    where
  obj Y := CostructuredArrow.mk (f Y)
  map g := CostructuredArrow.homMk (G.map g) (h g)
Похожие утверждения