hasLimit_of_reflective — Mathlib

English

If F has a limit and R is reflective, then F has a limit as well; reflective functors preserve the existence of limits through forgetful constructions.

Русский

Если F имеет предел, а R — отражатель, то F имеет предел, и отражатели сохраняют существование пределов через забывающие конструкций.

LaTeX

$$$[HasLimit (F \;⋙\; R)] \Rightarrow [\text{Reflective } R] \Rightarrow \text{HasLimit } F.$$$

Lean4

theorem hasLimit_of_reflective (F : J ⥤ D) (R : D ⥤ C) [HasLimit (F ⋙ R)] [Reflective R] : HasLimit F :=
  haveI := monadicCreatesLimits.{v, u} R
  hasLimit_of_created F R

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