whiskeringRightPreservesColimits — Mathlib

English

If F preserves colimits of shape J, then whiskeringRight by F preserves colimits of shape J in the functor category.

Русский

Если F сохраняет колимиты формы J, то whiskeringRight по F сохраняет колимиты формы J в категории функционоров.

LaTeX

$$$\\operatorname{PreservesColimitsOfShape} J\\big((\\mathrm{whiskeringRight}\\;C\\;D\\;E).\\mathrm{obj} F\\big)$$$

Lean4

instance whiskeringRightPreservesColimits {C : Type*} [Category C] {D : Type*} [Category D] {E : Type*} [Category E]
    (F : D ⥤ E) [HasColimitsOfSize.{w, w'} D] [PreservesColimitsOfSize.{w, w'} F] :
    PreservesColimitsOfSize.{w, w'} ((whiskeringRight C D E).obj F) :=
  ⟨inferInstance⟩

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