δ_iso_of_coreflective

Mathlib.CategoryTheory.Monad.Adjunction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.δ_iso_of_coreflective

English

If R is coreflective, then the δ morphism for the comonad is an isomorphism.

Русский

Если R является корефлексивной, то морфизм δ в комонаде является изоморфизмом.

LaTeX

$$$$\\delta \\text{ isIso for coreflector adjunction}$$$$

Lean4

instance δ_iso_of_coreflective [Coreflective R] : IsIso (coreflectorAdjunction R).toComonad.δ :=
  by
  dsimp
  infer_instance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru