English
Let Ω be a type and C a category whose objects and morphisms have cardinalities bounded by Ω. Then there exists a small category h (over Ω) such that the category of Ω-sized representations of h is equivalent to C.
Русский
Пусть Ω — тип, а C — категория, чьи объекты и множества морфизмов имеют кардинальности, ограниченные Ω. Тогда существует малая категория h (над Ω), такая что категория семей Ω h эквивалентна C.
LaTeX
$$$\\exists h\\, (\\text{categoryFamily}(\\Omega,h) \\simeq C)$$$
Lean4
theorem exists_equivalence (C : Type u) [Category.{v} C]
(h₁ : Cardinal.lift.{w} (Cardinal.mk C) ≤ Cardinal.lift.{u} (Cardinal.mk Ω))
(h₂ : ∀ (X Y : C), Cardinal.lift.{w} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v} (Cardinal.mk Ω)) :
∃ (h : SmallCategoryOfSet Ω), Nonempty (categoryFamily Ω h ≌ C) :=
by
let f₁ := (Cardinal.lift_mk_le'.1 h₁).some
let f₂ (X Y) := (Cardinal.lift_mk_le'.1 (h₂ X Y)).some
let e := Equiv.ofInjective _ f₁.injective
let h : CoreSmallCategoryOfSet Ω C :=
{ obj := Set.range f₁
hom X Y := Set.range (f₂ (e.symm X) (e.symm Y))
objEquiv := e.symm
homEquiv {_ _} := by simpa using (Equiv.ofInjective _ ((f₂ _ _).injective)).symm }
exact ⟨h.smallCategoryOfSet, ⟨h.equivalence⟩⟩
