# mathlib3documentation

category_theory.elements

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

## Tags #

category of elements, Grothendieck construction, comma category

@[nolint]
def category_theory.functor.elements {C : Type u} (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
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.map f takes x to y.

Equations
@[ext]
theorem category_theory.category_of_elements.ext {C : Type u} (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} {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} {F : C Type w} {p : F.elements} :
(𝟙 p).val = 𝟙 p.fst
@[protected, instance]
noncomputable def category_theory.groupoid_of_elements {G : Type u} (F : G Type w) :
Equations

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

Equations
@[simp]
theorem category_theory.category_of_elements.π_map {C : Type u} (F : C Type w) (X Y : F.elements) (f : X Y) :
@[simp]
theorem category_theory.category_of_elements.π_obj {C : Type u} (F : C Type w) (X : F.elements) :
@[simp]
theorem category_theory.category_of_elements.map_obj_snd {C : Type u} {F₁ F₂ : C Type w} (α : F₁ F₂) (t : F₁.elements) :
= α.app t.fst t.snd
@[simp]
theorem category_theory.category_of_elements.map_map_coe {C : Type u} {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} {F₁ F₂ : C Type w} (α : F₁ F₂) (t : F₁.elements) :
def category_theory.category_of_elements.map {C : Type u} {F₁ F₂ : C Type w} (α : F₁ F₂) :

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

Equations
@[simp]
theorem category_theory.category_of_elements.map_π {C : Type u} {F₁ F₂ : C Type w} (α : F₁ F₂) :

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

Equations
@[simp]
theorem category_theory.category_of_elements.to_structured_arrow_obj {C : Type u} (F : C Type w) (X : F.elements) :
= {left := {as := punit.star}, right := X.fst, hom := λ (_x : {as := punit.star}), X.snd}
@[simp]
theorem category_theory.category_of_elements.to_comma_map_right {C : Type u} (F : C Type w) {X Y : F.elements} (f : X Y) :

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

Equations
@[simp]
theorem category_theory.category_of_elements.from_structured_arrow_obj {C : Type u} (F : C Type w)  :
= X.right, X.hom punit.star

The equivalence between the category of elements F.elements and the comma category (*, F).

Equations
@[simp]
theorem category_theory.category_of_elements.structured_arrow_equivalence_counit_iso_hom_app_left {C : Type u} (F : C Type w)  :
= category_theory.eq_to_hom category_theory.structured_arrow.iso_mk._proof_1
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]

The forward direction of the equivalence F.elementsᵒᵖ ≅ (yoneda, F), given by category_theory.yoneda_sections.

Equations
@[simp]
@[simp]

The reverse direction of the equivalence F.elementsᵒᵖ ≅ (yoneda, F), given by category_theory.yoneda_equiv.

Equations

The unit of the equivalence F.elementsᵒᵖ ≅ (yoneda, F) is indeed iso.

The counit of the equivalence F.elementsᵒᵖ ≅ (yoneda, F) is indeed iso.

@[simp]
@[simp]
@[simp]
@[simp]

The equivalence F.elementsᵒᵖ ≅ (yoneda, F) given by yoneda lemma.

Equations
@[simp]
@[simp]
@[simp]

The equivalence (-.elements)ᵒᵖ ≅ (yoneda, -) of is actually a natural isomorphism of functors.