locallySmall_of_small_arrow — Mathlib

English

If Arrow C is small, then C is locally small.

Русский

Если Arrow C малая, то C локально малая.

LaTeX

$$$\\\\operatorname{Small}(\\\\operatorname{Arrow}(C)) \\\\Rightarrow \\\\operatorname{LocallySmall}(C)$$$

Lean4

theorem locallySmall_of_small_arrow (C : Type u) [Category.{v} C] [Small.{w} (Arrow C)] : LocallySmall.{w} C where
  hom_small X
    Y :=
    small_of_injective (f := fun f ↦ Arrow.mk f)
      (fun f g h ↦ by
        change (Arrow.mk f).hom = (Arrow.mk g).hom
        congr)

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