comparison_full

Mathlib.CategoryTheory.Monad.Adjunction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Reflective.comparison_full

English

There is a fullness property for Monad.comparison in the reflective setting.

Русский

Свойство полноты для сопоставления монад в отражательном контексте.

LaTeX

$$$$\\text{Monad.comparison}(\\text{reflectorAdjunction } R)\\text{ isFull}$$$$

Lean4

theorem comparison_full [R.Full] {L : C ⥤ D} (adj : L ⊣ R) : (Monad.comparison adj).Full where
  map_surjective f := ⟨R.preimage f.f, by cat_disch⟩

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

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

Разделы

Аффилиация

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