# 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 CategoryTheory.CategoryOfElements.structuredArrowEquivalence.

## Tags #

category of elements, Grothendieck construction, comma category

def CategoryTheory.Functor.Elements {C : Type u} (F : ) :
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
• F.Elements = ((c : C) × F.obj c)
Instances For
theorem CategoryTheory.Functor.Elements.ext {C : Type u} {F : } (x : F.Elements) (y : F.Elements) (h₁ : x.fst = y.fst) (h₂ : F.map x.snd = y.snd) :
x = y

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
theorem CategoryTheory.CategoryOfElements.ext {C : Type u} (F : ) {x : F.Elements} {y : F.Elements} (f : x y) (g : x y) (w : f = g) :
f = g
@[simp]
theorem CategoryTheory.CategoryOfElements.comp_val {C : Type u} {F : } {p : F.Elements} {q : F.Elements} {r : F.Elements} {f : p q} {g : q r} :
@[simp]
theorem CategoryTheory.CategoryOfElements.id_val {C : Type u} {F : } {p : F.Elements} :
@[simp]
theorem CategoryTheory.CategoryOfElements.map_snd {C : Type u} {F : } {p : F.Elements} {q : F.Elements} (f : p q) :
F.map (f) p.snd = q.snd
Equations
@[simp]
theorem CategoryTheory.CategoryOfElements.π_obj {C : Type u} (F : ) (X : F.Elements) :
X = X.fst
@[simp]
theorem CategoryTheory.CategoryOfElements.π_map {C : Type u} (F : ) :
∀ {X Y : F.Elements} (f : X Y), f = f

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

Equations
• = { obj := fun (X : F.Elements) => X.fst, map := fun {X Y : F.Elements} (f : X Y) => f, map_id := , map_comp := }
Instances For
Equations
• =
instance CategoryTheory.CategoryOfElements.instReflectsIsomorphismsElementsπ {C : Type u} (F : ) :
.ReflectsIsomorphisms
Equations
• =
@[simp]
theorem CategoryTheory.CategoryOfElements.map_obj_fst {C : Type u} {F₁ : } {F₂ : } (α : F₁ F₂) (t : F₁.Elements) :
().fst = t.fst
@[simp]
theorem CategoryTheory.CategoryOfElements.map_map_coe {C : Type u} {F₁ : } {F₂ : } (α : F₁ F₂) {t₁ : F₁.Elements} {t₂ : F₁.Elements} (k : t₁ t₂) :
() = k
@[simp]
theorem CategoryTheory.CategoryOfElements.map_obj_snd {C : Type u} {F₁ : } {F₂ : } (α : F₁ F₂) (t : F₁.Elements) :
().snd = α.app t.fst t.snd
def CategoryTheory.CategoryOfElements.map {C : Type u} {F₁ : } {F₂ : } (α : F₁ F₂) :
CategoryTheory.Functor F₁.Elements F₂.Elements

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

Equations
• = { obj := fun (t : F₁.Elements) => t.fst, α.app t.fst t.snd, map := fun {t₁ t₂ : F₁.Elements} (k : t₁ t₂) => k, , map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.CategoryOfElements.map_π {C : Type u} {F₁ : } {F₂ : } (α : F₁ F₂) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.CategoryOfElements.toStructuredArrow_obj {C : Type u} (F : ) (X : F.Elements) :
= { left := { as := PUnit.unit }, right := X.fst, hom := fun (x : .obj { as := PUnit.unit }) => X.snd }
@[simp]
theorem CategoryTheory.CategoryOfElements.to_comma_map_right {C : Type u} (F : ) {X : F.Elements} {Y : F.Elements} (f : X Y) :
.right = f

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.CategoryOfElements.fromStructuredArrow_obj {C : Type u} (F : ) (X : ) :
= X.right, X.hom PUnit.unit
@[simp]
theorem CategoryTheory.CategoryOfElements.fromStructuredArrow_map {C : Type u} (F : ) {X : } {Y : } (f : X Y) :
= f.right,
@[simp]
theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_inverse_obj {C : Type u} (F : ) (X : ) :
.obj X = X.right, X.hom PUnit.unit
@[simp]
theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_counitIso_hom {C : Type u} (F : ) :
.hom = { app := fun (X : ) => ().hom, naturality := }
@[simp]
theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_functor_map {C : Type u} (F : ) {X : F.Elements} {Y : F.Elements} (f : X Y) :
@[simp]
theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_counitIso_inv {C : Type u} (F : ) :
.inv = { app := fun (X : ) => ().inv, naturality := }
@[simp]
theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_inverse_map {C : Type u} (F : ) :
∀ {X Y : } (f : X Y), .map f = f.right,

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.CategoryOfElements.toCostructuredArrow_obj {C : Type u} (F : ) (X : F.Elementsᵒᵖ) :
= CategoryTheory.CostructuredArrow.mk (CategoryTheory.yonedaEquiv.symm X.unop.snd)
@[simp]
theorem CategoryTheory.CategoryOfElements.toCostructuredArrow_map {C : Type u} (F : ) :
∀ {X Y : F.Elementsᵒᵖ} (f : X Y), = CategoryTheory.CostructuredArrow.homMk (f.unop).unop

The forward direction of the equivalence F.Elementsᵒᵖ ≅ (yoneda, F), given by CategoryTheory.yonedaEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.CategoryOfElements.fromCostructuredArrow_map_coe {C : Type u} (F : ) {X : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ} {Y : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ} (f : X Y) :
= f.unop.left.op
@[simp]
theorem CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_fst {C : Type u} (F : ) (X : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ) :
.fst = { unop := X.unop.left }
@[simp]
theorem CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_snd {C : Type u} (F : ) (X : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ) :
.snd = CategoryTheory.yonedaEquiv.toFun X.unop.hom

The reverse direction of the equivalence F.Elementsᵒᵖ ≅ (yoneda, F), given by CategoryTheory.yonedaEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_mk {C : Type u} (F : ) {X : C} (f : CategoryTheory.yoneda.obj X F) :
= { unop := X }, CategoryTheory.yonedaEquiv.toFun f

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]
theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_inverse_map {C : Type u} (F : ) :
∀ {X Y : CategoryTheory.CostructuredArrow CategoryTheory.yoneda F} (f : X Y), f = ().op
@[simp]
theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_inverse_obj {C : Type u} (F : ) (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda F) :
X = { unop := { unop := X } }
@[simp]
theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_functor_obj {C : Type u} (F : ) (X : F.Elementsᵒᵖ) :
X = CategoryTheory.CostructuredArrow.mk (CategoryTheory.yonedaEquiv.symm X.unop.snd)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

The equivalence F.elementsᵒᵖ ≌ (yoneda, F) is compatible with the forgetful functors.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The equivalence F.elementsᵒᵖ ≌ (yoneda, F) is compatible with the forgetful functors.

Equations
• One or more equations did not get rendered due to their size.
Instances For