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

The functor mapping every object to PUnit.

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

    The cocone on constPUnitFunctor with cone point PUnit.

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance CategoryTheory.Limits.Types.instHasColimitConstPUnitFunctor (C : Type u) [Category.{v, u} C] [IsConnected C] :
        HasColimit (constPUnitFunctor C)
        source
        instance CategoryTheory.Limits.Types.instSubsingletonColimitPUnit (C : Type u) [Category.{v, u} C] [IsPreconnected C] [HasColimit (constPUnitFunctor C)] :
        Subsingleton (colimit (constPUnitFunctor C))
        source
        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.

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

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

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

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

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

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

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