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.
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
@[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).
Instances for category_theory.functor.elements
@[protected, instance]
def
category_theory.category_of_elements
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w) :
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
@[protected, instance]
noncomputable
def
category_theory.groupoid_of_elements
{G : Type u}
[category_theory.groupoid G]
(F : G ⥤ Type w) :
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' := _}
def
category_theory.category_of_elements.π
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w) :
The functor out of the category of elements which forgets the element.
@[simp]
theorem
category_theory.category_of_elements.π_map
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X Y : F.elements)
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.category_of_elements.π_obj
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : F.elements) :
@[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₂) :
↑((category_theory.category_of_elements.map α).map k) = k.val
@[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) :
((category_theory.category_of_elements.map α).obj t).fst = t.fst
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.
@[simp]
theorem
category_theory.category_of_elements.map_π
{C : Type u}
[category_theory.category C]
{F₁ F₂ : C ⥤ Type w}
(α : F₁ ⟶ F₂) :
def
category_theory.category_of_elements.to_structured_arrow
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w) :
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' := _}
@[simp]
theorem
category_theory.category_of_elements.to_structured_arrow_obj
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : F.elements) :
@[simp]
theorem
category_theory.category_of_elements.to_comma_map_right
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
{X Y : F.elements}
(f : X ⟶ Y) :
def
category_theory.category_of_elements.from_structured_arrow
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w) :
The reverse direction of the equivalence F.elements ≅ (*, F).
@[simp]
theorem
category_theory.category_of_elements.from_structured_arrow_obj
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : category_theory.structured_arrow punit F) :
@[simp]
theorem
category_theory.category_of_elements.from_structured_arrow_map
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
{X Y : category_theory.structured_arrow punit F}
(f : X ⟶ Y) :
def
category_theory.category_of_elements.structured_arrow_equivalence
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w) :
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), category_theory.structured_arrow.iso_mk (category_theory.iso.refl ((category_theory.category_of_elements.from_structured_arrow F ⋙ category_theory.category_of_elements.to_structured_arrow F).obj X).right) _) _)
@[simp]
theorem
category_theory.category_of_elements.structured_arrow_equivalence_counit_iso_hom_app_left
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : category_theory.structured_arrow punit F) :
((category_theory.category_of_elements.structured_arrow_equivalence F).counit_iso.hom.app X).left = category_theory.eq_to_hom category_theory.structured_arrow.iso_mk._proof_1
@[simp]
theorem
category_theory.category_of_elements.structured_arrow_equivalence_inverse_map_coe
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X Y : category_theory.structured_arrow punit F)
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.category_of_elements.structured_arrow_equivalence_counit_iso_hom_app_right
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : category_theory.structured_arrow punit F) :
@[simp]
theorem
category_theory.category_of_elements.structured_arrow_equivalence_unit_iso_inv_app_coe
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : F.elements) :
@[simp]
theorem
category_theory.category_of_elements.structured_arrow_equivalence_counit_iso_inv_app_left
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : category_theory.structured_arrow punit F) :
@[simp]
theorem
category_theory.category_of_elements.structured_arrow_equivalence_functor_map_right
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X Y : F.elements)
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.category_of_elements.structured_arrow_equivalence_functor_obj_hom
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : F.elements)
(_x : punit) :
@[simp]
theorem
category_theory.category_of_elements.structured_arrow_equivalence_functor_map_left_down_down
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X Y : F.elements)
(f : X ⟶ Y) :
_ = _
@[simp]
theorem
category_theory.category_of_elements.structured_arrow_equivalence_unit_iso_hom_app_coe
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : F.elements) :
@[simp]
theorem
category_theory.category_of_elements.structured_arrow_equivalence_inverse_obj_fst
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : category_theory.structured_arrow punit F) :
@[simp]
theorem
category_theory.category_of_elements.structured_arrow_equivalence_functor_obj_right
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : F.elements) :
@[simp]
theorem
category_theory.category_of_elements.structured_arrow_equivalence_counit_iso_inv_app_right
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : category_theory.structured_arrow punit F) :
@[simp]
theorem
category_theory.category_of_elements.structured_arrow_equivalence_inverse_obj_snd
{C : Type u}
[category_theory.category C]
(F : C ⥤ Type w)
(X : category_theory.structured_arrow punit F) :
def
category_theory.category_of_elements.to_costructured_arrow
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v) :
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' := _}
@[simp]
theorem
category_theory.category_of_elements.to_costructured_arrow_obj
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v)
(X : (F.elements)ᵒᵖ) :
@[simp]
theorem
category_theory.category_of_elements.to_costructured_arrow_map
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v)
(X Y : (F.elements)ᵒᵖ)
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.category_of_elements.from_costructured_arrow_obj_fst
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v)
(X : (category_theory.costructured_arrow category_theory.yoneda F)ᵒᵖ) :
@[simp]
theorem
category_theory.category_of_elements.from_costructured_arrow_obj_snd
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v)
(X : (category_theory.costructured_arrow category_theory.yoneda F)ᵒᵖ) :
@[simp]
theorem
category_theory.category_of_elements.from_costructured_arrow_map_coe
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v)
(X Y : (category_theory.costructured_arrow category_theory.yoneda F)ᵒᵖ)
(f : X ⟶ Y) :
def
category_theory.category_of_elements.from_costructured_arrow
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v) :
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), ⟨f.unop.left.op, _⟩, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.category_of_elements.from_costructured_arrow_obj_mk
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v)
{X : C}
(f : category_theory.yoneda.obj X ⟶ F) :
theorem
category_theory.category_of_elements.from_to_costructured_arrow_eq
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v) :
The unit of the equivalence F.elementsᵒᵖ ≅ (yoneda, F) is indeed iso.
theorem
category_theory.category_of_elements.to_from_costructured_arrow_eq
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v) :
The counit of the equivalence F.elementsᵒᵖ ≅ (yoneda, F) is indeed iso.
@[simp]
theorem
category_theory.category_of_elements.costructured_arrow_yoneda_equivalence_functor_obj_left
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v)
(X : (F.elements)ᵒᵖ) :
@[simp]
theorem
category_theory.category_of_elements.costructured_arrow_yoneda_equivalence_unit_iso_inv_app
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v)
(X : (F.elements)ᵒᵖ) :
(category_theory.category_of_elements.costructured_arrow_yoneda_equivalence F).unit_iso.inv.app X = ((category_theory.category_of_elements.from_costructured_arrow F).map (category_theory.costructured_arrow.hom_mk ↑(category_theory.eq_to_hom _).unop _).op).op ≫ ((category_theory.category_of_elements.from_costructured_arrow F).map (category_theory.eq_to_hom _)).op ≫ category_theory.eq_to_hom _
@[simp]
theorem
category_theory.category_of_elements.costructured_arrow_yoneda_equivalence_inverse_map
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v)
(X Y : category_theory.costructured_arrow category_theory.yoneda F)
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.category_of_elements.costructured_arrow_yoneda_equivalence_unit_iso_hom_app
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v)
(X : (F.elements)ᵒᵖ) :
(category_theory.category_of_elements.costructured_arrow_yoneda_equivalence F).unit_iso.hom.app X = category_theory.eq_to_hom _ ≫ ((category_theory.category_of_elements.from_costructured_arrow F).map (category_theory.eq_to_hom _)).op ≫ ((category_theory.category_of_elements.from_costructured_arrow F).map (category_theory.costructured_arrow.hom_mk ↑(category_theory.eq_to_hom _).unop _).op).op
@[simp]
theorem
category_theory.category_of_elements.costructured_arrow_yoneda_equivalence_functor_map_left
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v)
(X Y : (F.elements)ᵒᵖ)
(f : X ⟶ Y) :
def
category_theory.category_of_elements.costructured_arrow_yoneda_equivalence
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v) :
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 _)
@[simp]
theorem
category_theory.category_of_elements.costructured_arrow_yoneda_equivalence_inverse_obj
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v)
(X : category_theory.costructured_arrow category_theory.yoneda F) :
@[simp]
theorem
category_theory.category_of_elements.costructured_arrow_yoneda_equivalence_functor_obj_hom_app
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type v)
(X : (F.elements)ᵒᵖ)
(X_1 : Cᵒᵖ)
(a : (opposite.unop ((category_theory.yoneda.op.prod (𝟭 (Cᵒᵖ ⥤ Type v))).obj (opposite.op (opposite.unop (opposite.unop X).fst), F)).fst).obj X_1) :
((category_theory.category_of_elements.costructured_arrow_yoneda_equivalence F).functor.obj X).hom.app X_1 a = F.map (quiver.hom.op a) (opposite.unop X).snd
theorem
category_theory.category_of_elements.costructured_arrow_yoneda_equivalence_naturality
{C : Type u}
[category_theory.category C]
{F₁ F₂ : Cᵒᵖ ⥤ Type v}
(α : F₁ ⟶ F₂) :
The equivalence (-.elements)ᵒᵖ ≅ (yoneda, -) of is actually a natural isomorphism of functors.