hasFiniteColimits_of_hasColimits_of_createsFiniteColimits

English

If D has finite colimits and F creates finite colimits, then C has finite colimits.

Русский

Если в D существуют конечные когомапы и F создаёт конечные колимиты, тогда в C существуют конечные колимиты.

LaTeX

$$$HasFiniteColimits C$ given $HasFiniteColimits D$ and $CreatesFiniteColimits F$$$

Lean4

theorem hasFiniteColimits_of_hasColimits_of_createsFiniteColimits (F : C ⥤ D) [HasFiniteColimits D]
    [CreatesFiniteColimits F] : HasFiniteColimits C where
  out _ _ _ := hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape F

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