English
If a category has pullbacks and 𝒢 is a detecting set, then for subobjects P,Q ⊆ X we have P ⊓ Q = P provided that for all G ∈ 𝒢 and all f:G → X, P.Factors f → Q.Factors f.
Русский
Если в категории существуют pullbacks и 𝒢 является обнаруживающим набором, то для подобъектов P,Q ⊆ X выполняется P ∩ Q = P при условии, что для всех G ∈ 𝒢 и всех f:G → X, P.Factors f → Q.Factors f.
LaTeX
$$$$\text{HasPullbacks}(C) \Rightarrow \forall X\, \forall P,Q:\mathrm{Sub}(X),\ (\forall G\in 𝒢,\forall f:G\to X,\ P.Factors f \Rightarrow Q.Factors f) \Rightarrow P \sqcap Q = P.$$$$
Lean4
theorem inf_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 = P :=
eq_of_le_of_isDetecting h𝒢 _ _ _root_.inf_le_left fun _ hG _ hf => (inf_factors _).2 ⟨hf, h _ hG hf⟩
