mathlib documentation

category_theory.elements

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

References #

Tags #

category of elements, Grothendieck construction, comma category

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

Equations
@[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.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) (w : f.val = g.val) :
f = g
@[simp]
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
@[simp]
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.

Equations
@[simp]
@[simp]
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) :
@[simp]
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₂) :
@[simp]
theorem category_theory.category_of_elements.map_obj_fst {C : Type u} [category_theory.category C] {F₁ F₂ : C Type w} (α : F₁ F₂) (t : F₁.elements) :
def category_theory.category_of_elements.map {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.

Equations

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

Equations