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.

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

def CategoryTheory.Functor.Elements {C : Type u} [Category.{v, u} C] (F : Functor 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

• F.Elements = ((c : C) × F.obj c)

@[reducible, inline]

abbrev CategoryTheory.Functor.elementsMk {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) (X : C) (x : F.obj X) : F.Elements

Constructor for the type F.Elements when F is a functor to types.

Equations

• F.elementsMk X x = ⟨X, x⟩

theorem CategoryTheory.Functor.Elements.ext {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (x y : F.Elements) (h₁ : x.fst = y.fst) (h₂ : F.map (eqToHom h₁) x.snd = y.snd) : x = y

instance CategoryTheory.categoryOfElements {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : Category.{v, max u w} F.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

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

def CategoryTheory.NatTrans.mapElements {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (φ : F ⟶ G) : Functor F.Elements G.Elements

Natural transformations are mapped to functors between category of elements

Equations

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

@[simp]

theorem CategoryTheory.NatTrans.mapElements_obj {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (φ : F ⟶ G) (x✝ : F.Elements) : (mapElements φ).obj x✝ = match x✝ with | ⟨X, x⟩ => ⟨X, φ.app X x⟩

@[simp]

theorem CategoryTheory.NatTrans.mapElements_map_coe {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (φ : F ⟶ G) {p q : F.Elements} (x✝ : p ⟶ q) : ↑((mapElements φ).map x✝) = ↑x✝

def CategoryTheory.Functor.elementsFunctor {C : Type u} [Category.{v, u} C] : Functor (Functor C (Type w)) Cat

The functor mapping functors C ⥤ Type w to their category of elements

Equations

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

@[simp]

theorem CategoryTheory.Functor.elementsFunctor_map {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Functor C (Type w)} (n : X✝ ⟶ Y✝) : elementsFunctor.map n = NatTrans.mapElements n

@[simp]

theorem CategoryTheory.Functor.elementsFunctor_obj {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : elementsFunctor.obj F = Cat.of F.Elements

def CategoryTheory.CategoryOfElements.homMk {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (x y : F.Elements) (f : x.fst ⟶ y.fst) (hf : F.map f x.snd = y.snd) : x ⟶ y

Constructor for morphisms in the category of elements of a functor to types.

Equations

• CategoryTheory.CategoryOfElements.homMk x y f hf = ⟨f, hf⟩

@[simp]

theorem CategoryTheory.CategoryOfElements.homMk_coe {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (x y : F.Elements) (f : x.fst ⟶ y.fst) (hf : F.map f x.snd = y.snd) : ↑(homMk x y f hf) = f

theorem CategoryTheory.CategoryOfElements.ext {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {x y : F.Elements} (f g : x ⟶ y) (w : ↑f = ↑g) : f = g

theorem CategoryTheory.CategoryOfElements.ext_iff {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} {x y : F.Elements} {f g : x ⟶ y} : f = g ↔ ↑f = ↑g

@[simp]

theorem CategoryTheory.CategoryOfElements.comp_val {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} {p q r : F.Elements} {f : p ⟶ q} {g : q ⟶ r} : ↑(CategoryStruct.comp f g) = CategoryStruct.comp ↑f ↑g

@[simp]

theorem CategoryTheory.CategoryOfElements.id_val {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} {p : F.Elements} : ↑(CategoryStruct.id p) = CategoryStruct.id p.fst

@[simp]

theorem CategoryTheory.CategoryOfElements.map_snd {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} {p q : F.Elements} (f : p ⟶ q) : F.map (↑f) p.snd = q.snd

def CategoryTheory.CategoryOfElements.isoMk {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (x y : F.Elements) (e : x.fst ≅ y.fst) (he : F.map e.hom x.snd = y.snd) : x ≅ y

Constructor for isomorphisms in the category of elements of a functor to types.

Equations

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

@[simp]

theorem CategoryTheory.CategoryOfElements.isoMk_hom {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (x y : F.Elements) (e : x.fst ≅ y.fst) (he : F.map e.hom x.snd = y.snd) : (isoMk x y e he).hom = homMk x y e.hom he

@[simp]

theorem CategoryTheory.CategoryOfElements.isoMk_inv {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (x y : F.Elements) (e : x.fst ≅ y.fst) (he : F.map e.hom x.snd = y.snd) : (isoMk x y e he).inv = homMk y x e.inv ⋯

instance CategoryTheory.groupoidOfElements {G : Type u} [Groupoid G] (F : Functor G (Type w)) : Groupoid F.Elements

Equations

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

def CategoryTheory.CategoryOfElements.π {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : Functor F.Elements C

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

Equations

• CategoryTheory.CategoryOfElements.π F = { obj := fun (X : F.Elements) => X.fst, map := fun {X Y : F.Elements} (f : X ⟶ Y) => ↑f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.CategoryOfElements.π_obj {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) (X : F.Elements) : (π F).obj X = X.fst

@[simp]

theorem CategoryTheory.CategoryOfElements.π_map {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {X✝ Y✝ : F.Elements} (f : X✝ ⟶ Y✝) : (π F).map f = ↑f

instance CategoryTheory.CategoryOfElements.instFaithfulElementsπ {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : (π F).Faithful

instance CategoryTheory.CategoryOfElements.instReflectsIsomorphismsElementsπ {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : (π F).ReflectsIsomorphisms

def CategoryTheory.CategoryOfElements.map {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} (α : F₁ ⟶ F₂) : Functor F₁.Elements F₂.Elements

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

Equations

• CategoryTheory.CategoryOfElements.map α = { 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 := ⋯ }

@[simp]

theorem CategoryTheory.CategoryOfElements.map_obj_fst {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} (α : F₁ ⟶ F₂) (t : F₁.Elements) : ((map α).obj t).fst = t.fst

@[simp]

theorem CategoryTheory.CategoryOfElements.map_map_coe {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} (α : F₁ ⟶ F₂) {t₁ t₂ : F₁.Elements} (k : t₁ ⟶ t₂) : ↑((map α).map k) = ↑k

@[simp]

theorem CategoryTheory.CategoryOfElements.map_obj_snd {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} (α : F₁ ⟶ F₂) (t : F₁.Elements) : ((map α).obj t).snd = α.app t.fst t.snd

@[simp]

theorem CategoryTheory.CategoryOfElements.map_π {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor C (Type w)} (α : F₁ ⟶ F₂) : (map α).comp (π F₂) = π F₁

def CategoryTheory.CategoryOfElements.toStructuredArrow {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : Functor F.Elements (StructuredArrow PUnit.{w + 1} F)

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

Equations

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

@[simp]

theorem CategoryTheory.CategoryOfElements.toStructuredArrow_obj {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) (X : F.Elements) : (toStructuredArrow F).obj X = { left := { as := PUnit.unit }, right := X.fst, hom := fun (x : (Functor.fromPUnit PUnit.{w + 1}).obj { as := PUnit.unit }) => X.snd }

@[simp]

theorem CategoryTheory.CategoryOfElements.to_comma_map_right {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {X Y : F.Elements} (f : X ⟶ Y) : ((toStructuredArrow F).map f).right = ↑f

def CategoryTheory.CategoryOfElements.fromStructuredArrow {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : Functor (StructuredArrow PUnit.{w + 1} F) F.Elements

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

Equations

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

@[simp]

theorem CategoryTheory.CategoryOfElements.fromStructuredArrow_obj {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) (X : StructuredArrow PUnit.{w + 1} F) : (fromStructuredArrow F).obj X = ⟨X.right, X.hom PUnit.unit⟩

@[simp]

theorem CategoryTheory.CategoryOfElements.fromStructuredArrow_map {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {X Y : StructuredArrow PUnit.{w + 1} F} (f : X ⟶ Y) : (fromStructuredArrow F).map f = ⟨f.right, ⋯⟩

def CategoryTheory.CategoryOfElements.structuredArrowEquivalence {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : F.Elements ≌ StructuredArrow PUnit.{w + 1} F

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.

@[simp]

theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_inverse {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : (structuredArrowEquivalence F).inverse = fromStructuredArrow F

@[simp]

theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_counitIso {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : (structuredArrowEquivalence F).counitIso = Iso.refl ((fromStructuredArrow F).comp (toStructuredArrow F))

@[simp]

theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_unitIso {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : (structuredArrowEquivalence F).unitIso = Iso.refl (Functor.id F.Elements)

@[simp]

theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_functor {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : (structuredArrowEquivalence F).functor = toStructuredArrow F

def CategoryTheory.CategoryOfElements.toCostructuredArrow {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) : Functor F.Elementsᵒᵖ (CostructuredArrow yoneda F)

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.

@[simp]

theorem CategoryTheory.CategoryOfElements.toCostructuredArrow_map {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) {X✝ Y✝ : F.Elementsᵒᵖ} (f : X✝ ⟶ Y✝) : (toCostructuredArrow F).map f = CostructuredArrow.homMk (↑f.unop).unop ⋯

@[simp]

theorem CategoryTheory.CategoryOfElements.toCostructuredArrow_obj {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) (X : F.Elementsᵒᵖ) : (toCostructuredArrow F).obj X = CostructuredArrow.mk (yonedaEquiv.symm (Opposite.unop X).snd)

def CategoryTheory.CategoryOfElements.fromCostructuredArrow {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) : Functor (CostructuredArrow yoneda F)ᵒᵖ F.Elements

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.

@[simp]

theorem CategoryTheory.CategoryOfElements.fromCostructuredArrow_map_coe {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) {X Y : (CostructuredArrow yoneda F)ᵒᵖ} (f : X ⟶ Y) : ↑((fromCostructuredArrow F).map f) = f.unop.left.op

@[simp]

theorem CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_fst {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) (X : (CostructuredArrow yoneda F)ᵒᵖ) : ((fromCostructuredArrow F).obj X).fst = Opposite.op (Opposite.unop X).left

@[simp]

theorem CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_snd {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) (X : (CostructuredArrow yoneda F)ᵒᵖ) : ((fromCostructuredArrow F).obj X).snd = yonedaEquiv.toFun (Opposite.unop X).hom

@[simp]

theorem CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_mk {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) {X : C} (f : yoneda.obj X ⟶ F) : (fromCostructuredArrow F).obj (Opposite.op (CostructuredArrow.mk f)) = ⟨Opposite.op X, yonedaEquiv.toFun f⟩

def CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) : F.Elementsᵒᵖ ≌ CostructuredArrow yoneda F

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

Equations

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

@[simp]

theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_unitIso {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) : (costructuredArrowYonedaEquivalence F).unitIso = NatIso.ofComponents (fun (X : F.Elementsᵒᵖ) => (isoMk ((fromCostructuredArrow F).obj (Opposite.op ((toCostructuredArrow F).obj X))) (Opposite.unop X) (Iso.refl ((fromCostructuredArrow F).obj (Opposite.op ((toCostructuredArrow F).obj X))).fst) ⋯).op) ⋯

@[simp]

theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_functor {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) : (costructuredArrowYonedaEquivalence F).functor = toCostructuredArrow F

@[simp]

theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_counitIso {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) : (costructuredArrowYonedaEquivalence F).counitIso = NatIso.ofComponents (fun (X : CostructuredArrow yoneda F) => CostructuredArrow.isoMk (Iso.refl (((fromCostructuredArrow F).rightOp.comp (toCostructuredArrow F)).obj X).left) ⋯) ⋯

@[simp]

theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_inverse {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) : (costructuredArrowYonedaEquivalence F).inverse = (fromCostructuredArrow F).rightOp

theorem CategoryTheory.CategoryOfElements.costructuredArrow_yoneda_equivalence_naturality {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type v)} (α : F₁ ⟶ F₂) : (map α).op.comp (toCostructuredArrow F₂) = (toCostructuredArrow F₁).comp (CostructuredArrow.map α)

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

def CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) : (costructuredArrowYonedaEquivalence F).functor.comp (CostructuredArrow.proj yoneda F) ≅ (π F).leftOp

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.

@[simp]

theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_inv_app {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) (X : F.Elementsᵒᵖ) : (costructuredArrowYonedaEquivalenceFunctorProj F).inv.app X = CategoryStruct.id (Opposite.unop (Opposite.unop X).1)

@[simp]

theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_hom_app {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) (X : F.Elementsᵒᵖ) : (costructuredArrowYonedaEquivalenceFunctorProj F).hom.app X = CategoryStruct.id (Opposite.unop (Opposite.unop X).1)

def CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) : (costructuredArrowYonedaEquivalence F).inverse.comp (π F).leftOp ≅ CostructuredArrow.proj yoneda F

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.

@[simp]

theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_hom_app {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) (X : CostructuredArrow yoneda F) : (costructuredArrowYonedaEquivalenceInverseπ F).hom.app X = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_inv_app {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) (X : CostructuredArrow yoneda F) : (costructuredArrowYonedaEquivalenceInverseπ F).inv.app X = CategoryStruct.id X.left

def CategoryTheory.Functor.Elements.initial {C : Type u} [Category.{v, u} C] (A : C) : (yoneda.obj A).Elements

The initial object in the category of elements for a representable functor. In isInitial it is shown that this is initial.

Equations

• CategoryTheory.Functor.Elements.initial A = ⟨Opposite.op A, CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op A))⟩

def CategoryTheory.Functor.Elements.isInitial {C : Type u} [Category.{v, u} C] (A : C) : Limits.IsInitial (initial A)

Show that Elements.initial A is initial in the category of elements for the yoneda functor.

Equations

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