Connected category #
Define a connected category as a nonempty category for which every functor to a discrete category is isomorphic to the constant functor.
NB. Some authors include the empty category as connected, we do not. We instead are interested in categories with exactly one 'connected component'.
We give some equivalent definitions:
- A nonempty category for which every functor to a discrete category is
constant on objects.
See
any_functor_const_on_obj
andConnected.of_any_functor_const_on_obj
. - A nonempty category for which every function
F
for which the presence of a morphismf : j₁ ⟶ j₂
impliesF j₁ = F j₂
must be constant everywhere. Seeconstant_of_preserves_morphisms
andConnected.of_constant_of_preserves_morphisms
. - A nonempty category for which any subset of its elements containing the
default and closed under morphisms is everything.
See
induct_on_objects
andConnected.of_induct
. - A nonempty category for which every object is related under the reflexive
transitive closure of the relation "there is a morphism in some direction
from
j₁
toj₂
". Seeconnected_zigzag
andzigzag_connected
. - A nonempty category for which for any two objects there is a sequence of
morphisms (some reversed) from one to the other.
See
exists_zigzag'
andconnected_of_zigzag
.
We also prove the result that the functor given by (X × -)
preserves any
connected limit. That is, any limit of shape J
where J
is a connected
category is preserved by the functor (X × -)
. This appears in CategoryTheory.Limits.Connected
.
A possibly empty category for which every functor to a discrete category is constant.
- iso_constant : ∀ {α : Type u₁} (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j : J), Nonempty (F ≅ (CategoryTheory.Functor.const J).obj (F.obj j))
A possibly empty category for which every functor to a discrete category is constant.
Instances
A possibly empty category for which every functor to a discrete category is constant.
We define a connected category as a nonempty category for which every functor to a discrete category is constant.
NB. Some authors include the empty category as connected, we do not. We instead are interested in categories with exactly one 'connected component'.
This allows us to show that the functor X ⨯ - preserves connected limits.
See https://stacks.math.columbia.edu/tag/002S
- iso_constant : ∀ {α : Type u₁} (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j : J), Nonempty (F ≅ (CategoryTheory.Functor.const J).obj (F.obj j))
- is_nonempty : Nonempty J
Instances
If J
is connected, any functor F : J ⥤ Discrete α
is isomorphic to
the constant functor with value F.obj j
(for any choice of j
).
Equations
- One or more equations did not get rendered due to their size.
Instances For
If J
is connected, any functor to a discrete category is constant on objects.
The converse is given in IsConnected.of_any_functor_const_on_obj
.
If any functor to a discrete category is constant on objects, J is connected.
The converse of any_functor_const_on_obj
.
If any functor to a discrete category is constant on objects, J is connected.
The converse of any_functor_const_on_obj
.
If J
is connected, then given any function F
such that the presence of a
morphism j₁ ⟶ j₂
implies F j₁ = F j₂
, we have that F
is constant.
This can be thought of as a local-to-global property.
The converse is shown in IsConnected.of_constant_of_preserves_morphisms
J
is connected if: given any function F : J → α
which is constant for any
j₁, j₂
for which there is a morphism j₁ ⟶ j₂
, then F
is constant.
This can be thought of as a local-to-global property.
The converse of constant_of_preserves_morphisms
.
J
is connected if: given any function F : J → α
which is constant for any
j₁, j₂
for which there is a morphism j₁ ⟶ j₂
, then F
is constant.
This can be thought of as a local-to-global property.
The converse of constant_of_preserves_morphisms
.
An inductive-like property for the objects of a connected category.
If the set p
is nonempty, and p
is closed under morphisms of J
,
then p
contains all of J
.
The converse is given in IsConnected.of_induct
.
If any maximal connected component containing some element j₀ of J is all of J, then J is connected.
The converse of induct_on_objects
.
Lifting the universe level of morphisms and objects preserves connectedness.
Equations
- ⋯ = ⋯
Another induction principle for IsPreconnected J
:
given a type family Z : J → Sort*
and
a rule for transporting in both directions along a morphism in J
,
we can transport an x : Z j₀
to a point in Z j
for any j
.
If J
and K
are equivalent, then if J
is preconnected then K
is as well.
If J
and K
are equivalent, then if J
is connected then K
is as well.
If J
is preconnected, then Jᵒᵖ
is preconnected as well.
Equations
- ⋯ = ⋯
If J
is connected, then Jᵒᵖ
is connected as well.
Equations
- ⋯ = ⋯
j₁ and j₂ are related by Zag
if there is a morphism between them.
Instances For
j₁
and j₂
are related by Zigzag
if there is a chain of
morphisms from j₁
to j₂
, with backward morphisms allowed.
Equations
- CategoryTheory.Zigzag = Relation.ReflTransGen CategoryTheory.Zag
Instances For
The setoid given by the equivalence relation Zigzag
. A quotient for this
setoid is a connected component of the category.
Equations
- CategoryTheory.Zigzag.setoid J = { r := CategoryTheory.Zigzag, iseqv := ⋯ }
Instances For
If there is a zigzag from j₁
to j₂
, then there is a zigzag from F j₁
to
F j₂
as long as F
is a functor.
A Zag in a discrete category entails an equality of its extremities
A zigzag in a discrete category entails an equality of its extremities
Any equivalence relation containing (⟶) holds for all pairs of a connected category.
In a connected category, any two objects are related by Zigzag
.
Alias of CategoryTheory.isPreconnected_zigzag
.
In a connected category, any two objects are related by Zigzag
.
If any two objects in a nonempty category are related by Zigzag
, the category is connected.
If any two objects in a nonempty category are linked by a sequence of (potentially reversed) morphisms, then J is connected.
The converse of exists_zigzag'
.
If any two objects in a nonempty category are linked by a sequence of (potentially reversed) morphisms, then J is connected.
The converse of exists_zigzag'
.
If Discrete α
is connected, then α
is (type-)equivalent to PUnit
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For objects X Y : C
, any natural transformation α : const X ⟶ const Y
from a connected
category must be constant.
This is the key property of connected categories which we use to establish properties about limits.
Equations
- ⋯ = ⋯
Alias of CategoryTheory.nonempty_hom_of_preconnected_groupoid
.