instPreservesFiniteColimitsMapActionOfHasFiniteColimits

English

If F preserves finite colimits and V has finite colimits, then F.mapAction G preserves finite colimits.

Русский

Если F сохраняет конечные колимиты и V имеет конечные колимиты, тогда F.mapAction G сохраняет конечные колимиты.

LaTeX

$$$\\operatorname{PreservesFiniteColimits}(F.mapAction\\,G)$$$

Lean4

/-- `F.mapAction : Action V G ⥤ Action W G` preserves finite colimits if
`V` has finite colimits and `F` preserves finite colimits. -/
instance [PreservesFiniteColimits F] [HasFiniteColimits V] : PreservesFiniteColimits (F.mapAction G) where
  preservesFiniteColimits _ _ _ := inferInstance

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