hasLimit_of_comp_forget_hasLimit — Mathlib

English

If a diagram D of algebras has a limit after forgetting to the base category, then D has a limit provided the forgetful functor preserves the shape of limits.

Русский

Если диаграмма D алгебр имеет предел после отказа от структуры к базе, то D имеет предел при условии сохранения забывающей функции форм формы предела.

LaTeX

$$$[HasLimit (F \;⋙\; R)] \Rightarrow \text{HasLimit } F \quad\text{for appropriate } F,R.$$$

Lean4

/-- `D ⋙ forget T` has a limit, then `D` has a limit. -/
theorem hasLimit_of_comp_forget_hasLimit (D : J ⥤ Algebra T) [HasLimit (D ⋙ forget T)] : HasLimit D :=
  hasLimit_of_created D (forget T)

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