Documentation

Mathlib.CategoryTheory.Core

The core of a category #

The core of a category C is the (non-full) subcategory of C consisting of all objects, and all isomorphisms. We construct it as a CategoryTheory.Groupoid.

CategoryTheory.Core.inclusion : Core C ⥤ C gives the faithful inclusion into the original category.

Any functor F from a groupoid G into C factors through CategoryTheory.Core C, but this is not functorial with respect to F.

def CategoryTheory.Core (C : Type u₁) :
Type u₁

The core of a category C is the groupoid whose morphisms are all the isomorphisms of C.

Equations
Instances For

    The core of a category is naturally included in the category.

    Equations
    Instances For

      A functor from a groupoid to a category C factors through the core of C.

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

        We can functorially associate to any functor from a groupoid to the core of a category C, a functor from the groupoid to C, simply by composing with the embedding Core C ⥤ C.

        Equations
        Instances For

          ofEquivFunctor m lifts a type-level EquivFunctor to a categorical functor Core (Type u₁) ⥤ Core (Type u₂).

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