English
Let 𝒢 be a detecting set in C with HasPullbacks. If P,Q are subobjects of X and for every G ∈ 𝒢 and every f: G → X we have P.Factors f ↔ Q.Factors f, then P = Q.
Русский
Пусть 𝒢 — обнаруживающий набор в C, и чтобы HasPullbacks. Пусть P,Q — подобъекты X; если для каждого G ∈ 𝒢 и каждого f:G → X верно P.Factors f ↔ Q.Factors f, тогда P = Q.
LaTeX
$$$$\forall X\, \forall P,Q:\mathrm{Sub}(X),\ HasPullbacks(C) \Rightarrow (\forall G\in 𝒢,\forall f:G\to X,\ P.Factors f \iff Q.Factors f) \Rightarrow P = Q.$$$$
Lean4
theorem eq_of_isDetecting [HasPullbacks C] {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) {X : C} (P Q : Subobject X)
(h : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f) : P = Q :=
calc
P = P ⊓ Q := Eq.symm <| inf_eq_of_isDetecting h𝒢 _ _ fun G hG _ hf => (h G hG).1 hf
_ = Q ⊓ P := inf_comm ..
_ = Q := inf_eq_of_isDetecting h𝒢 _ _ fun G hG _ hf => (h G hG).2 hf
