English
Let 𝒢 be a detecting set in C. For any object X and subobjects P,Q ⊆ X, if P ≤ Q and for every G ∈ 𝒢 and every f: G → X we have Q.Factors f implies P.Factors f, then P = Q.
Русский
Пусть 𝒢 — обнаруживающий набор объектов в C. Пусть X — объект, P,Q ⊆ X — подобъекты. Если P ≤ Q и для каждого G ∈ 𝒢 и каждого f:G → X выполняется Q.Factors f ⇒ P.Factors f, то P = Q.
LaTeX
$$$$\forall X\,\forall P,Q \text{ Sub}(X),\ P \le Q \Rightarrow \\ \bigl(\forall G \in 𝒢, \forall f:G\to X,\ Q.Factors f \Rightarrow P.Factors f\bigr) \Rightarrow P = Q.$$$$
Lean4
theorem eq_of_le_of_isDetecting {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) {X : C} (P Q : Subobject X) (h₁ : P ≤ Q)
(h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f) : P = Q :=
by
suffices IsIso (ofLE _ _ h₁) by exact le_antisymm h₁ (le_of_comm (inv (ofLE _ _ h₁)) (by simp))
refine h𝒢 _ fun G hG f => ?_
have : P.Factors (f ≫ Q.arrow) := h₂ _ hG ((factors_iff _ _).2 ⟨_, rfl⟩)
refine ⟨factorThru _ _ this, ?_, fun g (hg : g ≫ _ = f) => ?_⟩
· simp only [← cancel_mono Q.arrow, Category.assoc, ofLE_arrow, factorThru_arrow]
·
simp only [← cancel_mono (Subobject.ofLE _ _ h₁), ← cancel_mono Q.arrow, hg, Category.assoc, ofLE_arrow,
factorThru_arrow]
