toStructuredArrow — Mathlib

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

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