@[nolint]
The core of a category C is the groupoid whose morphisms are all the isomorphisms of C.
Equations
@[instance]
Equations
- category_theory.core_category = {to_category := {to_category_struct := {to_has_hom := {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' := _}
@[simp]
theorem
category_theory.core.id_hom
{C : Type u₁}
[category_theory.category C]
(X : category_theory.core C) :
@[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) :
The core of a category is naturally included in the category.
Equations
- category_theory.core.inclusion = {obj := id (category_theory.core C), map := λ (X Y : category_theory.core C) (f : X ⟶ Y), f.hom, map_id' := _, map_comp' := _}
def
category_theory.core.functor_to_core
{C : Type u₁}
[category_theory.category C]
{G : Type u₂}
[category_theory.groupoid G] :
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.is_iso.inv f), hom_inv_id' := _, inv_hom_id' := _}, map_id' := _, map_comp' := _}
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.
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' := _}