Separating and detecting sets #
There are several non-equivalent notions of a generator of a category. Here, we consider two of them:
- We say that
π’is a separating set if the functorsC(G, -)forG β π’are collectively faithful, i.e., ifh β« f = h β« gfor allhwith domain inπ’impliesf = g. - We say that
π’is a detecting set if the functorsC(G, -)collectively reflect isomorphisms, i.e., if anyhwith domain inπ’uniquely factors throughf, thenfis an isomorphism.
There are, of course, also the dual notions of coseparating and codetecting sets.
Main results #
We
- define predicates
is_separating,is_coseparating,is_detectingandis_codetectingon sets of objects; - show that separating and coseparating are dual notions;
- show that detecting and codetecting are dual notions;
- show that if
Chas equalizers, then detecting implies separating; - show that if
Chas coequalizers, then codetecting implies separating; - show that if
Cis balanced, then separating implies detecting and coseparating implies codetecting; - show that
βis separating if and only ifβis coseparating if and only ifCis thin; - show that
βis detecting if and only ifβis codetecting if and only ifCis a groupoid; - define predicates
is_separator,is_coseparator,is_detectorandis_codetectoras the singleton counterparts to the definitions for sets above and restate the above results in this situation; - show that
Gis a separator if and only ifcoyoneda.obj (op G)is faithful (and the dual); - show that
Gis a detector if and only ifcoyoneda.obj (op G)reflects isomorphisms (and the dual).
Future work #
- We currently don't have any examples yet.
- We will want typeclasses
has_separator Cand similar.
def
category_theory.is_separating
{C : Type uβ}
[category_theory.category C]
(π’ : set C) :
Prop
We say that π’ is a separating set if the functors C(G, -) for G β π’ are collectively
faithful, i.e., if h β« f = h β« g for all h with domain in π’ implies f = g.
def
category_theory.is_coseparating
{C : Type uβ}
[category_theory.category C]
(π’ : set C) :
Prop
We say that π’ is a coseparating set if the functors C(-, G) for G β π’ are collectively
faithful, i.e., if f β« h = g β« h for all h with codomain in π’ implies f = g.
We say that π’ is a detecting set if the functors C(G, -) collectively reflect isomorphisms,
i.e., if any h with domain in π’ uniquely factors through f, then f is an isomorphism.
Equations
- category_theory.is_detecting π’ = β β¦X Y : Cβ¦ (f : X βΆ Y), (β (G : C), G β π’ β β (h : G βΆ Y), β! (h' : G βΆ X), h' β« f = h) β category_theory.is_iso f
def
category_theory.is_codetecting
{C : Type uβ}
[category_theory.category C]
(π’ : set C) :
Prop
We say that π’ is a codetecting set if the functors C(-, G) collectively reflect
isomorphisms, i.e., if any h with codomain in G uniquely factors through f, then f is
an isomorphism.
Equations
- category_theory.is_codetecting π’ = β β¦X Y : Cβ¦ (f : X βΆ Y), (β (G : C), G β π’ β β (h : X βΆ G), β! (h' : Y βΆ G), f β« h' = h) β category_theory.is_iso f
theorem
category_theory.is_separating_op_iff
{C : Type uβ}
[category_theory.category C]
(π’ : set C) :
theorem
category_theory.is_coseparating_op_iff
{C : Type uβ}
[category_theory.category C]
(π’ : set C) :
theorem
category_theory.is_coseparating_unop_iff
{C : Type uβ}
[category_theory.category C]
(π’ : set Cα΅α΅) :
theorem
category_theory.is_separating_unop_iff
{C : Type uβ}
[category_theory.category C]
(π’ : set Cα΅α΅) :
theorem
category_theory.is_detecting_op_iff
{C : Type uβ}
[category_theory.category C]
(π’ : set C) :
theorem
category_theory.is_codetecting_op_iff
{C : Type uβ}
[category_theory.category C]
(π’ : set C) :
theorem
category_theory.is_detecting_unop_iff
{C : Type uβ}
[category_theory.category C]
(π’ : set Cα΅α΅) :
theorem
category_theory.is_codetecting_unop_iff
{C : Type uβ}
[category_theory.category C]
{π’ : set Cα΅α΅} :
theorem
category_theory.is_detecting.is_separating
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_equalizers C]
{π’ : set C}
(hπ’ : category_theory.is_detecting π’) :
theorem
category_theory.is_codetecting.is_coseparating
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_coequalizers C]
{π’ : set C} :
theorem
category_theory.is_separating.is_detecting
{C : Type uβ}
[category_theory.category C]
[category_theory.balanced C]
{π’ : set C}
(hπ’ : category_theory.is_separating π’) :
theorem
category_theory.is_coseparating.is_codetecting
{C : Type uβ}
[category_theory.category C]
[category_theory.balanced C]
{π’ : set C} :
theorem
category_theory.is_detecting_iff_is_separating
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_equalizers C]
[category_theory.balanced C]
(π’ : set C) :
theorem
category_theory.is_codetecting_iff_is_coseparating
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_coequalizers C]
[category_theory.balanced C]
{π’ : set C} :
theorem
category_theory.is_separating.mono
{C : Type uβ}
[category_theory.category C]
{π’ : set C}
(hπ’ : category_theory.is_separating π’)
{β : set C}
(hπ’β : π’ β β) :
theorem
category_theory.is_coseparating.mono
{C : Type uβ}
[category_theory.category C]
{π’ : set C}
(hπ’ : category_theory.is_coseparating π’)
{β : set C}
(hπ’β : π’ β β) :
theorem
category_theory.is_detecting.mono
{C : Type uβ}
[category_theory.category C]
{π’ : set C}
(hπ’ : category_theory.is_detecting π’)
{β : set C}
(hπ’β : π’ β β) :
theorem
category_theory.is_codetecting.mono
{C : Type uβ}
[category_theory.category C]
{π’ : set C}
(hπ’ : category_theory.is_codetecting π’)
{β : set C}
(hπ’β : π’ β β) :
theorem
category_theory.thin_of_is_separating_empty
{C : Type uβ}
[category_theory.category C]
(h : category_theory.is_separating β
)
(X Y : C) :
subsingleton (X βΆ Y)
theorem
category_theory.is_separating_empty_of_thin
{C : Type uβ}
[category_theory.category C]
[β (X Y : C), subsingleton (X βΆ Y)] :
theorem
category_theory.thin_of_is_coseparating_empty
{C : Type uβ}
[category_theory.category C]
(h : category_theory.is_coseparating β
)
(X Y : C) :
subsingleton (X βΆ Y)
theorem
category_theory.is_coseparating_empty_of_thin
{C : Type uβ}
[category_theory.category C]
[β (X Y : C), subsingleton (X βΆ Y)] :
theorem
category_theory.groupoid_of_is_detecting_empty
{C : Type uβ}
[category_theory.category C]
(h : category_theory.is_detecting β
)
{X Y : C}
(f : X βΆ Y) :
theorem
category_theory.is_detecting_empty_of_groupoid
{C : Type uβ}
[category_theory.category C]
[β {X Y : C} (f : X βΆ Y), category_theory.is_iso f] :
theorem
category_theory.groupoid_of_is_codetecting_empty
{C : Type uβ}
[category_theory.category C]
(h : category_theory.is_codetecting β
)
{X Y : C}
(f : X βΆ Y) :
theorem
category_theory.is_codetecting_empty_of_groupoid
{C : Type uβ}
[category_theory.category C]
[β {X Y : C} (f : X βΆ Y), category_theory.is_iso f] :
theorem
category_theory.is_separating_iff_epi
{C : Type uβ}
[category_theory.category C]
(π’ : set C)
[β (A : C), category_theory.limits.has_coproduct (Ξ» (f : Ξ£ (G : β₯π’), βG βΆ A), β(f.fst))] :
category_theory.is_separating π’ β β (A : C), category_theory.epi (category_theory.limits.sigma.desc sigma.snd)
theorem
category_theory.is_coseparating_iff_mono
{C : Type uβ}
[category_theory.category C]
(π’ : set C)
[β (A : C), category_theory.limits.has_product (Ξ» (f : Ξ£ (G : β₯π’), A βΆ βG), β(f.fst))] :
category_theory.is_coseparating π’ β β (A : C), category_theory.mono (category_theory.limits.pi.lift sigma.snd)
theorem
category_theory.has_initial_of_is_coseparating
{C : Type uβ}
[category_theory.category C]
[category_theory.well_powered C]
[category_theory.limits.has_limits C]
{π’ : set C}
[small β₯π’]
(hπ’ : category_theory.is_coseparating π’) :
An ingredient of the proof of the Special Adjoint Functor Theorem: a complete well-powered category with a small coseparating set has an initial object.
In fact, it follows from the Special Adjoint Functor Theorem that C is already cocomplete.
theorem
category_theory.has_terminal_of_is_separating
{C : Type uβ}
[category_theory.category C]
[category_theory.well_powered Cα΅α΅]
[category_theory.limits.has_colimits C]
{π’ : set C}
[small β₯π’]
(hπ’ : category_theory.is_separating π’) :
An ingredient of the proof of the Special Adjoint Functor Theorem: a cocomplete well-copowered category with a small separating set has a terminal object.
In fact, it follows from the Special Adjoint Functor Theorem that C is already complete.
theorem
category_theory.subobject.eq_of_le_of_is_detecting
{C : Type uβ}
[category_theory.category C]
{π’ : set C}
(hπ’ : category_theory.is_detecting π’)
{X : C}
(P Q : category_theory.subobject X)
(hβ : P β€ Q)
(hβ : β (G : C), G β π’ β β {f : G βΆ X}, Q.factors f β P.factors f) :
P = Q
theorem
category_theory.subobject.inf_eq_of_is_detecting
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{π’ : set C}
(hπ’ : category_theory.is_detecting π’)
{X : C}
(P Q : category_theory.subobject X)
(h : β (G : C), G β π’ β β {f : G βΆ X}, P.factors f β Q.factors f) :
theorem
category_theory.subobject.eq_of_is_detecting
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{π’ : set C}
(hπ’ : category_theory.is_detecting π’)
{X : C}
(P Q : category_theory.subobject X)
(h : β (G : C), G β π’ β β {f : G βΆ X}, P.factors f β Q.factors f) :
P = Q
theorem
category_theory.well_powered_of_is_detecting
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{π’ : set C}
[small β₯π’]
(hπ’ : category_theory.is_detecting π’) :
A category with pullbacks and a small detecting set is well-powered.
theorem
category_theory.structured_arrow.is_coseparating_proj_preimage
{C : Type uβ}
[category_theory.category C]
{D : Type uβ}
[category_theory.category D]
(S : D)
(T : C β₯€ D)
{π’ : set C}
(hπ’ : category_theory.is_coseparating π’) :
theorem
category_theory.costructured_arrow.is_separating_proj_preimage
{C : Type uβ}
[category_theory.category C]
{D : Type uβ}
[category_theory.category D]
(S : C β₯€ D)
(T : D)
{π’ : set C}
(hπ’ : category_theory.is_separating π’) :
We say that G is a separator if the functor C(G, -) is faithful.
Equations
We say that G is a coseparator if the functor C(-, G) is faithful.
Equations
We say that G is a detector if the functor C(G, -) reflects isomorphisms.
Equations
We say that G is a codetector if the functor C(-, G) reflects isomorphisms.
Equations
theorem
category_theory.is_coseparator_op_iff
{C : Type uβ}
[category_theory.category C]
(G : C) :
theorem
category_theory.is_coseparator_unop_iff
{C : Type uβ}
[category_theory.category C]
(G : Cα΅α΅) :
theorem
category_theory.is_separator_unop_iff
{C : Type uβ}
[category_theory.category C]
(G : Cα΅α΅) :
theorem
category_theory.is_codetector_unop_iff
{C : Type uβ}
[category_theory.category C]
(G : Cα΅α΅) :
theorem
category_theory.is_detector_unop_iff
{C : Type uβ}
[category_theory.category C]
(G : Cα΅α΅) :
theorem
category_theory.is_detector.is_separator
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_equalizers C]
{G : C} :
theorem
category_theory.is_codetector.is_coseparator
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_coequalizers C]
{G : C} :
theorem
category_theory.is_separator.is_detector
{C : Type uβ}
[category_theory.category C]
[category_theory.balanced C]
{G : C} :
theorem
category_theory.is_cospearator.is_codetector
{C : Type uβ}
[category_theory.category C]
[category_theory.balanced C]
{G : C} :
theorem
category_theory.is_detector_def
{C : Type uβ}
[category_theory.category C]
(G : C) :
category_theory.is_detector G β β β¦X Y : Cβ¦ (f : X βΆ Y), (β (h : G βΆ Y), β! (h' : G βΆ X), h' β« f = h) β category_theory.is_iso f
theorem
category_theory.is_detector.def
{C : Type uβ}
[category_theory.category C]
{G : C} :
category_theory.is_detector G β β β¦X Y : Cβ¦ (f : X βΆ Y), (β (h : G βΆ Y), β! (h' : G βΆ X), h' β« f = h) β category_theory.is_iso f
theorem
category_theory.is_codetector_def
{C : Type uβ}
[category_theory.category C]
(G : C) :
category_theory.is_codetector G β β β¦X Y : Cβ¦ (f : X βΆ Y), (β (h : X βΆ G), β! (h' : Y βΆ G), f β« h' = h) β category_theory.is_iso f
theorem
category_theory.is_codetector.def
{C : Type uβ}
[category_theory.category C]
{G : C} :
category_theory.is_codetector G β β β¦X Y : Cβ¦ (f : X βΆ Y), (β (h : X βΆ G), β! (h' : Y βΆ G), f β« h' = h) β category_theory.is_iso f
theorem
category_theory.is_separator_iff_faithful_coyoneda_obj
{C : Type uβ}
[category_theory.category C]
(G : C) :
theorem
category_theory.is_coseparator_iff_faithful_yoneda_obj
{C : Type uβ}
[category_theory.category C]
(G : C) :
theorem
category_theory.is_separator_iff_epi
{C : Type uβ}
[category_theory.category C]
(G : C)
[β (A : C), category_theory.limits.has_coproduct (Ξ» (f : G βΆ A), G)] :
category_theory.is_separator G β β (A : C), category_theory.epi (category_theory.limits.sigma.desc (Ξ» (f : G βΆ A), f))
theorem
category_theory.is_coseparator_iff_mono
{C : Type uβ}
[category_theory.category C]
(G : C)
[β (A : C), category_theory.limits.has_product (Ξ» (f : A βΆ G), G)] :
category_theory.is_coseparator G β β (A : C), category_theory.mono (category_theory.limits.pi.lift (Ξ» (f : A βΆ G), f))
theorem
category_theory.is_separator_coprod
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(G H : C)
[category_theory.limits.has_binary_coproduct G H] :
category_theory.is_separator (G β¨Ώ H) β category_theory.is_separating {G, H}
theorem
category_theory.is_separator_coprod_of_is_separator_left
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(G H : C)
[category_theory.limits.has_binary_coproduct G H]
(hG : category_theory.is_separator G) :
theorem
category_theory.is_separator_coprod_of_is_separator_right
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(G H : C)
[category_theory.limits.has_binary_coproduct G H]
(hH : category_theory.is_separator H) :
theorem
category_theory.is_separator_sigma
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{Ξ² : Type w}
(f : Ξ² β C)
[category_theory.limits.has_coproduct f] :
theorem
category_theory.is_separator_sigma_of_is_separator
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{Ξ² : Type w}
(f : Ξ² β C)
[category_theory.limits.has_coproduct f]
(b : Ξ²)
(hb : category_theory.is_separator (f b)) :
theorem
category_theory.is_coseparator_prod
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(G H : C)
[category_theory.limits.has_binary_product G H] :
theorem
category_theory.is_coseparator_prod_of_is_coseparator_left
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(G H : C)
[category_theory.limits.has_binary_product G H]
(hG : category_theory.is_coseparator G) :
theorem
category_theory.is_coseparator_prod_of_is_coseparator_right
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(G H : C)
[category_theory.limits.has_binary_product G H]
(hH : category_theory.is_coseparator H) :
theorem
category_theory.is_coseparator_pi
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{Ξ² : Type w}
(f : Ξ² β C)
[category_theory.limits.has_product f] :
theorem
category_theory.is_coseparator_pi_of_is_coseparator
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{Ξ² : Type w}
(f : Ξ² β C)
[category_theory.limits.has_product f]
(b : Ξ²)
(hb : category_theory.is_coseparator (f b)) :
theorem
category_theory.is_detector_iff_reflects_isomorphisms_coyoneda_obj
{C : Type uβ}
[category_theory.category C]
(G : C) :
theorem
category_theory.is_codetector_iff_reflects_isomorphisms_yoneda_obj
{C : Type uβ}
[category_theory.category C]
(G : C) :
theorem
category_theory.well_powered_of_is_detector
{C : Type uβ}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
(G : C)
(hG : category_theory.is_detector G) :