preservesFiniteColimits_of_preservesFiniteColimitsOfSize

English

If for every finite J there is a preservation of shape J by F, then F preserves all finite colimits.

Русский

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

LaTeX

$$$\forall J\, [\text{FinCategory } J], \; \mathrm{PreservesColimitsOfShape}(J, F) \Rightarrow \mathrm{PreservesFiniteColimits}(F)$$$

Lean4

/-- We can always derive `PreservesFiniteColimits C`
by showing that we are preserving colimits at an arbitrary universe. -/
theorem preservesFiniteColimits_of_preservesFiniteColimitsOfSize (F : C ⥤ D)
    (h : ∀ (J : Type w) {𝒥 : SmallCategory J} (_ : @FinCategory J 𝒥), PreservesColimitsOfShape J F) :
    PreservesFiniteColimits F where
  preservesFiniteColimits J (_ : SmallCategory J)
    _ := by
    letI : Category (ULiftHom (ULift J)) := ULiftHom.category
    haveI := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift
    exact preservesColimitsOfShape_of_equiv (ULiftHomULiftCategory.equiv J).symm F

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