Documentation

Mathlib.CategoryTheory.Limits.IsConnected

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

source
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
Instances For
    source
    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
    Instances For
      source
      @[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
      source
      @[simp]
      theorem CategoryTheory.Limits.Types.pUnitCocone_pt (C : Type u) [CategoryTheory.Category.{v, u} C] :
      (CategoryTheory.Limits.Types.pUnitCocone C).pt = PUnit.{w + 1}
      source
      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.
      Instances For
        source
        instance CategoryTheory.Limits.Types.instHasColimitConstPUnitFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsConnected C] :
        CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.Types.constPUnitFunctor C)
        Equations
        • ⋯ = ⋯
        source
        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))
        Equations
        • ⋯ = ⋯
        source
        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.
        Instances For
          source
          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.

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

          source
          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))
          source
          theorem CategoryTheory.Limits.Types.isConnected_iff_of_final {C : Type u} {D : Type u₂} [CategoryTheory.Category.{v, u} C] [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.