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

• CategoryTheory.Core C = C

instance CategoryTheory.coreCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Groupoid (CategoryTheory.Core C)

Equations

• CategoryTheory.coreCategory = CategoryTheory.Groupoid.mk fun {X Y : CategoryTheory.Core C} (f : X ⟶ Y) => f.symm

@[simp]

theorem CategoryTheory.Core.id_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Core.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : CategoryTheory.Core C} {Y : CategoryTheory.Core C} {Z : CategoryTheory.Core C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

def CategoryTheory.Core.inclusion (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Functor (CategoryTheory.Core C) C

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

Equations

• CategoryTheory.Core.inclusion C = CategoryTheory.Functor.mk { obj := id, map := fun {X Y : CategoryTheory.Core C} (f : X ⟶ Y) => f.hom }

instance CategoryTheory.Core.instFaithfulCoreToCategoryCoreCategoryInclusion (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Faithful (CategoryTheory.Core.inclusion C)

Equations

• (_ : CategoryTheory.Faithful (CategoryTheory.Core.inclusion C)) = (_ : CategoryTheory.Faithful (CategoryTheory.Core.inclusion C))

noncomputable def CategoryTheory.Core.functorToCore {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : Type u₂} [CategoryTheory.Groupoid G] (F : CategoryTheory.Functor G C) : CategoryTheory.Functor G (CategoryTheory.Core C)

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.

def CategoryTheory.Core.forgetFunctorToCore {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : Type u₂} [CategoryTheory.Groupoid G] : CategoryTheory.Functor (CategoryTheory.Functor G (CategoryTheory.Core C)) (CategoryTheory.Functor 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

• CategoryTheory.Core.forgetFunctorToCore = (CategoryTheory.whiskeringRight G (CategoryTheory.Core C) C).toPrefunctor.obj (CategoryTheory.Core.inclusion C)

def CategoryTheory.ofEquivFunctor (m : Type u₁ → Type u₂) [EquivFunctor m] : CategoryTheory.Functor (CategoryTheory.Core (Type u₁)) (CategoryTheory.Core (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.