mathlib3 documentation


The category of elements #

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

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

References #

Tags #

category of elements, Grothendieck construction, comma category


The type of objects for the category of elements of a functor F : C ⥤ Type is a pair (X : C, x : F.obj X).

Instances for category_theory.functor.elements
@[protected, instance]

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

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

theorem category_theory.category_of_elements.map_obj_snd {C : Type u} [category_theory.category C] {F₁ F₂ : C Type w} (α : F₁ F₂) (t : F₁.elements) :
theorem category_theory.category_of_elements.map_map_coe {C : Type u} [category_theory.category C] {F₁ F₂ : C Type w} (α : F₁ F₂) (t₁ t₂ : F₁.elements) (k : t₁ t₂) :
def {C : Type u} [category_theory.category C] {F₁ F₂ : C Type w} (α : F₁ F₂) :

A natural transformation between functors induces a functor between the categories of elements.


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