mathlib documentation


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

core.inclusion : core C ⥤ C gives the faithful inclusion into the original category.

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

def category_theory.core (C : Type u₁) :
Type u₁

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

Instances for category_theory.core
@[protected, instance]
theorem category_theory.core.comp_hom {C : Type u₁} [category_theory.category C] {X Y Z : category_theory.core C} (f : X Y) (g : Y Z) :
(f g).hom = f.hom g.hom

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

Instances for category_theory.core.inclusion
noncomputable def category_theory.core.functor_to_core {C : Type u₁} [category_theory.category C] {G : Type u₂} [category_theory.groupoid G] (F : G C) :

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


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.

def category_theory.of_equiv_functor (m : Type u₁Type u₂) [equiv_functor m] :

of_equiv_functor m lifts a type-level equiv_functor to a categorical functor core (Type u₁) ⥤ core (Type u₂).