# 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
instance CategoryTheory.coreCategory {C : Type u₁} [] :
Equations
@[simp]
theorem CategoryTheory.Core.id_hom {C : Type u₁} [] (X : C) :
@[simp]
theorem CategoryTheory.Core.comp_hom {C : Type u₁} [] {X : } {Y : } {Z : } (f : X Y) (g : Y Z) :

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

Equations
• = { obj := id, map := fun {X Y : } (f : X Y) => f.hom, map_id := , map_comp := }
Instances For
instance CategoryTheory.Core.instFaithfulInclusion (C : Type u₁) [] :
.Faithful
Equations
• =
def CategoryTheory.Core.functorToCore {C : Type u₁} [] {G : Type u₂} (F : ) :

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
def CategoryTheory.Core.forgetFunctorToCore {C : Type u₁} [] {G : Type u₂} :

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
• CategoryTheory.Core.forgetFunctorToCore =
Instances For
def CategoryTheory.ofEquivFunctor (m : Type u₁ → Type u₂) [] :

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