English
Another instance of CounitAuxAux expressing the isomorphism at op s for the presheaf-to-Over construction.
Русский
Еще один пример CounitAuxAux, выражающий изоморфизм на op s для преобразования presheaf в Over.
LaTeX
$$$$ F.obj (op s) \cong OverArrows (\yonedaCollectionPresheafToA F) \ s.hom $$$$
Lean4
@[simp]
theorem overEquivPresheafCostructuredArrow_functor_map_toOverCompYoneda {A : Cᵒᵖ ⥤ Type v} {T : Over A}
{X : CostructuredArrow yoneda A} (f : yoneda.obj X ⟶ (overEquivPresheafCostructuredArrow A).functor.obj T) :
(overEquivPresheafCostructuredArrow A).functor.map (((CostructuredArrow.toOverCompYoneda A T).inv.app (op X) f)) =
(CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).hom.app X ≫ f :=
by simp [CostructuredArrow.toOverCompYoneda]
