hasLimit_iff_small_sections — Mathlib

English

The existence of a limit for F is equivalent to the smallness of the sections of F composed with forgetful functors.

Русский

Существование предела для F эквивалентно малости секций F в цепочке забываний.

LaTeX

$$$\\text{HasLimit } F \\iff \\text{Small}(F \\to \\mathrm{forget GrpCat})$$$

Lean4

/-- A functor `F : J ⥤ GrpCat.{u}` has a limit iff `(F ⋙ forget GrpCat).sections` is
`u`-small. -/
@[to_additive /-- A functor `F : J ⥤ AddGrpCat.{u}` has a limit iff
    `(F ⋙ forget AddGrpCat).sections` is `u`-small. -/
    ]
theorem hasLimit_iff_small_sections : HasLimit F ↔ Small.{u} (F ⋙ forget GrpCat).sections :=
  by
  constructor
  · apply Concrete.small_sections_of_hasLimit
  · intro
    infer_instance

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