mathlib documentation

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]

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