# mathlibdocumentation

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

@[nolint]
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.

Equations
Instances for category_theory.core
@[protected, instance]
def category_theory.core_category {C : Type u₁}  :
Equations
@[simp]
theorem category_theory.core.id_hom {C : Type u₁} (X : category_theory.core C) :
(𝟙 X).hom = 𝟙 X
@[simp]
theorem category_theory.core.comp_hom {C : Type u₁} {X Y Z : category_theory.core C} (f : X Y) (g : Y Z) :
(f g).hom = f.hom g.hom
def category_theory.core.inclusion (C : Type u₁)  :

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

Equations
Instances for category_theory.core.inclusion
@[protected, instance]
noncomputable def category_theory.core.functor_to_core {C : Type u₁} {G : Type u₂} (F : G C) :

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

Equations
def category_theory.core.forget_functor_to_core {C : Type u₁} {G : Type u₂}  :
G 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.

Equations
def category_theory.of_equiv_functor (m : Type u₁Type u₂)  :

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

Equations