mathlib documentation


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 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.



category of elements, Grothendieck construction, comma category

def category_theory.functor.elements {C : Type u} [category_theory.category C] :
C Type wType (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).


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 takes x to y.

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) :
f.val = g.valf = g

theorem category_theory.category_of_elements.comp_val {C : Type u} [category_theory.category C] {F : C Type w} {p q r : F.elements} {f : p q} {g : q r} :
(f g).val = f.val g.val

theorem category_theory.category_of_elements.id_val {C : Type u} [category_theory.category C] {F : C Type w} {p : F.elements} :
(𝟙 p).val = 𝟙 p.fst

The functor out of the category of elements which forgets the element.


The forward direction of the equivalence F.elements ≅ (*, F).

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_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_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_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_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' := _}