mathlib documentation

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
@[instance]
Equations
@[simp]
@[simp]
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.

Equations

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

Equations

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₂) [equiv_functor m] :

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

Equations