locallySmall_congr — Mathlib

English

LocallySmall is invariant under equivalence of categories.

Русский

Локально-малость инвариантна по отношению к эквивалентности категорий.

LaTeX

$$$\operatorname{LocallySmall}(C) \iff \operatorname{LocallySmall}(D)$ under an equivalence$$

Lean4

theorem locallySmall_congr {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D] (e : C ≌ D) :
    LocallySmall.{w} C ↔ LocallySmall.{w} D :=
  ⟨fun _ => locallySmall_of_faithful e.inverse, fun _ => locallySmall_of_faithful e.functor⟩

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