English
For a functor F: C ⥤ D and an object d ∈ D, there is a contravariant functor from costructured arrows F.op.obj c ⟶ op d to the structured arrows d ⟶ F.obj c.
Русский
Для функторa F: C ⥤ D и объекта d ∈ D существует контрвариантный функтор от коструктурированных стрелок F.op.obj c ⟶ op d к структурированным стрелкам d ⟶ F.obj c.
LaTeX
$$$toStructuredArrow (F : C \to D) (d : D) : (CostructuredArrow F d)^{op} ⥤ StructuredArrow (op d) F^{op}$$$
Lean4
/-- For a functor `F : C ⥤ D` and an object `d : D`, we obtain a contravariant functor from the
category of costructured arrows `F.obj c ⟶ d` to the category of structured arrows
`op d ⟶ F.op.obj c`.
-/
@[simps]
def toStructuredArrow (F : C ⥤ D) (d : D) : (CostructuredArrow F d)ᵒᵖ ⥤ StructuredArrow (op d) F.op
where
obj X := @StructuredArrow.mk _ _ _ _ _ (op X.unop.left) F.op X.unop.hom.op
map f := StructuredArrow.homMk f.unop.left.op (by simp [← op_comp])
