isColimitEquiv — Mathlib

English

There is an equivalence between IsColimit of G.toCofork and IsColimit of G.

Русский

Существует эквивалентность между IsColimit у G.toCofork и IsColimit у G.

LaTeX

$$$\mathrm{IsColimit}(G.\text{toCofork}) \simeq \mathrm{IsColimit}(G)$$$

Lean4

/-- A reflexive cofork is a colimit cocone if and only if the underlying cofork is. -/
def isColimitEquiv (G : ReflexiveCofork F) : IsColimit (G.toCofork) ≃ IsColimit G :=
  IsColimit.equivIsoColimit (reflexiveCoforkEquivCoforkObjIso F G).symm |>.trans <|
    (IsColimit.precomposeHomEquiv (diagramIsoParallelPair _).symm (G.whisker _)).trans <|
      Functor.Final.isColimitWhiskerEquiv _ _

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