English
There is a canonical functor from StructuredArrow on the diagonal to Under-forget, given by projecting to components and mapping morphisms accordingly.
Русский
Существует канонический функтор между структурированной стрелкой над диагональю и Under.forget, получаемый проекцией на компоненты и отображением тождественных морфизмов.
LaTeX
$$$\mathrm{functor}\;:\mathrm{StructuredArrow}(X,\mathrm{diag})\to \mathrm{StructuredArrow}(X.2, \mathrm{Under.forget}(X.1))$$$
Lean4
/-- The canonical functor from the costructured arrow category on the diagonal functor
`T ⥤ T × T` to the costructured arrow category on `Under.forget`. -/
@[simps!]
def functor (X : T × T) : CostructuredArrow (Functor.diag _) X ⥤ CostructuredArrow (Over.forget X.1) X.2 :=
Functor.toCostructuredArrow
(Functor.toOver (CostructuredArrow.proj _ X) _ (fun g => by exact g.hom.1)
(fun m => by have := congrArg (·.1) m.w; cat_disch))
_ _ (fun f => f.hom.2) (fun m => by have := congrArg (·.2) m.w; cat_disch)
