mathlib3 documentation

category_theory.grothendieck

The Grothendieck construction #

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

Given a functor F : C ⥤ Cat, the objects of grothendieck F consist of dependent pairs (b, f), where b : C and f : F.obj c, and a morphism (b, f) ⟶ (b', f') is a pair β : b ⟶ b' in C, and φ : (F.map β).obj f ⟶ f'

Categories such as PresheafedSpace are in fact examples of this construction, and it may be interesting to try to generalize some of the development there.

Implementation notes #

Really we should treat Cat as a 2-category, and allow F to be a 2-functor.

There is also a closely related construction starting with G : Cᵒᵖ ⥤ Cat, where morphisms consists again of β : b ⟶ b' and φ : f ⟶ (F.map (op β)).obj f'.

References #

See also category_theory.functor.elements for the category of elements of functor F : C ⥤ Type.

@[nolint]

structure category_theory.grothendieck {C : Type u_1} [category_theory.category C] (F : C ⥤ category_theory.Cat) :

Type (max u_1 u_6)

base : C
fiber : ↥(F.obj self.base)

The Grothendieck construction (often written as ∫ F in mathematics) for a functor F : C ⥤ Cat gives a category whose

objects X consist of X.base : C and X.fiber : F.obj base
morphisms f : X ⟶ Y consist of base : X.base ⟶ Y.base and f.fiber : (F.map base).obj X.fiber ⟶ Y.fiber

Instances for category_theory.grothendieck

category_theory.grothendieck.has_sizeof_inst
category_theory.grothendieck.category_theory.category

structure category_theory.grothendieck.hom {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} (X Y : category_theory.grothendieck F) :

Type (max u_3 u_5)

base : X.base ⟶ Y.base
fiber : (F.map self.base).obj X.fiber ⟶ Y.fiber

A morphism in the Grothendieck category F : C ⥤ Cat consists of base : X.base ⟶ Y.base and f.fiber : (F.map base).obj X.fiber ⟶ Y.fiber.

Instances for category_theory.grothendieck.hom

category_theory.grothendieck.hom.has_sizeof_inst
category_theory.grothendieck.hom.inhabited

@[ext]

theorem category_theory.grothendieck.ext {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} {X Y : category_theory.grothendieck F} (f g : X.hom Y) (w_base : f.base = g.base) (w_fiber : category_theory.eq_to_hom _ ≫ f.fiber = g.fiber) :

f = g

@[simp]

theorem category_theory.grothendieck.id_fiber {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} (X : category_theory.grothendieck F) :

X.id.fiber = category_theory.eq_to_hom _

def category_theory.grothendieck.id {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} (X : category_theory.grothendieck F) :

X.hom X

The identity morphism in the Grothendieck category.

Equations

X.id = {base := 𝟙 X.base, fiber := category_theory.eq_to_hom _}

@[simp]

theorem category_theory.grothendieck.id_base {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} (X : category_theory.grothendieck F) :

X.id.base = 𝟙 X.base

@[protected, instance]

def category_theory.grothendieck.hom.inhabited {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} (X : category_theory.grothendieck F) :

inhabited (X.hom X)

Equations

category_theory.grothendieck.hom.inhabited X = {default := X.id}

def category_theory.grothendieck.comp {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} {X Y Z : category_theory.grothendieck F} (f : X.hom Y) (g : Y.hom Z) :

X.hom Z

Composition of morphisms in the Grothendieck category.

Equations

category_theory.grothendieck.comp f g = {base := f.base ≫ g.base, fiber := category_theory.eq_to_hom _ ≫ (F.map g.base).map f.fiber ≫ g.fiber}

@[simp]

theorem category_theory.grothendieck.comp_base {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} {X Y Z : category_theory.grothendieck F} (f : X.hom Y) (g : Y.hom Z) :

(category_theory.grothendieck.comp f g).base = f.base ≫ g.base

@[simp]

theorem category_theory.grothendieck.comp_fiber {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} {X Y Z : category_theory.grothendieck F} (f : X.hom Y) (g : Y.hom Z) :

(category_theory.grothendieck.comp f g).fiber = category_theory.eq_to_hom _ ≫ (F.map g.base).map f.fiber ≫ g.fiber

@[protected, instance]

def category_theory.grothendieck.category_theory.category {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} :

category_theory.category (category_theory.grothendieck F)

Equations

category_theory.grothendieck.category_theory.category = {to_category_struct := {to_quiver := {hom := λ (X Y : category_theory.grothendieck F), X.hom Y}, id := λ (X : category_theory.grothendieck F), X.id, comp := λ (X Y Z : category_theory.grothendieck F) (f : X ⟶ Y) (g : Y ⟶ Z), category_theory.grothendieck.comp f g}, id_comp' := _, comp_id' := _, assoc' := _}

@[simp]

theorem category_theory.grothendieck.id_fiber' {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} (X : category_theory.grothendieck F) :

(𝟙 X).fiber = category_theory.eq_to_hom _

theorem category_theory.grothendieck.congr {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} {X Y : category_theory.grothendieck F} {f g : X ⟶ Y} (h : f = g) :

f.fiber = category_theory.eq_to_hom _ ≫ g.fiber

@[simp]

theorem category_theory.grothendieck.forget_map {C : Type u_1} [category_theory.category C] (F : C ⥤ category_theory.Cat) (X Y : category_theory.grothendieck F) (f : X ⟶ Y) :

(category_theory.grothendieck.forget F).map f = f.base

@[simp]

theorem category_theory.grothendieck.forget_obj {C : Type u_1} [category_theory.category C] (F : C ⥤ category_theory.Cat) (X : category_theory.grothendieck F) :

(category_theory.grothendieck.forget F).obj X = X.base

def category_theory.grothendieck.forget {C : Type u_1} [category_theory.category C] (F : C ⥤ category_theory.Cat) :

category_theory.grothendieck F ⥤ C

The forgetful functor from grothendieck F to the source category.

Equations

category_theory.grothendieck.forget F = {obj := λ (X : category_theory.grothendieck F), X.base, map := λ (X Y : category_theory.grothendieck F) (f : X ⟶ Y), f.base, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.grothendieck.grothendieck_Type_to_Cat_functor_obj_snd {C : Type u_1} [category_theory.category C] (G : C ⥤ Type w) (X : category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat)) :

((category_theory.grothendieck.grothendieck_Type_to_Cat_functor G).obj X).snd = X.fiber.as

@[simp]

theorem category_theory.grothendieck.grothendieck_Type_to_Cat_functor_map_coe {C : Type u_1} [category_theory.category C] (G : C ⥤ Type w) (X Y : category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat)) (f : X ⟶ Y) :

↑((category_theory.grothendieck.grothendieck_Type_to_Cat_functor G).map f) = f.base

@[simp]

theorem category_theory.grothendieck.grothendieck_Type_to_Cat_functor_obj_fst {C : Type u_1} [category_theory.category C] (G : C ⥤ Type w) (X : category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat)) :

((category_theory.grothendieck.grothendieck_Type_to_Cat_functor G).obj X).fst = X.base

def category_theory.grothendieck.grothendieck_Type_to_Cat_functor {C : Type u_1} [category_theory.category C] (G : C ⥤ Type w) :

category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat) ⥤ G.elements

Auxiliary definition for grothendieck_Type_to_Cat, to speed up elaboration.

Equations

category_theory.grothendieck.grothendieck_Type_to_Cat_functor G = {obj := λ (X : category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat)), ⟨X.base, X.fiber.as⟩, map := λ (X Y : category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat)) (f : X ⟶ Y), ⟨f.base, _⟩, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.grothendieck.grothendieck_Type_to_Cat_inverse_map_fiber_down_down {C : Type u_1} [category_theory.category C] (G : C ⥤ Type w) (X Y : G.elements) (f : X ⟶ Y) :

_ = _

@[simp]

theorem category_theory.grothendieck.grothendieck_Type_to_Cat_inverse_obj_fiber_as {C : Type u_1} [category_theory.category C] (G : C ⥤ Type w) (X : G.elements) :

((category_theory.grothendieck.grothendieck_Type_to_Cat_inverse G).obj X).fiber.as = X.snd

@[simp]

theorem category_theory.grothendieck.grothendieck_Type_to_Cat_inverse_obj_base {C : Type u_1} [category_theory.category C] (G : C ⥤ Type w) (X : G.elements) :

((category_theory.grothendieck.grothendieck_Type_to_Cat_inverse G).obj X).base = X.fst

def category_theory.grothendieck.grothendieck_Type_to_Cat_inverse {C : Type u_1} [category_theory.category C] (G : C ⥤ Type w) :

G.elements ⥤ category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat)

Auxiliary definition for grothendieck_Type_to_Cat, to speed up elaboration.

Equations

category_theory.grothendieck.grothendieck_Type_to_Cat_inverse G = {obj := λ (X : G.elements), {base := X.fst, fiber := {as := X.snd}}, map := λ (X Y : G.elements) (f : X ⟶ Y), {base := f.val, fiber := {down := {down := _}}}, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.grothendieck.grothendieck_Type_to_Cat_inverse_map_base {C : Type u_1} [category_theory.category C] (G : C ⥤ Type w) (X Y : G.elements) (f : X ⟶ Y) :

((category_theory.grothendieck.grothendieck_Type_to_Cat_inverse G).map f).base = f.val

def category_theory.grothendieck.grothendieck_Type_to_Cat {C : Type u_1} [category_theory.category C] (G : C ⥤ Type w) :

category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat) ≌ G.elements

The Grothendieck construction applied to a functor to Type (thought of as a functor to Cat by realising a type as a discrete category) is the same as the 'category of elements' construction.

Equations

category_theory.grothendieck.grothendieck_Type_to_Cat G = {functor := category_theory.grothendieck.grothendieck_Type_to_Cat_functor G, inverse := category_theory.grothendieck.grothendieck_Type_to_Cat_inverse G, unit_iso := category_theory.nat_iso.of_components (λ (X : category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat)), X.cases_on (λ (X_base : C) (X_fiber : ↥((G ⋙ category_theory.Type_to_Cat).obj X_base)), category_theory.discrete.cases_on X_fiber (λ (X_fiber : G.obj X_base), category_theory.iso.refl ((𝟭 (category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat))).obj {base := X_base, fiber := {as := X_fiber}})))) _, counit_iso := category_theory.nat_iso.of_components (λ (X : G.elements), sigma.cases_on X (λ (X_fst : C) (X_snd : G.obj X_fst), category_theory.iso.refl ((category_theory.grothendieck.grothendieck_Type_to_Cat_inverse G ⋙ category_theory.grothendieck.grothendieck_Type_to_Cat_functor G).obj ⟨X_fst, X_snd⟩))) _, functor_unit_iso_comp' := _}

@[simp]

theorem category_theory.grothendieck.grothendieck_Type_to_Cat_inverse_2 {C : Type u_1} [category_theory.category C] (G : C ⥤ Type w) :

(category_theory.grothendieck.grothendieck_Type_to_Cat G).inverse = category_theory.grothendieck.grothendieck_Type_to_Cat_inverse G

@[simp]

theorem category_theory.grothendieck.grothendieck_Type_to_Cat_functor_2 {C : Type u_1} [category_theory.category C] (G : C ⥤ Type w) :

(category_theory.grothendieck.grothendieck_Type_to_Cat G).functor = category_theory.grothendieck.grothendieck_Type_to_Cat_functor G

@[simp]

theorem category_theory.grothendieck.grothendieck_Type_to_Cat_counit_iso {C : Type u_1} [category_theory.category C] (G : C ⥤ Type w) :

(category_theory.grothendieck.grothendieck_Type_to_Cat G).counit_iso = category_theory.nat_iso.of_components (λ (X : G.elements), sigma.cases_on X (λ (X_fst : C) (X_snd : G.obj X_fst), category_theory.iso.refl ((category_theory.grothendieck.grothendieck_Type_to_Cat_inverse G ⋙ category_theory.grothendieck.grothendieck_Type_to_Cat_functor G).obj ⟨X_fst, X_snd⟩))) _

@[simp]

theorem category_theory.grothendieck.grothendieck_Type_to_Cat_unit_iso {C : Type u_1} [category_theory.category C] (G : C ⥤ Type w) :

(category_theory.grothendieck.grothendieck_Type_to_Cat G).unit_iso = category_theory.nat_iso.of_components (λ (X : category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat)), X.cases_on (λ (X_base : C) (X_fiber : ↥((G ⋙ category_theory.Type_to_Cat).obj X_base)), category_theory.discrete.cases_on X_fiber (λ (X_fiber : G.obj X_base), category_theory.iso.refl ((𝟭 (category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat))).obj {base := X_base, fiber := {as := X_fiber}})))) _