comparison_essSurj — Mathlib

English

There is an equivalence between Coalgebra and the comonad structure induced by a comonadic adjunction.

Русский

Существует эквивалентность между структурой Coalgebra и комонады, индуцируемой комонадным сопряжением.

LaTeX

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

Lean4

instance comparison_essSurj [Coreflective R] : (Comonad.comparison (coreflectorAdjunction R)).EssSurj :=
  by
  refine ⟨fun X => ⟨(coreflector R).obj X.A, ⟨?_⟩⟩⟩
  refine Comonad.Coalgebra.isoMk ?_ ?_
  · exact (asIso ((coreflectorAdjunction R).counit.app X.A))
  rw [← cancel_mono ((coreflectorAdjunction R).counit.app X.A)]
  simp only [Functor.comp_obj, Functor.id_obj, assoc]
  simpa using (coreflectorAdjunction R).counit.app X.A ≫= X.counit.symm

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