preservesFiniteColimits_of_createsFiniteColimits_and_hasFiniteColimits

English

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

Русский

Если F создаёт конечные колимиты, и D имеет конечные колимиты, тогда F сохраняет конечные колимиты.

LaTeX

$$$PreservesFiniteColimits F$$$

Lean4

instance (priority := 100) preservesFiniteColimits_of_createsFiniteColimits_and_hasFiniteColimits (F : C ⥤ D)
    [CreatesFiniteColimits F] [HasFiniteColimits D] : PreservesFiniteColimits F where
  preservesFiniteColimits _ _ _ := inferInstance

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