mathlib documentation

category_theory.is_connected

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:

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 category_theory.limits.connected.

@[class]
structure category_theory.is_preconnected (J : Type v₂) [category_theory.category J] :
Prop

A possibly empty category for which every functor to a discrete category is constant.

Instances
@[class]
structure category_theory.is_connected (J : Type v₂) [category_theory.category J] :
Prop

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

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
theorem category_theory.any_functor_const_on_obj {J : Type v₂} [category_theory.category J] [category_theory.is_preconnected J] {α : Type v₂} (F : J category_theory.discrete α) (j j' : J) :
F.obj j = F.obj j'

If J is connected, any functor to a discrete category is constant on objects. The converse is given in is_connected.of_any_functor_const_on_obj.

theorem category_theory.is_connected.of_any_functor_const_on_obj {J : Type v₂} [category_theory.category J] [nonempty J] :
(∀ {α : Type v₂} (F : J category_theory.discrete α) (j j' : J), F.obj j = F.obj j')category_theory.is_connected J

If any functor to a discrete category is constant on objects, J is connected. The converse of any_functor_const_on_obj.

theorem category_theory.constant_of_preserves_morphisms {J : Type v₂} [category_theory.category J] [category_theory.is_preconnected J] {α : Type v₂} (F : J → α) (h : ∀ (j₁ j₂ : J), (j₁ j₂)F j₁ = F j₂) (j j' : J) :
F j = F j'

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 is_connected.of_constant_of_preserves_morphisms

theorem category_theory.is_connected.of_constant_of_preserves_morphisms {J : Type v₂} [category_theory.category J] [nonempty J] :
(∀ {α : Type v₂} (F : J → α), (∀ {j₁ j₂ : J}, (j₁ j₂)F j₁ = F j₂)∀ (j j' : J), F j = F j')category_theory.is_connected J

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.

theorem category_theory.induct_on_objects {J : Type v₂} [category_theory.category J] [category_theory.is_preconnected J] (p : set J) {j₀ : J} (h0 : j₀ p) (h1 : ∀ {j₁ j₂ : J}, (j₁ j₂)(j₁ p j₂ p)) (j : J) :
j p

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 is_connected.of_induct.

theorem category_theory.is_connected.of_induct {J : Type v₂} [category_theory.category J] [nonempty J] {j₀ : J} :
(∀ (p : set J), j₀ p(∀ {j₁ j₂ : J}, (j₁ j₂)(j₁ p j₂ p))∀ (j : J), j p)category_theory.is_connected J

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.

theorem category_theory.is_preconnected_induction {J : Type v₂} [category_theory.category J] [category_theory.is_preconnected J] (Z : J → Sort u_1) (h₁ : Π {j₁ j₂ : J}, (j₁ j₂)Z j₁Z j₂) (h₂ : Π {j₁ j₂ : J}, (j₁ j₂)Z j₂Z j₁) {j₀ : J} (x : Z j₀) (j : J) :
nonempty (Z j)

Another induction principle for is_preconnected 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.

def category_theory.zag {J : Type v₂} [category_theory.category J] :
J → J → Prop

j₁ and j₂ are related by zag if there is a morphism between them.

Equations
def category_theory.zigzag {J : Type v₂} [category_theory.category J] :
J → J → Prop

j₁ and j₂ are related by zigzag if there is a chain of morphisms from j₁ to j₂, with backward morphisms allowed.

Equations
theorem category_theory.equiv_relation {J : Type v₂} [category_theory.category J] [category_theory.is_connected J] (r : J → J → Prop) (hr : equivalence r) (h : ∀ {j₁ j₂ : J}, (j₁ j₂)r j₁ j₂) (j₁ j₂ : J) :
r j₁ j₂

Any equivalence relation containing (⟶) holds for all pairs of a connected category.

In a connected category, any two objects are related by zigzag.

theorem category_theory.zigzag_is_connected {J : Type v₂} [category_theory.category J] [nonempty J] :
(∀ (j₁ j₂ : J), category_theory.zigzag j₁ j₂)category_theory.is_connected J

If any two objects in an nonempty category are related by zigzag, the category is connected.

theorem category_theory.exists_zigzag' {J : Type v₂} [category_theory.category J] [category_theory.is_connected J] (j₁ j₂ : J) :
∃ (l : list J), list.chain category_theory.zag j₁ l (j₁ :: l).last _ = j₂

theorem category_theory.is_connected_of_zigzag {J : Type v₂} [category_theory.category J] [nonempty J] :
(∀ (j₁ j₂ : J), ∃ (l : list J), list.chain category_theory.zag j₁ l (j₁ :: l).last _ = j₂)category_theory.is_connected J

If any two objects in an nonempty category are linked by a sequence of (potentially reversed) morphisms, then J is connected.

The converse of exists_zigzag'.

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.