English
If a category has pullbacks and a small detecting set 𝒢, then it is well-powered; that is, for every object X, the collection of subobjects of X is a set.
Русский
Если категория имеет pullbacks и существует малый обнаруживающий набор 𝒢, то она хорошо мощности: для каждого объекта X множество подобъектов X является множеством.
LaTeX
$$$$\text{HasPullbacks}(C) \land \text{IsDetecting}(\mathcal{G}) \Rightarrow \text{WellPowered}(C).$$$$
Lean4
/-- A category with pullbacks and a small detecting set is well-powered. -/
theorem wellPowered_of_isDetecting [HasPullbacks C] {𝒢 : Set C} [Small.{w} 𝒢] [LocallySmall.{w} C]
(h𝒢 : IsDetecting 𝒢) : WellPowered.{w} C :=
⟨fun X =>
@small_of_injective _ _ _ (fun P : Subobject X => {f : Σ G : 𝒢, G.1 ⟶ X | P.Factors f.2}) fun P Q h =>
Subobject.eq_of_isDetecting h𝒢 _ _ (by simpa [Set.ext_iff, Sigma.forall] using h)⟩
