instHasCoequalizerMapAAppCounitObjAOfHasCoequalizerOfIsSplitPair

English

If f,g form an IsSplitPair and G preserves the split, then G preserves the colimit of the parallel pair.

Русский

Если f,g образуют IsSplitPair и G сохраняет этот разрез, тогда G сохраняет колимит параллельной пары.

LaTeX

$$$\\forall f,g,\\; G \\text{ preserves } \\operatorname{colimit}(\\operatorname{parallelPair}(f,g))$ under the IsSplitPair hypotheses.$$

Lean4

instance [HasCoequalizerOfIsSplitPair G] :
    ∀ (A : Algebra adj.toMonad), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A)) := fun _ =>
  HasCoequalizerOfIsSplitPair.out G _
    _
      -- Porting note: added these to replace parametric instances https://github.com/leanprover/lean4/issues/2311
      -- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsSplitPair f g], PreservesColimit (parallelPair f g) G]

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