preservesColimits_const — Mathlib

English

The constant functor Const_D: C ⥤ (D ⥤ C) preserves all colimits (i.e., colimits of all shapes) whenever C has those colimits.

Русский

Постоянный функтор Const_D: C ⥤ (D ⥤ C) сохраняет все колимиты, если у C существуют такие колимиты.

LaTeX

$$$\\text{Const}_D: C \\to \\mathsf{Fun}(D, C) \\text{ preserves all colimits}. $$$

Lean4

/-- The constant functor `C ⥤ (D ⥤ C)` preserves colimits. -/
instance preservesColimits_const : PreservesColimitsOfSize.{w', w} (const D : C ⥤ _) :=
  preservesColimits_of_evaluation _ fun _ => preservesColimits_of_natIso <| Iso.symm <| constCompEvaluationObj _ _

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