multicoforkEquivSigmaCofork — Mathlib

Lean4
/-- The category of multicoforks is equivalent to the category of coforks over `∐ I.left ⇉ ∐ I.right`.
It then follows from `CategoryTheory.IsColimit.ofPreservesCoconeInitial` (or `reflects`) that
it preserves and reflects colimit cocones.
-/
@[simps]
noncomputable def multicoforkEquivSigmaCofork : Multicofork I ≌ Cofork I.fstSigmaMap I.sndSigmaMap
    where
  functor := toSigmaCoforkFunctor I
  inverse := ofSigmaCoforkFunctor I
  unitIso := NatIso.ofComponents fun K => Cocones.ext (Iso.refl _) (by rintro (_ | _) <;> simp)
  counitIso :=
    NatIso.ofComponents fun K =>
      Cofork.ext (Iso.refl _)
        (by
          -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): in mathlib3 this was just `ext` and I don't know why it's not here

          apply Limits.colimit.hom_ext
          rintro ⟨j⟩
          simp)
Похожие утверждения