reflectsFiniteLimits — Mathlib

English

The reflection of limits from any size implies reflection for all finite limits.

Русский

Отражение пределов для произвольного размера влечёт отражение всех конечных пределов.

LaTeX

$$ReflectsLimitsOfSize(F) ⇒ ReflectsFiniteLimits F$$

Lean4

/-- If we reflect limits of some arbitrary size, then we reflect all finite limits. -/
theorem reflectsFiniteLimits (F : C ⥤ D) [ReflectsLimitsOfSize.{w, w₂} F] : ReflectsFiniteLimits F where
  reflects J (sJ : SmallCategory J)
    fJ := by
    haveI := reflectsSmallestLimits_of_reflectsLimits F
    exact reflectsLimitsOfShape_of_equiv (FinCategory.equivAsType J) F

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