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 and connected.of_any_functor_const_on_obj.
A nonempty category for which every function F for which the presence of a morphism f : j₁ ⟶ j₂ implies F j₁ = F j₂ must be constant everywhere. See constant_of_preserves_morphisms and connected.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 and connected.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₁ to j₂". See connected_zigzag and zigzag_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' and connected_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 × -).

source

@[class]

structure category_theory.connected (J : Type v₂) [category_theory.category J] :

Type (max v₁ (v₂+1))

to_inhabited : inhabited J
iso_constant : Π {α : Type ?} (F : J ⥤ category_theory.discrete α), F ≅ (category_theory.functor.const J).obj (F.obj (inhabited.default J))

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.

Instances

source

theorem category_theory.any_functor_const_on_obj {J : Type v₂} [category_theory.category J] [category_theory.connected J] {α : Type v₂} (F : J ⥤ category_theory.discrete α) (j : J) :

F.obj j = F.obj (inhabited.default J)

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

source

def category_theory.connected.of_any_functor_const_on_obj {J : Type v₂} [category_theory.category J] [inhabited J] :

(∀ {α : Type v₂} (F : J ⥤ category_theory.discrete α) (j : J), F.obj j = F.obj (inhabited.default J)) → category_theory.connected J

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

Equations

category_theory.connected.of_any_functor_const_on_obj h = {to_inhabited := _inst_2, iso_constant := λ (α : Type v₂) (F : J ⥤ category_theory.discrete α), category_theory.nat_iso.of_components (λ (B : J), category_theory.eq_to_iso _) _}

source

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

F j = F (inhabited.default 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 connected.of_constant_of_preserves_morphisms

source

def category_theory.connected.of_constant_of_preserves_morphisms {J : Type v₂} [category_theory.category J] [inhabited J] :

(∀ {α : Type v₂} (F : J → α), (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂) → ∀ (j : J), F j = F (inhabited.default J)) → category_theory.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.

Equations

category_theory.connected.of_constant_of_preserves_morphisms h = category_theory.connected.of_any_functor_const_on_obj _

source

theorem category_theory.induct_on_objects {J : Type v₂} [category_theory.category J] [category_theory.connected J] (p : set J) (h0 : inhabited.default 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 default J is in the set p, and p is closed under morphisms of J, then p contains all of J.

The converse is given in connected.of_induct.

source

def category_theory.connected.of_induct {J : Type v₂} [category_theory.category J] [inhabited J] :

(∀ (p : set J), inhabited.default J ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p) → category_theory.connected J

If any maximal connected component of J containing the default is all of J, then J is connected.

The converse of induct_on_objects.

Equations

category_theory.connected.of_induct h = category_theory.connected.of_constant_of_preserves_morphisms _

source

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

category_theory.zag j₁ j₂ = (nonempty (j₁ ⟶ j₂) ∨ nonempty (j₂ ⟶ j₁))

source

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

category_theory.zigzag = relation.refl_trans_gen category_theory.zag

source

theorem category_theory.equiv_relation {J : Type v₂} [category_theory.category J] [category_theory.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.

source

theorem category_theory.connected_zigzag {J : Type v₂} [category_theory.category J] [category_theory.connected J] (j₁ j₂ : J) :

category_theory.zigzag j₁ j₂

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

source

def category_theory.zigzag_connected {J : Type v₂} [category_theory.category J] [inhabited J] :

(∀ (j₁ j₂ : J), category_theory.zigzag j₁ j₂) → category_theory.connected J

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

Equations

category_theory.zigzag_connected h = category_theory.connected.of_induct _

source

theorem category_theory.exists_zigzag' {J : Type v₂} [category_theory.category J] [category_theory.connected J] (j₁ j₂ : J) :

∃ (l : list J), list.chain category_theory.zag j₁ l ∧ (j₁ :: l).last _ = j₂

source

def category_theory.connected_of_zigzag {J : Type v₂} [category_theory.category J] [inhabited J] :

(∀ (j₁ j₂ : J), ∃ (l : list J), list.chain category_theory.zag j₁ l ∧ (j₁ :: l).last _ = j₂) → category_theory.connected J

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

The converse of exists_zigzag'.

Equations

category_theory.connected_of_zigzag h = category_theory.connected.of_induct _

source

def category_theory.discrete_connected_equiv_punit {α : Type (max u_1 u_2)} [category_theory.connected (category_theory.discrete α)] :

α ≃ punit

If discrete α is connected, then α is (type-)equivalent to punit.

Equations

source

theorem category_theory.nat_trans_from_connected {J : Type v₂} [category_theory.category J] {C : Type u₂} [category_theory.category C] [conn : category_theory.connected J] {X Y : C} (α : (category_theory.functor.const J).obj X ⟶ (category_theory.functor.const J).obj Y) (j : J) :

α.app j = α.app (inhabited.default J)

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.

mathlib documentation

category_theory.connected

Connected category

General documentation

Additional documentation

Library

mathlib documentation

category_theory.​connected

Connected category

General documentation

Additional documentation

Library

category_theory.connected