# mathlibdocumentation

category_theory.core

@[nolint]
def category_theory.core  :
Type u₁Type u₁

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

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