essentiallySmall_of_fully_faithful

English

If F: C → D is fully faithful and D is essentially small, then C is essentially small.

Русский

Если F: C → D полно и отображает инъективно, и D является существенно малой, то C является существенно малой.

LaTeX

$$$\text{Full}(F) \wedge \text{Faithful}(F) \wedge \text{EssentiallySmall}(D) \Rightarrow \text{EssentiallySmall}(C)$$$

Lean4

theorem essentiallySmall_of_fully_faithful {D : Type u'} [Category.{v'} D] (F : C ⥤ D) [F.Full] [F.Faithful]
    [EssentiallySmall.{w} D] : EssentiallySmall.{w} C :=
  (essentiallySmall_iff C).2 ⟨small_of_injective F.mapSkeleton_injective, locallySmall_of_faithful F⟩

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