comp_comparison_hasLimit — Mathlib

English

If F ⋙ R has a limit for a monadic right adjoint R, then F ⋙ Monad.comparison (monadicAdjunction R) also has a limit.

Русский

Если F ⋙ R имеет предел, то F ⋙ Monad.comparison (monadicAdjunction R) также имеет предел.

LaTeX

$$$\text{HasLimit} (F \;⋙\; \mathrm{comparison} (\mathrm{monadicAdjunction} R)) \Rightarrow \text{HasLimit} (F ⋙ R).$$$

Lean4

instance comp_comparison_hasLimit (F : J ⥤ D) (R : D ⥤ C) [MonadicRightAdjoint R] [HasLimit (F ⋙ R)] :
    HasLimit (F ⋙ Monad.comparison (monadicAdjunction R)) :=
  Monad.hasLimit_of_comp_forget_hasLimit (F ⋙ Monad.comparison (monadicAdjunction R))

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