The category of elements
This file defines the category of elements, also known as (a special case of) the Grothendieck construction.
Given a functor F : C ⥤ Type, an object of F.elements is a pair (X : C, x : F.obj X).
A morphism (X, x) ⟶ (Y, y) is a morphism f : X ⟶ Y in C, so F.map f takes x to y.
Implementation notes
This construction is equivalent to a special case of a comma construction, so this is mostly just
a more convenient API. We prove the equivalence in category_theory.category_of_elements.comma_equivalence.
References
- [Emily Riehl, Category Theory in Context, Section 2.4][riehl2017]
- https://en.wikipedia.org/wiki/Category_of_elements
- https://ncatlab.org/nlab/show/category+of+elements
Tags
category of elements, Grothendieck construction, comma category
@[nolint]
def
category_theory.functor.elements
{C : Type u}
[category_theory.category C] :
C ⥤ Type w → Type (max u w)
The type of objects for the category of elements of a functor F : C ⥤ Type
is a pair (X : C, x : F.obj X).
@[instance]
def
category_theory.category_of_elements
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w) :
The category structure on F.elements, for F : C ⥤ Type.
A morphism (X, x) ⟶ (Y, y) is a morphism f : X ⟶ Y in C, so F.map f takes x to y.
Equations
@[ext]
theorem
category_theory.category_of_elements.ext
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
{x y : F.elements}
(f g : x ⟶ y) :
@[simp]
theorem
category_theory.category_of_elements.id_val
{C : Type u}
[category_theory.category C]
{F : C ⥤ Type w}
{p : F.elements} :
@[instance]
def
category_theory.groupoid_of_elements
{G : Type u}
[category_theory.groupoid G]
(F : G ⥤ Type w) :
Equations
- category_theory.groupoid_of_elements F = {to_category := {to_category_struct := category_theory.category.to_category_struct (category_theory.category_of_elements F), id_comp' := _, comp_id' := _, assoc' := _}, inv := λ (p q : F.elements) (f : p ⟶ q), ⟨category_theory.is_iso.inv f.val (category_theory.is_iso.of_groupoid f.val), _⟩, inv_comp' := _, comp_inv' := _}
@[simp]
theorem
category_theory.category_of_elements.π_obj
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : F.elements) :
def
category_theory.category_of_elements.π
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w) :
The functor out of the category of elements which forgets the element.
@[simp]
theorem
category_theory.category_of_elements.π_map
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X Y : F.elements)
(f : X ⟶ Y) :
def
category_theory.category_of_elements.to_comma
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w) :
The forward direction of the equivalence F.elements ≅ (*, F).
Equations
- category_theory.category_of_elements.to_comma F = {obj := λ (X : F.elements), {left := punit.star, right := X.fst, hom := λ (_x : (category_theory.functor.from_punit punit).obj punit.star), X.snd}, map := λ (X Y : F.elements) (f : X ⟶ Y), {left := subtype.cases_on f (λ (f_val : X.fst ⟶ Y.fst) (f_property : F.map f_val X.snd = Y.snd), sigma.cases_on Y (λ (Y_fst : C) (Y_snd : F.obj Y_fst) (f_val : X.fst ⟶ ⟨Y_fst, Y_snd⟩.fst) (f_property : F.map f_val X.snd = ⟨Y_fst, Y_snd⟩.snd), sigma.cases_on X (λ (X_fst : C) (X_snd : F.obj X_fst) (f_val : ⟨X_fst, X_snd⟩.fst ⟶ ⟨Y_fst, Y_snd⟩.fst) (f_property : F.map f_val ⟨X_fst, X_snd⟩.snd = ⟨Y_fst, Y_snd⟩.snd), id (λ (F : C ⥤ Type w) (Y_fst : C) (Y_snd : F.obj Y_fst) (X_fst : C) (X_snd : F.obj X_fst) (f_val : X_fst ⟶ Y_fst) (f_property : F.map f_val X_snd = Y_snd), eq.drec {down := category_theory.category_of_elements.to_comma._proof_1.mpr {down := _}} f_property) F Y_fst Y_snd X_fst X_snd f_val f_property) f_val f_property) f_val f_property), right := f.val, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.category_of_elements.to_comma_obj
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : F.elements) :
(category_theory.category_of_elements.to_comma F).obj X = {left := punit.star, right := X.fst, hom := λ (_x : (category_theory.functor.from_punit punit).obj punit.star), X.snd}
@[simp]
theorem
category_theory.category_of_elements.to_comma_map
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
{X Y : F.elements}
(f : X ⟶ Y) :
(category_theory.category_of_elements.to_comma F).map f = {left := subtype.cases_on f (λ (f_val : X.fst ⟶ Y.fst) (f_property : F.map f_val X.snd = Y.snd), sigma.cases_on Y (λ (Y_fst : C) (Y_snd : F.obj Y_fst) (f_val : X.fst ⟶ ⟨Y_fst, Y_snd⟩.fst) (f_property : F.map f_val X.snd = ⟨Y_fst, Y_snd⟩.snd), sigma.cases_on X (λ (X_fst : C) (X_snd : F.obj X_fst) (f_val : ⟨X_fst, X_snd⟩.fst ⟶ ⟨Y_fst, Y_snd⟩.fst) (f_property : F.map f_val ⟨X_fst, X_snd⟩.snd = ⟨Y_fst, Y_snd⟩.snd), id (λ (F : C ⥤ Type w) (Y_fst : C) (Y_snd : F.obj Y_fst) (X_fst : C) (X_snd : F.obj X_fst) (f_val : X_fst ⟶ Y_fst) (f_property : F.map f_val X_snd = Y_snd), eq.drec {down := _.mpr {down := _}} f_property) F Y_fst Y_snd X_fst X_snd f_val f_property) f_val f_property) f_val f_property), right := f.val, w' := _}
def
category_theory.category_of_elements.from_comma
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w) :
The reverse direction of the equivalence F.elements ≅ (*, F).
Equations
- category_theory.category_of_elements.from_comma F = {obj := λ (X : category_theory.comma (category_theory.functor.from_punit punit) F), ⟨X.right, X.hom punit.star⟩, map := λ (X Y : category_theory.comma (category_theory.functor.from_punit punit) F) (f : X ⟶ Y), ⟨f.right, _⟩, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.category_of_elements.from_comma_obj
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : category_theory.comma (category_theory.functor.from_punit punit) F) :
@[simp]
theorem
category_theory.category_of_elements.from_comma_map
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
{X Y : category_theory.comma (category_theory.functor.from_punit punit) F}
(f : X ⟶ Y) :
(category_theory.category_of_elements.from_comma F).map f = ⟨f.right, _⟩
def
category_theory.category_of_elements.comma_equivalence
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w) :
The equivalence between the category of elements F.elements
and the comma category (*, F).
Equations
- category_theory.category_of_elements.comma_equivalence F = category_theory.equivalence.mk (category_theory.category_of_elements.to_comma F) (category_theory.category_of_elements.from_comma F) (category_theory.nat_iso.of_components (λ (X : F.elements), category_theory.eq_to_iso _) _) (category_theory.nat_iso.of_components (λ (X : category_theory.comma (category_theory.functor.from_punit punit) F), {hom := {left := id (λ (F : C ⥤ Type w) (X : category_theory.comma (category_theory.functor.from_punit punit) F), {down := _.mpr {down := _}}) F X, right := 𝟙 ((category_theory.category_of_elements.from_comma F ⋙ category_theory.category_of_elements.to_comma F).obj X).right, w' := _}, inv := {left := id (λ (F : C ⥤ Type w) (X : category_theory.comma (category_theory.functor.from_punit punit) F), {down := _.mpr {down := _}}) F X, right := 𝟙 ((𝟭 (category_theory.comma (category_theory.functor.from_punit punit) F)).obj X).right, w' := _}, hom_inv_id' := _, inv_hom_id' := _}) _)
@[simp]
theorem
category_theory.category_of_elements.comma_equivalence_functor
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w) :
@[simp]
theorem
category_theory.category_of_elements.comma_equivalence_inverse
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w) :