-
Notifications
You must be signed in to change notification settings - Fork 298
/
core.lean
88 lines (70 loc) · 2.9 KB
/
core.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
/-
Copyright (c) 2019 Scott Morrison All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import category_theory.groupoid
import control.equiv_functor
import category_theory.types
/-!
# 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`.
-/
namespace category_theory
universes v₁ v₂ u₁ u₂ -- morphism levels before object levels. See note [category_theory universes].
/-- The core of a category C is the groupoid whose morphisms are all the
isomorphisms of C. -/
@[nolint has_inhabited_instance]
def core (C : Type u₁) := C
variables {C : Type u₁} [category.{v₁} C]
instance core_category : groupoid.{v₁} (core C) :=
{ hom := λ X Y : C, X ≅ Y,
inv := λ X Y f, iso.symm f,
id := λ X, iso.refl X,
comp := λ X Y Z f g, iso.trans f g }
namespace core
@[simp] lemma id_hom (X : core C) : iso.hom (𝟙 X) = 𝟙 X := rfl
@[simp] lemma comp_hom {X Y Z : core C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).hom = f.hom ≫ g.hom :=
rfl
variables (C)
/-- The core of a category is naturally included in the category. -/
def inclusion : core C ⥤ C :=
{ obj := id,
map := λ X Y f, f.hom }
instance : faithful (inclusion C) := {}
variables {C} {G : Type u₂} [groupoid.{v₂} G]
/-- A functor from a groupoid to a category C factors through the core of C. -/
-- Note that this function is not functorial
-- (consider the two functors from [0] to [1], and the natural transformation between them).
noncomputable
def functor_to_core (F : G ⥤ C) : G ⥤ core C :=
{ obj := λ X, F.obj X,
map := λ X Y f, ⟨F.map f, F.map (inv f)⟩ }
/--
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 forget_functor_to_core : (G ⥤ core C) ⥤ (G ⥤ C) := (whiskering_right _ _ _).obj (inclusion C)
end core
/--
`of_equiv_functor m` lifts a type-level `equiv_functor`
to a categorical functor `core (Type u₁) ⥤ core (Type u₂)`.
-/
def of_equiv_functor (m : Type u₁ → Type u₂) [equiv_functor m] :
core (Type u₁) ⥤ core (Type u₂) :=
{ obj := m,
map := λ α β f, (equiv_functor.map_equiv m f.to_equiv).to_iso,
-- These are not very pretty.
map_id' := λ α, begin ext, exact (congr_fun (equiv_functor.map_refl _) x), end,
map_comp' := λ α β γ f g,
begin
ext,
simp only [equiv_functor.map_equiv_apply, equiv.to_iso_hom,
function.comp_app, core.comp_hom, types_comp],
erw [iso.to_equiv_comp, equiv_functor.map_trans],
end, }
end category_theory