hasLimit_iff_small_sections — Mathlib

English

A functor F : J ⥤ CommGrpCat has a limit iff the sections of F ⋙ forget CommGrpCat are small.

Русский

У F : J ⥤ CommGrpCat предел существует тогда и только тогда, когда секции F ⋙ forget CommGrpCat являются малым множеством.

LaTeX

$$$ \mathrm{HasLimit}(F) \;\iff\; \text{Small}((F \cdot \text{forget CommGrpCat}).\text{sections}).$$$

Lean4

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

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