counitBackward — Mathlib

English

Intermediate stage giving an isomorphism between F.obj (op s) and OverArrows (yonedaCollectionPresheafToA F) s.hom.

Русский

Промежуточная стадия, дающая изоморфизм между F.obj (op s) и OverArrows (yonedaCollectionPresheafToA F) s.hom.

LaTeX

$$$$ F.obj (op\,s) \cong OverArrows\ (yonedaCollectionPresheafToA\ F)\ s.hom $$$$

Lean4

/-- Backward direction of the counit. -/
def counitBackward (F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) (s : CostructuredArrow yoneda A) :
    OverArrows (yonedaCollectionPresheafToA F) s.hom → F.obj (op s) := fun p =>
  F.map (eqToHom (by simp [← CostructuredArrow.eq_mk])) p.val.snd

Похожие утверждения