Colimits of connected index categories

This file proves two characterizations of connected categories by means of colimits.

Characterization of connected categories by means of the unit-valued functor

First, it is proved that a category C is connected if and only if colim F is a singleton, where F : C ⥤ Type w and F.obj _ = PUnit (for arbitrary w).

See isConnected_iff_colimit_constPUnitFunctor_iso_pUnit for the proof of this characterization and constPUnitFunctor for the definition of the constant functor used in the statement. A formulation based on IsColimit instead of colimit is given in isConnected_iff_isColimit_pUnitCocone.

The if direction is also available directly in several formulations: For connected index categories C, PUnit.{w} is a colimit of the constPUnitFunctor, where w is arbitrary. See instHasColimitConstPUnitFunctor, isColimitPUnitCocone and colimitConstPUnitIsoPUnit.

Final functors preserve connectedness of categories (in both directions)

isConnected_iff_of_final proves that the domain of a final functor is connected if and only if its codomain is connected.

Tags

unit-valued, singleton, colimit

def CategoryTheory.Limits.Types.constPUnitFunctor (C : Type u) [Category.{v, u} C] : Functor C (Type w)

The functor mapping every object to PUnit.

def CategoryTheory.Limits.Types.pUnitCocone (C : Type u) [Category.{v, u} C] : Cocone (constPUnitFunctor C)

The cocone on constPUnitFunctor with cone point PUnit.

@[simp]

theorem CategoryTheory.Limits.Types.pUnitCocone_ι_app (C : Type u) [Category.{v, u} C] (x✝ : C) (a : (constPUnitFunctor C).obj x✝) : (pUnitCocone C).ι.app x✝ a = id a

@[simp]

theorem CategoryTheory.Limits.Types.pUnitCocone_pt (C : Type u) [Category.{v, u} C] : (pUnitCocone C).pt = PUnit.{w + 1}

noncomputable def CategoryTheory.Limits.Types.isColimitPUnitCocone (C : Type u) [Category.{v, u} C] [IsConnected C] : IsColimit (pUnitCocone C)

If C is connected, the cocone on constPUnitFunctor with cone point PUnit is a colimit cocone.

instance CategoryTheory.Limits.Types.instHasColimitConstPUnitFunctor (C : Type u) [Category.{v, u} C] [IsConnected C] : HasColimit (constPUnitFunctor C)

instance CategoryTheory.Limits.Types.instSubsingletonColimitPUnit (C : Type u) [Category.{v, u} C] [IsPreconnected C] [HasColimit (constPUnitFunctor C)] : Subsingleton (colimit (constPUnitFunctor C))

noncomputable def CategoryTheory.Limits.Types.colimitConstPUnitIsoPUnit (C : Type u) [Category.{v, u} C] [IsConnected C] : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}

Given a connected index category, the colimit of the constant unit-valued functor is PUnit.

theorem CategoryTheory.Limits.Types.zigzag_of_eqvGen_colimitTypeRel (C : Type u) [Category.{v, u} C] (F : Functor C (Type w)) (c d : (j : C) × F.obj j) (h : Relation.EqvGen F.ColimitTypeRel c d) : Zigzag c.fst d.fst

Let F be a Type-valued functor. If two elements a : F c and b : F d represent the same element of colimit F, then c and d are related by a Zigzag.

@[deprecated CategoryTheory.Limits.Types.zigzag_of_eqvGen_colimitTypeRel (since := "2025-06-22")]

theorem CategoryTheory.Limits.Types.zigzag_of_eqvGen_quot_rel (C : Type u) [Category.{v, u} C] (F : Functor C (Type w)) (c d : (j : C) × F.obj j) (h : Relation.EqvGen F.ColimitTypeRel c d) : Zigzag c.fst d.fst

Alias of CategoryTheory.Limits.Types.zigzag_of_eqvGen_colimitTypeRel.

---

Let F be a Type-valued functor. If two elements a : F c and b : F d represent the same element of colimit F, then c and d are related by a Zigzag.

theorem CategoryTheory.Limits.Types.isConnected_iff_colimit_constPUnitFunctor_iso_pUnit (C : Type u) [Category.{v, u} C] [HasColimit (constPUnitFunctor C)] : IsConnected C ↔ Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})

An index category is connected iff the colimit of the constant singleton-valued functor is a singleton.

theorem CategoryTheory.Limits.Types.isConnected_iff_isColimit_pUnitCocone (C : Type u) [Category.{v, u} C] : IsConnected C ↔ Nonempty (IsColimit (pUnitCocone C))

theorem CategoryTheory.Functor.isConnected_iff_of_final {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.Final] : IsConnected C ↔ IsConnected D

The domain of a final functor is connected if and only if its codomain is connected.

theorem CategoryTheory.Functor.isConnected_iff_of_initial {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.Initial] : IsConnected C ↔ IsConnected D

The domain of an initial functor is connected if and only if its codomain is connected.

theorem CategoryTheory.isConnected_of_isInitial (C : Type u_1) [Category.{u_2, u_1} C] {x : C} (h : Limits.IsInitial x) : IsConnected C

Prove that a category is connected by supplying an explicit initial object.

theorem CategoryTheory.isConnected_of_isTerminal (C : Type u_1) [Category.{u_2, u_1} C] {x : C} (h : Limits.IsTerminal x) : IsConnected C

Prove that a category is connected by supplying an explicit terminal object.

theorem CategoryTheory.isConnected_of_hasInitial (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasInitial C] : IsConnected C

theorem CategoryTheory.isConnected_of_hasTerminal (C : Type u_1) [Category.{u_2, u_1} C] [Limits.HasTerminal C] : IsConnected C