instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCosplitPair

English

For a coalgebra A of the adjunction-induced comonad, the main pair (G.map A.a, η_GA) is cosplit.

Русский

Для коалгебры A комонад после сопряжения основная пара (G.map A.a, η_GA) кослитна.

LaTeX

$$$\text{main\_pair\_F\_cosplit }(A) : (G.map A.a, adj.unit.app (G.obj A.A)) \text{ is a } F\text{-cosplit pair.}$$$

Lean4

instance [PreservesLimitOfIsCosplitPair F] :
    ∀ (A : Coalgebra adj.toComonad), PreservesLimit (parallelPair (G.map A.a) (NatTrans.app adj.unit (G.obj A.A))) F :=
  fun _ => PreservesLimitOfIsCosplitPair.out _ _

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