instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair

English

Let C and D be categories and G : D ⥤ C a functor that preserves colimits of split pairs. Let F ⊣ G be an adjunction with adj : F ⊣ G. For every algebra A over the monad adj.toMonad, the functor G preserves the colimit of the parallel pair defined by F.map A.a and adj.counit.app (F.obj A.A).

Русский

Пусть C и D — категории, G : D ⥤ C сохраняет колимиты по распавшимся парам. Пусть F ⊣ G — смыкающееся сопряжение. Для каждого алгебрического объекта A над монадой adj.toMonad карета G сохраняет колимит пары (F.map A.a, adj.counit.app (F.obj A.A)).

LaTeX

$$$\\forall A:\\mathrm{Algebra}(adj.toMonad),\\; \\operatorname{PreservesColimit}\\left(\\operatorname{parallelPair}\\left(F.map A.a,\\; \\mathrm{NatTrans.app}\\ adj.counit\\ (F.obj A.A)\\right)\\right)\\ G$$$

Lean4

instance [PreservesColimitOfIsSplitPair G] :
    ∀ (A : Algebra adj.toMonad), PreservesColimit (parallelPair (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))) G :=
  fun _ =>
  PreservesColimitOfIsSplitPair.out _
    _
      -- 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], ReflectsColimit (parallelPair f g) G] :

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