instSmallSubtypeForallCarrierObjMemSubmoduleSectionsSubmodule

English

For every diagram F: J → Module_R, the subobject consisting of sections that lie in the submodule is itself a small type, i.e. its underlying carrier is a small set.

Русский

Для каждого диаграммы F: J → модулей_R подпредставление секций, принадлежащих подпмодулю, образует малый тип; его несущая часть является малой по размеру.

LaTeX

$$$\operatorname{Small}\left( \operatorname{Subtype}\big( x \mapsto \big( x \in \mathrm{ModuleCat.sectionsSubmodule}(F) \big) \right) \right)$$$

Lean4

instance : Small.{w} (sectionsSubmodule F) :=
  inferInstanceAs <|
    Small.{w}
      (Functor.sections (F ⋙ forget (ModuleCat R)))
        -- Adding the following instance speeds up `limitModule` noticeably,
        -- by preventing a bad unfold of `limitAddCommGroup`.

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