isColimitMapCoconeCoforkEquiv — Mathlib

English

Same as above, asserting that equalizer comparison is an iso under preservation assumptions.

Русский

То же самое: равнопроизводитель равенств по сохранению — изоморфизм.

LaTeX

$$$\\text{IsIso}(\\text{equalizerComparison } f g G)$$$

Lean4

/-- The map of a cofork is a colimit iff the cofork consisting of the mapped morphisms is a colimit.
This essentially lets us commute `Cofork.ofπ` with `Functor.mapCocone`.
-/
def isColimitMapCoconeCoforkEquiv :
    IsColimit (G.mapCocone (Cofork.ofπ h w)) ≃
      IsColimit (Cofork.ofπ (G.map h) (by simp only [← G.map_comp, w]) : Cofork (G.map f) (G.map g)) :=
  (IsColimit.precomposeInvEquiv (diagramIsoParallelPair _) _).symm.trans <|
    IsColimit.equivIsoColimit <|
      Cofork.ext (Iso.refl _) <| by
        dsimp only [Cofork.π, Cofork.ofπ_ι_app]
        dsimp; rw [Category.comp_id, Category.id_comp]

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