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 × -). This appears in CategoryTheory.Limits.Connected.

class CategoryTheory.IsPreconnected (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] : Prop

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).toPrefunctor.obj (F.toPrefunctor.obj j))

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

class CategoryTheory.IsConnected (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] extends CategoryTheory.IsPreconnected : 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

• iso_constant : ∀ {α : Type u₁} (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j : J), Nonempty (F ≅ (CategoryTheory.Functor.const J).toPrefunctor.obj (F.toPrefunctor.obj j))
• is_nonempty : Nonempty J

def CategoryTheory.isoConstant {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected J] {α : Type u₂} (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j : J) : F ≅ (CategoryTheory.Functor.const J).toPrefunctor.obj (F.toPrefunctor.obj j)

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.

theorem CategoryTheory.any_functor_const_on_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected J] {α : Type u₂} (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j : J) (j' : J) : F.toPrefunctor.obj j = F.toPrefunctor.obj j'

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.

theorem CategoryTheory.IsConnected.of_any_functor_const_on_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [Nonempty J] (h : ∀ {α : Type u₁} (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j j' : J), F.toPrefunctor.obj j = F.toPrefunctor.obj j') : CategoryTheory.IsConnected J

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

theorem CategoryTheory.constant_of_preserves_morphisms {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected J] {α : Type u₂} (F : J → α) (h : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → F j₁ = F j₂) (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 IsConnected.of_constant_of_preserves_morphisms

theorem CategoryTheory.IsConnected.of_constant_of_preserves_morphisms {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [Nonempty J] (h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂) → ∀ (j j' : J), F j = F j') : CategoryTheory.IsConnected 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 CategoryTheory.induct_on_objects {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected 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 IsConnected.of_induct.

theorem CategoryTheory.IsConnected.of_induct {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [Nonempty J] {j₀ : J} (h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p) : CategoryTheory.IsConnected 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.

instance CategoryTheory.instIsConnectedULiftHomULiftCategoryUliftCategory {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [hc : CategoryTheory.IsConnected J] : CategoryTheory.IsConnected (CategoryTheory.ULiftHom (ULift.{u₂, u₁} J))

Lifting the universe level of morphisms and objects preserves connectedness.

Equations

• (_ : CategoryTheory.IsConnected (CategoryTheory.ULiftHom (ULift.{u₂, u₁} J))) = (_ : CategoryTheory.IsConnected (CategoryTheory.ULiftHom (ULift.{u₂, u₁} J)))

theorem CategoryTheory.isPreconnected_induction {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected 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 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.

theorem CategoryTheory.isPreconnected_of_equivalent {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.IsPreconnected J] (e : J ≌ K) : CategoryTheory.IsPreconnected K

If J and K are equivalent, then if J is preconnected then K is as well.

theorem CategoryTheory.isConnected_of_equivalent {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (e : J ≌ K) [CategoryTheory.IsConnected J] : CategoryTheory.IsConnected K

If J and K are equivalent, then if J is connected then K is as well.

instance CategoryTheory.isPreconnected_op {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected J] : CategoryTheory.IsPreconnected Jᵒᵖ

If J is preconnected, then Jᵒᵖ is preconnected as well.

Equations

• (_ : CategoryTheory.IsPreconnected Jᵒᵖ) = (_ : CategoryTheory.IsPreconnected Jᵒᵖ)

instance CategoryTheory.isConnected_op {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsConnected J] : CategoryTheory.IsConnected Jᵒᵖ

If J is connected, then Jᵒᵖ is connected as well.

Equations

• (_ : CategoryTheory.IsConnected Jᵒᵖ) = (_ : CategoryTheory.IsConnected Jᵒᵖ)

theorem CategoryTheory.isPreconnected_of_isPreconnected_op {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected Jᵒᵖ] : CategoryTheory.IsPreconnected J

theorem CategoryTheory.isConnected_of_isConnected_op {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsConnected Jᵒᵖ] : CategoryTheory.IsConnected J

@[reducible]

def CategoryTheory.Zag {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] (j₁ : J) (j₂ : J) : Prop

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

Equations

• CategoryTheory.Zag j₁ j₂ = (Nonempty (j₁ ⟶ j₂) ∨ Nonempty (j₂ ⟶ j₁))

theorem CategoryTheory.zag_symmetric {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] : Symmetric CategoryTheory.Zag

@[reducible]

def CategoryTheory.Zigzag {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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

• CategoryTheory.Zigzag = Relation.ReflTransGen CategoryTheory.Zag

theorem CategoryTheory.zigzag_symmetric {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] : Symmetric CategoryTheory.Zigzag

theorem CategoryTheory.zigzag_equivalence {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] : Equivalence CategoryTheory.Zigzag

def CategoryTheory.Zigzag.setoid (J : Type u₂) [CategoryTheory.Category.{v₁, u₂} J] : Setoid J

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 := (_ : Equivalence CategoryTheory.Zigzag) }

theorem CategoryTheory.zigzag_obj_of_zigzag {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J K) {j₁ : J} {j₂ : J} (h : CategoryTheory.Zigzag j₁ j₂) : CategoryTheory.Zigzag (F.toPrefunctor.obj j₁) (F.toPrefunctor.obj j₂)

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.

theorem CategoryTheory.zag_of_zag_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J K) [CategoryTheory.Full F] {j₁ : J} {j₂ : J} (h : CategoryTheory.Zag (F.toPrefunctor.obj j₁) (F.toPrefunctor.obj j₂)) : CategoryTheory.Zag j₁ j₂

theorem CategoryTheory.equiv_relation {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsConnected J] (r : J → J → Prop) (hr : Equivalence r) (h : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → r j₁ j₂) (j₁ : J) (j₂ : J) : r j₁ j₂

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

theorem CategoryTheory.isConnected_zigzag {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsConnected J] (j₁ : J) (j₂ : J) : CategoryTheory.Zigzag j₁ j₂

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

theorem CategoryTheory.zigzag_isConnected {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [Nonempty J] (h : ∀ (j₁ j₂ : J), CategoryTheory.Zigzag j₁ j₂) : CategoryTheory.IsConnected J

If any two objects in a nonempty category are related by Zigzag, the category is connected.

theorem CategoryTheory.exists_zigzag' {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsConnected J] (j₁ : J) (j₂ : J) : ∃ (l : List J), List.Chain CategoryTheory.Zag j₁ l ∧ List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂

theorem CategoryTheory.isConnected_of_zigzag {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [Nonempty J] (h : ∀ (j₁ j₂ : J), ∃ (l : List J), List.Chain CategoryTheory.Zag j₁ l ∧ List.getLast (j₁ :: l) (_ : j₁ :: l ≠ []) = j₂) : CategoryTheory.IsConnected J

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'.

def CategoryTheory.discreteIsConnectedEquivPUnit {α : Type u₁} [CategoryTheory.IsConnected (CategoryTheory.Discrete α)] : α ≃ PUnit.{u₁ + 1}

If Discrete α is connected, then α is (type-)equivalent to PUnit.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.nat_trans_from_is_connected {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{u₁, u₂} C] [CategoryTheory.IsPreconnected J] {X : C} {Y : C} (α : (CategoryTheory.Functor.const J).toPrefunctor.obj X ⟶ (CategoryTheory.Functor.const J).toPrefunctor.obj Y) (j : J) (j' : J) : α.app j = α.app 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.

instance CategoryTheory.instFullFunctorCategoryConst {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{u₁, u₂} C] [CategoryTheory.IsConnected J] : CategoryTheory.Full (CategoryTheory.Functor.const J)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.nonempty_hom_of_connected_groupoid {G : Type u_1} [CategoryTheory.Groupoid G] [CategoryTheory.IsConnected G] (x : G) (y : G) : Nonempty (x ⟶ y)

Equations

• (_ : ∀ (x y : G), Nonempty (x ⟶ y)) = (_ : ∀ (j₁ j₂ : G), Nonempty (j₁ ⟶ j₂))