inverse — Mathlib

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