instEssSurjCoalgebraToComonadAdjComparison

English

There is an ess-surjectivity instance for the comonad comparison associated to a comonadic adjunction.

Русский

Сопутствующее свойство эс-сюръективности для сопоставления комонады, связанного с сопряжением комонады.

LaTeX

$$$$\\text{EssSurj}(\\mathrm{Comonad.comparison}(\\text{comonadicAdjunction } L))$$$$

Lean4

instance (G : Comonad C) : (Comonad.comparison G.adj).EssSurj where
  mem_essImage
    X :=
    ⟨{  A := X.A
        a := X.a
        counit := by simpa using X.counit
        coassoc := by simpa using X.coassoc }, ⟨Comonad.Coalgebra.isoMk (Iso.refl _)⟩⟩

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