locallySmall_of_faithful — Mathlib

English

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

Русский

Если F: C → D верен и D локально мал, то C локально мал.

LaTeX

$$$\operatorname{LocallySmall}(C)$, given $\operatorname{Faithful}(F)$ and $\operatorname{LocallySmall}(D)$$$

Lean4

theorem locallySmall_of_faithful {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D] (F : C ⥤ D) [F.Faithful]
    [LocallySmall.{w} D] : LocallySmall.{w} C where hom_small {_ _} := small_of_injective F.map_injective

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