Joint reflection of subobject order

A family of pullback-preserving, mono-preserving functors that jointly reflects isomorphisms also reflects order and equality between subobjects of a fixed object. Local factorisations make the images of the global pullback projection isomorphisms; joint reflection then gives the global factorisation.

The theorem compares existing subobjects. It does not construct a subobject from local data or assert any gluing condition.

theorem CategoryTheory.Subobject.le_iff_mapFunctor_le_of_jointlyReflectsIsomorphisms {I : Type w} {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {D : I → Type u'} [(i : I) → Category.{v', u'} (D i)] (F : (i : I) → Functor C (D i)) [∀ (i : I), Limits.PreservesLimitsOfShape Limits.WalkingCospan (F i)] [∀ (i : I), (F i).PreservesMonomorphisms] (hF : JointlyReflectIsomorphisms F) {X : C} (P Q : Subobject X) : P ≤ Q ↔ ∀ (i : I), mapFunctor (F i) P ≤ mapFunctor (F i) Q

A pullback-preserving family jointly reflecting isomorphisms reflects subobject order. No finite-colimit or finite-cover hypothesis is needed.

theorem CategoryTheory.Subobject.eq_iff_mapFunctor_eq_of_jointlyReflectsIsomorphisms {I : Type w} {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {D : I → Type u'} [(i : I) → Category.{v', u'} (D i)] (F : (i : I) → Functor C (D i)) [∀ (i : I), Limits.PreservesLimitsOfShape Limits.WalkingCospan (F i)] [∀ (i : I), (F i).PreservesMonomorphisms] (hF : JointlyReflectIsomorphisms F) {X : C} (P Q : Subobject X) : P = Q ↔ ∀ (i : I), mapFunctor (F i) P = mapFunctor (F i) Q

Equality of two existing subobjects is detected by the same family.