functor — Mathlib

Lean4
/-- Auxiliary definition for `structuredArrowRightwardsOpEquivalence`. -/
@[simps!]
def functor : (w.op.StructuredArrowRightwards g)ᵒᵖ ⥤ w.CostructuredArrowDownwards g.unop
    where
  obj
    f :=
    CostructuredArrowDownwards.mk _ _ f.unop.right.left.unop f.unop.right.hom.unop f.unop.hom.left.unop
      (Quiver.Hom.op_inj (by simpa using CostructuredArrow.w f.unop.hom))
  map {f f'}
    φ :=
    CostructuredArrow.homMk
      (StructuredArrow.homMk (φ.unop.right.left.unop) (Quiver.Hom.op_inj (CostructuredArrow.w φ.unop.right)))
      (by
        ext
        exact Quiver.Hom.op_inj ((CostructuredArrow.proj _ _).congr_map (StructuredArrow.w φ.unop)))
Похожие утверждения