locallySmall_of_hasLocalization — Mathlib

English

If a localization exists for W, then the target category D is locally W-small.

Русский

Если существует локализация для W, то целевая категория D локально по W-морфизмам малая.

LaTeX

$$$\text{LocallySmall}^w(D)$$$

Lean4

/-- If a class of morphisms `W : MorphismProperty C` satisfies `HasLocalization.{w} W`,
then any localized category for `W` (i.e. any target of a localization functor
`L : C ⥤ D` for `W`) is locally `w`-small. -/
theorem locallySmall_of_hasLocalization {D : Type u₂} [Category.{v₂} D] (L : C ⥤ D) [L.IsLocalization W]
    [HasLocalization.{w} W] : LocallySmall.{w} D where
  hom_small _ _ := small_of_injective (fun _ _ h ↦ (Localization.uniq L W.Q' W).functor.map_injective h)

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