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 #
- Emily Riehl, Category Theory in Context, Section 2.4
- https://en.wikipedia.org/wiki/Category_of_elements
- https://ncatlab.org/nlab/show/category+of+elements
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
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
Equations
- category_theory.groupoid_of_elements F = {to_category := {to_category_struct := category_theory.category.to_category_struct (category_theory.category_of_elements F), id_comp' := _, comp_id' := _, assoc' := _}, inv := λ (p q : F.elements) (f : p ⟶ q), ⟨category_theory.inv f.val _, _⟩, inv_comp' := _, comp_inv' := _}
The functor out of the category of elements which forgets the element.
A natural transformation between functors induces a functor between the categories of elements.
The forward direction of the equivalence F.elements ≅ (*, F)
.
Equations
- category_theory.category_of_elements.to_structured_arrow F = {obj := λ (X : F.elements), category_theory.structured_arrow.mk (λ (_x : punit), X.snd), map := λ (X Y : F.elements) (f : X ⟶ Y), category_theory.structured_arrow.hom_mk f.val _, map_id' := _, map_comp' := _}
The reverse direction of the equivalence F.elements ≅ (*, F)
.
The equivalence between the category of elements F.elements
and the comma category (*, F)
.
Equations
- category_theory.category_of_elements.structured_arrow_equivalence F = category_theory.equivalence.mk (category_theory.category_of_elements.to_structured_arrow F) (category_theory.category_of_elements.from_structured_arrow F) (category_theory.nat_iso.of_components (λ (X : F.elements), category_theory.eq_to_iso _) _) (category_theory.nat_iso.of_components (λ (X : category_theory.structured_arrow punit F), {hom := {left := id (λ (F : C ⥤ Type w) (X : category_theory.structured_arrow punit F), {down := id (λ (F : C ⥤ Type w) (X : category_theory.structured_arrow punit F), _.mpr {down := _}) F X}) F X, right := 𝟙 ((category_theory.category_of_elements.from_structured_arrow F ⋙ category_theory.category_of_elements.to_structured_arrow F).obj X).right, w' := _}, inv := {left := id (λ (F : C ⥤ Type w) (X : category_theory.structured_arrow punit F), {down := id (λ (F : C ⥤ Type w) (X : category_theory.structured_arrow punit F), _.mpr {down := _}) F X}) F X, right := 𝟙 ((𝟭 (category_theory.structured_arrow punit F)).obj X).right, w' := _}, hom_inv_id' := _, inv_hom_id' := _}) _)
The forward direction of the equivalence F.elementsᵒᵖ ≅ (yoneda, F)
,
given by category_theory.yoneda_sections
.
Equations
- category_theory.category_of_elements.to_costructured_arrow F = {obj := λ (X : (F.elements)ᵒᵖ), category_theory.costructured_arrow.mk ((category_theory.yoneda_sections (opposite.unop (opposite.unop X).fst) F).inv {down := (opposite.unop X).snd}), map := λ (X Y : (F.elements)ᵒᵖ) (f : X ⟶ Y), category_theory.costructured_arrow.hom_mk f.unop.val.unop _, map_id' := _, map_comp' := _}
The reverse direction of the equivalence F.elementsᵒᵖ ≅ (yoneda, F)
,
given by category_theory.yoneda_equiv
.
Equations
- category_theory.category_of_elements.from_costructured_arrow F = {obj := λ (X : (category_theory.costructured_arrow category_theory.yoneda F)ᵒᵖ), ⟨opposite.op (opposite.unop X).left, category_theory.yoneda_equiv.to_fun (opposite.unop X).hom⟩, map := λ (X Y : (category_theory.costructured_arrow category_theory.yoneda F)ᵒᵖ) (f : X ⟶ Y), ⟨quiver.hom.op f.unop.left, _⟩, map_id' := _, map_comp' := _}
The unit of the equivalence F.elementsᵒᵖ ≅ (yoneda, F)
is indeed iso.
The counit of the equivalence F.elementsᵒᵖ ≅ (yoneda, F)
is indeed iso.
The equivalence F.elementsᵒᵖ ≅ (yoneda, F)
given by yoneda lemma.
Equations
- category_theory.category_of_elements.costructured_arrow_yoneda_equivalence F = category_theory.equivalence.mk (category_theory.category_of_elements.to_costructured_arrow F) (category_theory.category_of_elements.from_costructured_arrow F).right_op (category_theory.nat_iso.op (category_theory.eq_to_iso _)) (category_theory.eq_to_iso _)
The equivalence (-.elements)ᵒᵖ ≅ (yoneda, -)
of is actually a natural isomorphism of functors.