instSmallFunctorOfLocallySmall — Mathlib

English

If C is small and locally small, and D is small and locally small, then Functor(C,D) is small.

Русский

Если C малая и локально малая, и D малая и локально малая, то категорию функторов Functor(C,D) малая.

LaTeX

$$$\text{Small}(\text{Functor}(C,D))$$$

Lean4

instance [Small.{w} C] [LocallySmall.{w} C] {D : Type u'} [Category.{v'} D] [Small.{w} D] [LocallySmall.{w} D] :
    Small.{w} (C ⥤ D) :=
  by
  refine
    small_of_injective (f := fun F (f : Arrow C) ↦ Arrow.mk (F.map f.hom))
      (fun F G h ↦ Functor.ext (fun X ↦ ?_) (fun X Y f ↦ ?_))
  · exact congr_arg Comma.left (congr_fun h (Arrow.mk (𝟙 X)))
  · have : Arrow.mk (F.map f) = Arrow.mk (G.map f) := congr_fun h (Arrow.mk f)
    rw [Arrow.mk_eq_mk_iff] at this
    tauto

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