English
Inverse map formula for toOverCompCoyoneda in the costructured-arrow setting, analogous to Yoneda case.
Русский
Обратное отображение для toOverCompCoyoneda в контексте CostructuredArrow, аналогично случаю Yoneda.
LaTeX
$$$$ (overEquivPresheafCostructuredArrow A).inverse.map (((CostructuredArrow.toOverCompCoyoneda A).hom.app (op X)).app T f) = (CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).isoCompInverse.inv.app X \\gg f \\gg (overEquivPresheafCostructuredArrow A).unit.app T $$$$
Lean4
@[simp]
theorem overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda {A : Cᵒᵖ ⥤ Type v} {T : Over A}
{X : CostructuredArrow yoneda A} (f : (CostructuredArrow.toOver yoneda A).obj X ⟶ T) :
(overEquivPresheafCostructuredArrow A).inverse.map
(((CostructuredArrow.toOverCompCoyoneda A).hom.app (op X)).app T f) =
(CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).isoCompInverse.inv.app X ≫
f ≫ (overEquivPresheafCostructuredArrow A).unit.app T :=
by simp [CostructuredArrow.toOverCompCoyoneda]
