The core of a category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

@[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

category_theory.core C = C

Instances for category_theory.core

category_theory.core_category

source

@[protected, instance]

def category_theory.core_category {C : Type u₁} [category_theory.category C] :

category_theory.groupoid (category_theory.core C)

Equations

category_theory.core_category = {to_category := {to_category_struct := {to_quiver := {hom := λ (X Y : C), X ≅ Y}, id := λ (X : category_theory.core C), category_theory.iso.refl X, comp := λ (X Y Z : category_theory.core C) (f : X ⟶ Y) (g : Y ⟶ Z), f ≪≫ g}, id_comp' := _, comp_id' := _, assoc' := _}, inv := λ (X Y : category_theory.core C) (f : X ⟶ Y), category_theory.iso.symm f, inv_comp' := _, comp_inv' := _}

source

@[simp]

theorem category_theory.core.id_hom {C : Type u₁} [category_theory.category C] (X : category_theory.core C) :

(𝟙 X).hom = 𝟙 X

source

@[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

source

def category_theory.core.inclusion (C : Type u₁) [category_theory.category C] :

category_theory.core C ⥤ C

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

Equations

category_theory.core.inclusion C = {obj := id (category_theory.core C), map := λ (X Y : category_theory.core C) (f : X ⟶ Y), f.hom, map_id' := _, map_comp' := _}

Instances for category_theory.core.inclusion

category_theory.core.inclusion.category_theory.faithful

source

@[protected, instance]

def category_theory.core.inclusion.category_theory.faithful (C : Type u₁) [category_theory.category C] :

category_theory.faithful (category_theory.core.inclusion C)

source

noncomputable def category_theory.core.functor_to_core {C : Type u₁} [category_theory.category C] {G : Type u₂} [category_theory.groupoid G] (F : G ⥤ C) :

G ⥤ category_theory.core C

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

Equations

category_theory.core.functor_to_core F = {obj := λ (X : G), F.obj X, map := λ (X Y : G) (f : X ⟶ Y), {hom := F.map f, inv := F.map (category_theory.inv f), hom_inv_id' := _, inv_hom_id' := _}, map_id' := _, map_comp' := _}

source

def category_theory.core.forget_functor_to_core {C : Type u₁} [category_theory.category C] {G : Type u₂} [category_theory.groupoid G] :

(G ⥤ category_theory.core C) ⥤ 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

category_theory.core.forget_functor_to_core = (category_theory.whiskering_right G (category_theory.core C) C).obj (category_theory.core.inclusion C)

source

def category_theory.of_equiv_functor (m : Type u₁ → Type u₂) [equiv_functor m] :

category_theory.core (Type u₁) ⥤ category_theory.core (Type u₂)

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

Equations

category_theory.of_equiv_functor m = {obj := m, map := λ (α β : category_theory.core (Type u₁)) (f : α ⟶ β), (equiv_functor.map_equiv m (category_theory.iso.to_equiv f)).to_iso, map_id' := _, map_comp' := _}