English
Let F: C → D be a functor and d an object of D. Then there exists a contravariant functor from the category of structured arrows op d ⟶ F.op.obj c to the category of costructured arrows F.obj c ⟶ d.
Русский
Пусть F: C ⥤ D — функтор и d — объект D. Существуют контрвариантные перестановки от категории структурированных стрелок op d ⟶ F.op.obj c к категории коструктурированных стрелок F.obj c ⟶ d.
LaTeX
$$$toCostructuredArrow'(F,d) : (StructuredArrow (\mathrm{op} \, d) F^{op})^{op} \longrightarrow \mathrm{CostructuredArrow} F d$$$
Lean4
/-- For a functor `F : C ⥤ D` and an object `d : D`, we obtain a contravariant functor from the
category of structured arrows `op d ⟶ F.op.obj c` to the category of costructured arrows
`F.obj c ⟶ d`.
-/
@[simps]
def toCostructuredArrow' (F : C ⥤ D) (d : D) : (StructuredArrow (op d) F.op)ᵒᵖ ⥤ CostructuredArrow F d
where
obj X := @CostructuredArrow.mk _ _ _ _ _ (unop X.unop.right) F X.unop.hom.unop
map
f :=
CostructuredArrow.homMk f.unop.right.unop
(by
dsimp
rw [← Quiver.Hom.unop_op (F.map (Quiver.Hom.unop f.unop.right)), ← unop_comp, ← F.op_map, ← f.unop.w]
simp)
