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) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor C (Type w)

The functor mapping every object to PUnit.

Equations

• CategoryTheory.Limits.Types.constPUnitFunctor C = (CategoryTheory.Functor.const C).obj PUnit.{?u.21 + 1}

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

The cocone on constPUnitFunctor with cone point PUnit.

Equations

• CategoryTheory.Limits.Types.pUnitCocone C = { pt := PUnit.{?u.25 + 1}, ι := { app := fun (x : C) => id, naturality := ⋯ } }

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

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

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

Equations

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

theorem CategoryTheory.Limits.Types.zigzag_of_eqvGen_quot_rel (C : Type u) [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (c d : (j : C) × F.obj j) (h : Relation.EqvGen (CategoryTheory.Limits.Types.Quot.Rel F) c d) : CategoryTheory.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.

theorem CategoryTheory.Limits.Types.isConnected_iff_colimit_constPUnitFunctor_iso_pUnit (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.Types.constPUnitFunctor C)] : CategoryTheory.IsConnected C ↔ Nonempty (CategoryTheory.Limits.colimit (CategoryTheory.Limits.Types.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) [CategoryTheory.Category.{v, u} C] : CategoryTheory.IsConnected C ↔ Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.pUnitCocone C))

theorem CategoryTheory.Functor.isConnected_iff_of_final {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Final] : CategoryTheory.IsConnected C ↔ CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] : CategoryTheory.IsConnected C ↔ CategoryTheory.IsConnected D

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