coconeEquivalenceOpConeOp — Mathlib

Lean4
/-- The category of cocones on `F`
is equivalent to the opposite category of
the category of cones on the opposite of `F`.
-/
def coconeEquivalenceOpConeOp : Cocone F ≌ (Cone F.op)ᵒᵖ
    where
  functor :=
    { obj := fun c => op (Cocone.op c)
      map := fun {X} {Y} f =>
        Quiver.Hom.op
          { hom := f.hom.op
            w := fun j => by
              apply Quiver.Hom.unop_inj
              dsimp
              apply CoconeMorphism.w } }
  inverse :=
    { obj := fun c => Cone.unop (unop c)
      map := fun {X} {Y} f =>
        { hom := f.unop.hom.unop
          w := fun j => by
            apply Quiver.Hom.op_inj
            dsimp
            apply ConeMorphism.w } }
  unitIso := NatIso.ofComponents (fun c => Cocones.ext (Iso.refl _))
  counitIso :=
    NatIso.ofComponents (fun c => (Cones.ext (Iso.refl c.unop.pt)).op) fun {X} {Y} f =>
      Quiver.Hom.unop_inj (ConeMorphism.ext _ _ (by simp))
  functor_unitIso_comp
    c := by
    apply Quiver.Hom.unop_inj
    apply ConeMorphism.ext
    dsimp
    apply comp_id
Похожие утверждения