English
Let W be a morphism property on C. Then W is small if and only if there exists a small indexing type ι, objects A_i,B_i and arrows f_i : A_i ⟶ B_i such that W = ofHoms f.
Русский
Пусть W — свойство морфизмов на C. Тогда W малое тогда и только тогда, когда существует малый индекс ι, семейство объектов A_i,B_i и стрел f_i : A_i ⟶ B_i такие, что W = ofHoms f.
LaTeX
$$$\operatorname{IsSmall}(W) \iff \exists \iota\,(A,B: \iota \to C)\,(f: \forall i:\iota, A_i \to B_i),\ W = \operatorname{ofHoms} f$$$
Lean4
theorem isSmall_iff_eq_ofHoms : IsSmall.{w} W ↔ ∃ (ι : Type w) (A B : ι → C) (f : ∀ i, A i ⟶ B i), W = ofHoms f :=
by
constructor
· intro
refine ⟨Shrink.{w} W.toSet, _, _, fun i ↦ ((equivShrink _).symm i).1.hom, ?_⟩
ext A B f
rw [ofHoms_iff]
constructor
· intro hf
exact ⟨equivShrink _ ⟨f, hf⟩, by simp⟩
· rintro ⟨i, hi⟩
simp only [← W.arrow_mk_mem_toSet_iff, hi, Arrow.mk_eq, Subtype.coe_prop]
· rintro ⟨_, _, _, _, rfl⟩
infer_instance
