hasLimitsOfShape_of_initial — Mathlib

English

If F: C ⥤ D is initial and E has limits of shape C, then D has limits of shape D. More precisely, for any G: D ⥤ E, the limit of G is obtained by composing with F: lim_G = lim_{G ∘ F}.

Русский

Если F: C → D начальный и в E существуют пределы формы C, то в D существуют пределы формы D; предел диаграммы G: D ⥤ E задаётся как предел диаграммы G ∘ F.

LaTeX

$$$F \text{ initial} \\Rightarrow [\\text{HasLimitsOfShape } C E] \\Rightarrow [\\text{HasLimitsOfShape } D E],\\quad \\text{with } \\operatorname{Lim}(G) = \\operatorname{Lim}(G \\circ F).$$$

Lean4

theorem hasLimitsOfShape_of_initial [HasLimitsOfShape C E] : HasLimitsOfShape D E where
  has_limit := fun _ => hasLimit_of_comp F

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