locallySmall — Mathlib

English

The category of cochain complexes over a locally small category is locally small when the index category is small.

Русский

Категория коцепентных комплексов над локально малой категорией локально мала, если индексная категория малая.

LaTeX

$$$\text{LocallySmall}(\mathrm{CochainComplex}(C, \mathbb{Z}))$, при условии локальной малости $C$ и малости индекса.$$

Lean4

instance locallySmall [LocallySmall.{w} C] [Small.{w} ι] : LocallySmall.{w} (HomologicalComplex C c) where
  hom_small K
    L := by
    let emb (f : K ⟶ L) (i : Shrink.{w} ι) := (equivShrink.{w} _) (f.f ((equivShrink _).symm i))
    have hemb : Function.Injective emb := fun f g h ↦ by
      ext i
      obtain ⟨i, rfl⟩ := (equivShrink.{w} _).symm.surjective i
      simpa [emb] using congr_fun h i
    apply small_of_injective hemb

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