colimitsOfShape_le — Mathlib

English

Let C be a category and W a morphism property on C. For any shape J, if W is closed under colimits of shape J, then every morphism that appears as a colimit of a shape J diagram whose arrows all have property W also has property W. In particular, W(colimits of shape J) ⊆ W.

Русский

Пусть C — категория, W — свойство морфизмов в C. Для любой формы J, если W сохраняется под колимитами формы J, то каждый морфизм, возникающий как колимит диаграммы формы J, состоящей из стрел, удовлетворяющих свойству W, также имеет свойство W. Тогда W(colimits по форме J) ⊆ W.

LaTeX

$$$W\colimitsOfShape J \le W$$$

Lean4

theorem colimitsOfShape_le [W.IsStableUnderColimitsOfShape J] : W.colimitsOfShape J ≤ W := by
  rwa [← isStableUnderColimitsOfShape_iff_colimitsOfShape_le]

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