reflectsFiniteColimits — Mathlib

English

If F reflects isomorphisms and has finite colimits and preserves finite colimits, then F reflects finite colimits.

Русский

Если F отражает изomорфизмы, имеет конечные колимиты и сохраняет их, то F отражает конечные колимиты.

LaTeX

$$$\mathrm{ReflectsIsomorphisms}(F) \land \mathrm{HasFiniteColimits}(C) \land \mathrm{PreservesFiniteColimits}(F) \Rightarrow \mathrm{ReflectsFiniteColimits}(F)$$$

Lean4

/-- If we reflect colimits of some arbitrary size, then we reflect all finite colimits. -/
theorem reflectsFiniteColimits (F : C ⥤ D) [ReflectsColimitsOfSize.{w, w₂} F] : ReflectsFiniteColimits F where
  reflects J (sJ : SmallCategory J)
    fJ := by
    haveI := reflectsSmallestColimits_of_reflectsColimits F
    exact reflectsColimitsOfShape_of_equiv (FinCategory.equivAsType J) F

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