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 such that 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.Functor.Elements.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

structure 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).

• obj : C

  the underlying object of an element of a functor to types

• val : F.obj self.obj

  the value of the element

@[deprecated CategoryTheory.Functor.Elements.obj (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.obj.

---

the underlying object of an element of a functor to types

Equations

• @CategoryTheory.Functor.Elements.fst = @CategoryTheory.Functor.Elements.obj

@[deprecated CategoryTheory.Functor.Elements.val (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.val.

---

the value of the element

Equations

• @CategoryTheory.Functor.Elements.snd = @CategoryTheory.Functor.Elements.val

@[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 = { obj := X, val := x }

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

structure CategoryTheory.Functor.Elements.Hom {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (x y : F.Elements) : Type v

A morphism x ⟶ y in the category F.Elements of elements of a functor F : C ⥤ Type w consists of a morphism hom : x.obj ⟶ y.obj such that F.map hom sends x.val to y.val.

• hom : x.obj ⟶ y.obj

  the underlying morphism of objects

• map_val : (ConcreteCategory.hom (F.map self.hom)) x.val = y.val

theorem CategoryTheory.Functor.Elements.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {F : Functor C (Type w)} {x y : F.Elements} {x✝ y✝ : x.Hom y} (hom : x✝.hom = y✝.hom) : x✝ = y✝

theorem CategoryTheory.Functor.Elements.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {F : Functor C (Type w)} {x y : F.Elements} {x✝ y✝ : x.Hom y} : x✝ = y✝ ↔ x✝.hom = y✝.hom

@[instance_reducible]

instance CategoryTheory.Functor.Elements.instCategory {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.

@[simp]

theorem CategoryTheory.Functor.Elements.id_hom {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (x : F.Elements) : (CategoryStruct.id x).hom = CategoryStruct.id x.obj

@[simp]

theorem CategoryTheory.Functor.Elements.comp_hom {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} {X✝ Y✝ Z✝ : F.Elements} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

@[implicit_reducible]

def CategoryTheory.Functor.Elements.π {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.Functor.Elements.π F = { obj := fun (X : F.Elements) => X.obj, map := fun {X Y : F.Elements} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }

@[simp]

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

@[simp]

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

@[implicit_reducible]

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 categories of elements.

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.NatTrans.mapElements_map_hom {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (φ : F ⟶ G) {e₁ e₂ : F.Elements} (f : e₁ ⟶ e₂) : ((mapElements φ).map f).hom = f.hom

@[simp]

theorem CategoryTheory.NatTrans.mapElements_obj_val {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (φ : F ⟶ G) (e : F.Elements) : ((mapElements φ).obj e).val = (ConcreteCategory.hom (φ.app e.obj)) e.val

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

If φ : F ⟶ G is a natural transformation between functors to types, this is the canonical isomorphism φ.mapElements ⋙ Functor.Elements.π G ≅ Functor.Elements.π F.

Equations

• CategoryTheory.NatTrans.mapElementsCompπIso φ = CategoryTheory.Iso.refl ((CategoryTheory.NatTrans.mapElements φ).comp (CategoryTheory.Functor.Elements.π G))

@[simp]

theorem CategoryTheory.NatTrans.mapElementsCompπIso_hom_app {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (φ : F ⟶ G) (X : F.Elements) : (mapElementsCompπIso φ).hom.app X = CategoryStruct.id X.obj

@[simp]

theorem CategoryTheory.NatTrans.mapElementsCompπIso_inv_app {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (φ : F ⟶ G) (X : F.Elements) : (mapElementsCompπIso φ).inv.app X = CategoryStruct.id X.obj

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

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).toCatHom

@[simp]

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

@[reducible, inline]

abbrev CategoryTheory.Functor.Elements.homMk {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} {x y : F.Elements} (f : x.obj ⟶ y.obj) (hf : (ConcreteCategory.hom (F.map f)) x.val = y.val := by cat_disch) : x ⟶ y

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

Equations

• CategoryTheory.Functor.Elements.homMk f hf = { hom := f, map_val := hf }

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

theorem CategoryTheory.Functor.Elements.hom_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.hom = g.hom

def CategoryTheory.Functor.Elements.isoMk {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} {x y : F.Elements} (e : x.obj ≅ y.obj) (he : (ConcreteCategory.hom (F.map e.hom)) x.val = y.val := by cat_disch) : x ≅ y

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

Equations

• CategoryTheory.Functor.Elements.isoMk e he = { hom := CategoryTheory.Functor.Elements.homMk e.hom he, inv := CategoryTheory.Functor.Elements.homMk e.inv ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

theorem CategoryTheory.Functor.Elements.isoMk_hom {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} {x y : F.Elements} (e : x.obj ≅ y.obj) (he : (ConcreteCategory.hom (F.map e.hom)) x.val = y.val := by cat_disch) : (isoMk e he).hom = homMk e.hom he

instance CategoryTheory.Functor.Elements.instLocallySmall {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} [LocallySmall.{w, v, u} C] : LocallySmall.{w, v, max u w} F.Elements

@[instance_reducible]

instance CategoryTheory.Functor.Elements.groupoid {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.

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

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

@[implicit_reducible]

def CategoryTheory.Functor.Elements.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.Functor.Elements.toStructuredArrow_obj {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) (e : F.Elements) : (toStructuredArrow F).obj e = StructuredArrow.mk (TypeCat.ofHom fun (x : PUnit.{w + 1}) => e.val)

@[simp]

theorem CategoryTheory.Functor.Elements.toStructuredArrow_map {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {X✝ Y✝ : F.Elements} (f : X✝ ⟶ Y✝) : (toStructuredArrow F).map f = StructuredArrow.homMk f.hom ⋯

@[implicit_reducible]

def CategoryTheory.Functor.Elements.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.Functor.Elements.fromStructuredArrow_obj {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) (X : StructuredArrow PUnit.{w + 1} F) : (fromStructuredArrow F).obj X = F.elementsMk X.right ((ConcreteCategory.hom X.hom) PUnit.unit)

@[simp]

theorem CategoryTheory.Functor.Elements.fromStructuredArrow_map_hom {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).hom = StructuredArrow.Hom.right f

theorem CategoryTheory.Functor.Elements.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 = { hom := StructuredArrow.Hom.right f, map_val := ⋯ }

@[implicit_reducible]

def CategoryTheory.Functor.Elements.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.Functor.Elements.structuredArrowEquivalence_functor {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : (structuredArrowEquivalence F).functor = toStructuredArrow F

@[simp]

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

@[simp]

theorem CategoryTheory.Functor.Elements.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.Functor.Elements.structuredArrowEquivalence_counitIso {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : (structuredArrowEquivalence F).counitIso = Iso.refl ((fromStructuredArrow F).comp (toStructuredArrow F))

@[implicit_reducible]

def CategoryTheory.Functor.Elements.toCostructuredArrow {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) : Functor F.Elementsᵒᵖ (CostructuredArrow CategoryTheory.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.Functor.Elements.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.hom.unop ⋯

@[simp]

theorem CategoryTheory.Functor.Elements.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).val)

@[implicit_reducible]

def CategoryTheory.Functor.Elements.fromCostructuredArrow {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) : Functor (CostructuredArrow CategoryTheory.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.Functor.Elements.fromCostructuredArrow_map {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) {X✝ Y✝ : (CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ} (f : X✝ ⟶ Y✝) : (fromCostructuredArrow F).map f = homMk f.unop.left.op ⋯

@[simp]

theorem CategoryTheory.Functor.Elements.fromCostructuredArrow_obj {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) (X : (CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ) : (fromCostructuredArrow F).obj X = F.elementsMk (Opposite.op (Opposite.unop X).left) (yonedaEquiv (Opposite.unop X).hom)

@[simp]

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

@[implicit_reducible]

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.Elements.costructuredArrowYonedaEquivalenceFunctorProj {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) : (costructuredArrowYonedaEquivalence F).functor.comp (CostructuredArrow.proj CategoryTheory.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.Functor.Elements.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)

@[simp]

theorem CategoryTheory.Functor.Elements.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)

def CategoryTheory.Functor.Elements.costructuredArrowYonedaEquivalenceInverseπ {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) : (costructuredArrowYonedaEquivalence F).inverse.comp (π F).leftOp ≅ CostructuredArrow.proj CategoryTheory.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.Functor.Elements.costructuredArrowYonedaEquivalenceInverseπ_inv_app {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type v)) (X : CostructuredArrow CategoryTheory.yoneda F) : (costructuredArrowYonedaEquivalenceInverseπ F).inv.app X = CategoryStruct.id X.left

@[simp]

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

@[implicit_reducible]

def CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalence {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type (max w v))) : F.Elementsᵒᵖ ≌ CostructuredArrow uliftYoneda.{w, v, u} F

The opposite of the category of elements of a presheaf of types is equivalent to a category of costructured arrows for the Yoneda embedding functor.

Equations

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

@[simp]

theorem CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalence_functor_map {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type (max w v))) {X✝ Y✝ : F.Elementsᵒᵖ} (f : X✝ ⟶ Y✝) : (costructuredArrowULiftYonedaEquivalence F).functor.map f = CostructuredArrow.homMk f.unop.hom.unop ⋯

@[simp]

theorem CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalence_inverse_map {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type (max w v))) {X✝ Y✝ : CostructuredArrow uliftYoneda.{w, v, u} F} (f : X✝ ⟶ Y✝) : (costructuredArrowULiftYonedaEquivalence F).inverse.map f = (homMk f.left.op ⋯).op

@[simp]

theorem CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalence_functor_obj {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type (max w v))) (x : F.Elementsᵒᵖ) : (costructuredArrowULiftYonedaEquivalence F).functor.obj x = CostructuredArrow.mk (uliftYonedaEquiv.symm (Opposite.unop x).val)

@[simp]

theorem CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalence_counitIso {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type (max w v))) : (costructuredArrowULiftYonedaEquivalence F).counitIso = NatIso.ofComponents (fun (x : CostructuredArrow uliftYoneda.{w, v, u} F) => CostructuredArrow.isoMk (Iso.refl (({ obj := fun (x : CostructuredArrow uliftYoneda.{w, v, u} F) => Opposite.op (F.elementsMk (Opposite.op x.left) (uliftYonedaEquiv x.hom)), map := fun {X Y : CostructuredArrow uliftYoneda.{w, v, u} F} (f : X ⟶ Y) => (homMk f.left.op ⋯).op, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (x : F.Elementsᵒᵖ) => CostructuredArrow.mk (uliftYonedaEquiv.symm (Opposite.unop x).val), map := fun {X Y : F.Elementsᵒᵖ} (f : X ⟶ Y) => CostructuredArrow.homMk f.unop.hom.unop ⋯, map_id := ⋯, map_comp := ⋯ }).obj x).left) ⋯) ⋯

@[simp]

theorem CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalence_inverse_obj {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type (max w v))) (x : CostructuredArrow uliftYoneda.{w, v, u} F) : (costructuredArrowULiftYonedaEquivalence F).inverse.obj x = Opposite.op (F.elementsMk (Opposite.op x.left) (uliftYonedaEquiv x.hom))

@[simp]

theorem CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalence_unitIso {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type (max w v))) : (costructuredArrowULiftYonedaEquivalence F).unitIso = NatIso.ofComponents (fun (x : F.Elementsᵒᵖ) => (isoMk (Iso.refl (F.elementsMk (Opposite.op ({ obj := fun (x : F.Elementsᵒᵖ) => CostructuredArrow.mk (uliftYonedaEquiv.symm (Opposite.unop x).val), map := fun {X Y : F.Elementsᵒᵖ} (f : X ⟶ Y) => CostructuredArrow.homMk f.unop.hom.unop ⋯, map_id := ⋯, map_comp := ⋯ }.obj x).left) (uliftYonedaEquiv ({ obj := fun (x : F.Elementsᵒᵖ) => CostructuredArrow.mk (uliftYonedaEquiv.symm (Opposite.unop x).val), map := fun {X Y : F.Elementsᵒᵖ} (f : X ⟶ Y) => CostructuredArrow.homMk f.unop.hom.unop ⋯, map_id := ⋯, map_comp := ⋯ }.obj x).hom)).obj) ⋯).op) ⋯

def CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalenceFunctorCompProjIso {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type (max w v))) : (costructuredArrowULiftYonedaEquivalence F).functor.comp (CostructuredArrow.proj uliftYoneda.{w, v, u} F) ≅ (π F).leftOp

The functor of the equivalence costructuredArrowULiftYonedaEquivalence F followed by the projection CostructuredArrow uliftYoneda.{w} F ⥤ C identifies to (π F).leftOp.

Equations

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

noncomputable def CategoryTheory.Functor.Elements.costructuredArrowShrinkYonedaEquivalence {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (F : Functor Cᵒᵖ (Type w)) : F.Elementsᵒᵖ ≌ CostructuredArrow shrinkYoneda.{w, v, u} F

Given F : Cᵒᵖ ⥤ Type w where C is a locally w-small category, this is the equivalence between the opposite of the category of elements of F and CostructuredArrow shrinkYoneda.{w} F.

Equations

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

@[simp]

theorem CategoryTheory.Functor.Elements.costructuredArrowShrinkYonedaEquivalence_functor_map {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (F : Functor Cᵒᵖ (Type w)) {X✝ Y✝ : F.Elementsᵒᵖ} (f : X✝ ⟶ Y✝) : (costructuredArrowShrinkYonedaEquivalence F).functor.map f = CostructuredArrow.homMk f.unop.hom.unop ⋯

@[simp]

theorem CategoryTheory.Functor.Elements.costructuredArrowShrinkYonedaEquivalence_inverse_obj {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (F : Functor Cᵒᵖ (Type w)) (x : CostructuredArrow shrinkYoneda.{w, v, u} F) : (costructuredArrowShrinkYonedaEquivalence F).inverse.obj x = Opposite.op (F.elementsMk (Opposite.op x.left) (shrinkYonedaEquiv x.hom))

@[simp]

theorem CategoryTheory.Functor.Elements.costructuredArrowShrinkYonedaEquivalence_unitIso {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (F : Functor Cᵒᵖ (Type w)) : (costructuredArrowShrinkYonedaEquivalence F).unitIso = NatIso.ofComponents (fun (x : F.Elementsᵒᵖ) => (isoMk (Iso.refl (F.elementsMk (Opposite.op ({ obj := fun (x : F.Elementsᵒᵖ) => CostructuredArrow.mk (shrinkYonedaEquiv.symm (Opposite.unop x).val), map := fun {X Y : F.Elementsᵒᵖ} (f : X ⟶ Y) => CostructuredArrow.homMk f.unop.hom.unop ⋯, map_id := ⋯, map_comp := ⋯ }.obj x).left) (shrinkYonedaEquiv ({ obj := fun (x : F.Elementsᵒᵖ) => CostructuredArrow.mk (shrinkYonedaEquiv.symm (Opposite.unop x).val), map := fun {X Y : F.Elementsᵒᵖ} (f : X ⟶ Y) => CostructuredArrow.homMk f.unop.hom.unop ⋯, map_id := ⋯, map_comp := ⋯ }.obj x).hom)).obj) ⋯).op) ⋯

@[simp]

theorem CategoryTheory.Functor.Elements.costructuredArrowShrinkYonedaEquivalence_counitIso {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (F : Functor Cᵒᵖ (Type w)) : (costructuredArrowShrinkYonedaEquivalence F).counitIso = NatIso.ofComponents (fun (x : CostructuredArrow shrinkYoneda.{w, v, u} F) => CostructuredArrow.isoMk (Iso.refl (({ obj := fun (x : CostructuredArrow shrinkYoneda.{w, v, u} F) => Opposite.op (F.elementsMk (Opposite.op x.left) (shrinkYonedaEquiv x.hom)), map := fun {X Y : CostructuredArrow shrinkYoneda.{w, v, u} F} (f : X ⟶ Y) => (homMk f.left.op ⋯).op, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (x : F.Elementsᵒᵖ) => CostructuredArrow.mk (shrinkYonedaEquiv.symm (Opposite.unop x).val), map := fun {X Y : F.Elementsᵒᵖ} (f : X ⟶ Y) => CostructuredArrow.homMk f.unop.hom.unop ⋯, map_id := ⋯, map_comp := ⋯ }).obj x).left) ⋯) ⋯

@[simp]

theorem CategoryTheory.Functor.Elements.costructuredArrowShrinkYonedaEquivalence_functor_obj {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (F : Functor Cᵒᵖ (Type w)) (x : F.Elementsᵒᵖ) : (costructuredArrowShrinkYonedaEquivalence F).functor.obj x = CostructuredArrow.mk (shrinkYonedaEquiv.symm (Opposite.unop x).val)

@[simp]

theorem CategoryTheory.Functor.Elements.costructuredArrowShrinkYonedaEquivalence_inverse_map {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (F : Functor Cᵒᵖ (Type w)) {X✝ Y✝ : CostructuredArrow shrinkYoneda.{w, v, u} F} (f : X✝ ⟶ Y✝) : (costructuredArrowShrinkYonedaEquivalence F).inverse.map f = (homMk f.left.op ⋯).op

noncomputable def CategoryTheory.Functor.Elements.costructuredArrowShrinkYonedaEquivalenceFunctorCompProjIso {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (F : Functor Cᵒᵖ (Type w)) : (costructuredArrowShrinkYonedaEquivalence F).functor.comp (CostructuredArrow.proj shrinkYoneda.{w, v, u} F) ≅ (π F).leftOp

The functor of the equivalence costructuredArrowShrinkYonedaEquivalence F followed by the projection CostructuredArrow shrinkYoneda.{w} F ⥤ C identifies to (π F).leftOp.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Functor.Elements.initialOfRepresentableBy {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type u_1)} {X : C} (h : F.RepresentableBy X) : F.Elements

The initial object in F.Elements if F is representable.

Equations

• CategoryTheory.Functor.Elements.initialOfRepresentableBy h = { obj := Opposite.op X, val := h.homEquiv (CategoryTheory.CategoryStruct.id X) }

def CategoryTheory.Functor.Elements.isInitialOfRepresentableBy {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type u_1)} {X : C} (h : F.RepresentableBy X) : Limits.IsInitial (initialOfRepresentableBy h)

If F is represented by X, X with its universal element is the initial object of F.Elements.

Equations

• CategoryTheory.Functor.Elements.isInitialOfRepresentableBy h = CategoryTheory.Limits.IsInitial.ofUniqueHom (fun (e : F.Elements) => { hom := (h.homEquiv.symm e.val).op, map_val := ⋯ }) ⋯

@[reducible, inline]

abbrev CategoryTheory.Functor.Elements.initialOfCorepresentableBy {C : Type u} [Category.{v, u} C] {F : Functor C (Type u_1)} {X : C} (h : F.CorepresentableBy X) : F.Elements

The initial object in F.Elements if F is corepresentable.

Equations

• CategoryTheory.Functor.Elements.initialOfCorepresentableBy h = { obj := X, val := h.homEquiv (CategoryTheory.CategoryStruct.id X) }

def CategoryTheory.Functor.Elements.isInitialOfCorepresentableBy {C : Type u} [Category.{v, u} C] {F : Functor C (Type u_1)} {X : C} (h : F.CorepresentableBy X) : Limits.IsInitial (initialOfCorepresentableBy h)

If F is corepresented by X, X with its universal element is the initial object of F.Elements.

Equations

• CategoryTheory.Functor.Elements.isInitialOfCorepresentableBy h = CategoryTheory.Limits.IsInitial.ofUniqueHom (fun (e : F.Elements) => { hom := h.homEquiv.symm e.val, map_val := ⋯ }) ⋯

@[reducible, inline]

abbrev CategoryTheory.Functor.Elements.initialYonedaObj {C : Type u} [Category.{v, u} C] (A : C) : (CategoryTheory.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.initialYonedaObj A = { obj := Opposite.op A, val := CategoryTheory.CategoryStruct.id A }

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

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

Equations

• CategoryTheory.Functor.Elements.isInitialYonedaObj A = CategoryTheory.Functor.Elements.isInitialOfRepresentableBy (CategoryTheory.Functor.RepresentableBy.yoneda A)

@[deprecated CategoryTheory.Functor.Elements.initialYonedaObj (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.initialYonedaObj.

---

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.yoneda = @CategoryTheory.Functor.Elements.initialYonedaObj

@[deprecated CategoryTheory.Functor.Elements.isInitialYonedaObj (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.isInitialYonedaObj.

---

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

Equations

• @CategoryTheory.Functor.Elements.isInitial = @CategoryTheory.Functor.Elements.isInitialYonedaObj

@[implicit_reducible]

def CategoryTheory.Functor.Elements.precomp {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) (G : Functor D (Type w)) : Functor (F.comp G).Elements G.Elements

The functor (F ⋙ G).Elements ⥤ G.Elements.

Equations

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

@[simp]

theorem CategoryTheory.Functor.Elements.precomp_obj_val {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) (G : Functor D (Type w)) (x : (F.comp G).Elements) : ((precomp F G).obj x).val = x.val

@[simp]

theorem CategoryTheory.Functor.Elements.precomp_map_hom {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) (G : Functor D (Type w)) {X✝ Y✝ : (F.comp G).Elements} (f : X✝ ⟶ Y✝) : ((precomp F G).map f).hom = F.map f.hom

@[simp]

theorem CategoryTheory.Functor.Elements.precomp_obj_obj {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) (G : Functor D (Type w)) (x : (F.comp G).Elements) : ((precomp F G).obj x).obj = F.obj x.obj

instance CategoryTheory.Functor.Elements.essentiallySmall {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) [EssentiallySmall.{w, v, u} C] : EssentiallySmall.{w, v, max u w} F.Elements

def CategoryTheory.NatTrans.mapElementsOpCompToCostructuredArrowIso {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type v)} (α : F₁ ⟶ F₂) : (mapElements α).op.comp (Functor.Elements.toCostructuredArrow F₂) ≅ (Functor.Elements.toCostructuredArrow F₁).comp (CostructuredArrow.map α)

The functor Functor.Elements.toCostructuredArrow is compatible with NatTrans.mapElements.

Equations

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

@[simp]

theorem CategoryTheory.NatTrans.mapElementsOpCompToCostructuredArrowIso_hom_app {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type v)} (α : F₁ ⟶ F₂) (X : F₁.Elementsᵒᵖ) : (mapElementsOpCompToCostructuredArrowIso α).hom.app X = (CostructuredArrow.isoMk (Iso.refl (Opposite.unop (Opposite.unop X).obj)) ⋯).hom

@[simp]

theorem CategoryTheory.NatTrans.mapElementsOpCompToCostructuredArrowIso_inv_app {C : Type u} [Category.{v, u} C] {F₁ F₂ : Functor Cᵒᵖ (Type v)} (α : F₁ ⟶ F₂) (X : F₁.Elementsᵒᵖ) : (mapElementsOpCompToCostructuredArrowIso α).inv.app X = (CostructuredArrow.isoMk (Iso.refl (Opposite.unop (Opposite.unop X).obj)) ⋯).inv

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

@[deprecated CategoryTheory.Functor.Elements.homMk (since := "2026-08-30")]

def CategoryTheory.CategoryOfElements.homMk {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} {x y : F.Elements} (f : x.obj ⟶ y.obj) (hf : (ConcreteCategory.hom (F.map f)) x.val = y.val := by cat_disch) : x ⟶ y

Alias of CategoryTheory.Functor.Elements.homMk.

---

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

Equations

• @CategoryTheory.CategoryOfElements.homMk = @CategoryTheory.Functor.Elements.homMk

@[deprecated CategoryTheory.Functor.Elements.isoMk (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.isoMk.

---

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

Equations

• @CategoryTheory.CategoryOfElements.isoMk = @CategoryTheory.Functor.Elements.isoMk

@[deprecated CategoryTheory.Functor.Elements.hom_ext (since := "2026-08-30")]

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.hom = g.hom) : f = g

Alias of CategoryTheory.Functor.Elements.hom_ext.

@[deprecated CategoryTheory.Functor.Elements.id_hom (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.id_hom.

@[deprecated CategoryTheory.Functor.Elements.comp_hom (since := "2026-08-30")]

theorem CategoryTheory.CategoryOfElements.comp_val {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} {X✝ Y✝ Z✝ : F.Elements} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

Alias of CategoryTheory.Functor.Elements.comp_hom.

@[deprecated CategoryTheory.Functor.Elements.Hom.map_val (since := "2026-08-30")]

theorem CategoryTheory.CategoryOfElements.map_snd {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} {x y : F.Elements} (self : x.Hom y) : (ConcreteCategory.hom (F.map self.hom)) x.val = y.val

Alias of CategoryTheory.Functor.Elements.Hom.map_val.

@[deprecated CategoryTheory.Functor.Elements.π (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.π.

---

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

Equations

• @CategoryTheory.CategoryOfElements.π = @CategoryTheory.Functor.Elements.π

@[deprecated CategoryTheory.NatTrans.mapElements (since := "2026-08-30")]

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

Alias of CategoryTheory.NatTrans.mapElements.

---

Natural transformations are mapped to functors between categories of elements.

Equations

• @CategoryTheory.CategoryOfElements.map = @CategoryTheory.NatTrans.mapElements

@[deprecated CategoryTheory.NatTrans.mapElements_comp_π (since := "2026-08-30")]

theorem CategoryTheory.CategoryOfElements.map_π {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (φ : F ⟶ G) : (NatTrans.mapElements φ).comp (Functor.Elements.π G) = Functor.Elements.π F

Alias of CategoryTheory.NatTrans.mapElements_comp_π.

@[deprecated CategoryTheory.Functor.Elements.toStructuredArrow (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.toStructuredArrow.

---

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

Equations

• @CategoryTheory.CategoryOfElements.toStructuredArrow = @CategoryTheory.Functor.Elements.toStructuredArrow

@[deprecated CategoryTheory.Functor.Elements.fromStructuredArrow (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.fromStructuredArrow.

---

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

Equations

• @CategoryTheory.CategoryOfElements.fromStructuredArrow = @CategoryTheory.Functor.Elements.fromStructuredArrow

@[deprecated CategoryTheory.Functor.Elements.toStructuredArrow_obj (since := "2026-08-30")]

theorem CategoryTheory.CategoryOfElements.fromStructuredArrow_obj {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) (e : F.Elements) : (Functor.Elements.toStructuredArrow F).obj e = StructuredArrow.mk (TypeCat.ofHom fun (x : PUnit.{w + 1}) => e.val)

Alias of CategoryTheory.Functor.Elements.toStructuredArrow_obj.

@[deprecated CategoryTheory.Functor.Elements.toStructuredArrow_map (since := "2026-08-30")]

theorem CategoryTheory.CategoryOfElements.fromStructuredArrow_map {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {X✝ Y✝ : F.Elements} (f : X✝ ⟶ Y✝) : (Functor.Elements.toStructuredArrow F).map f = StructuredArrow.homMk f.hom ⋯

Alias of CategoryTheory.Functor.Elements.toStructuredArrow_map.

@[deprecated CategoryTheory.Functor.Elements.structuredArrowEquivalence (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.structuredArrowEquivalence.

---

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

Equations

• @CategoryTheory.CategoryOfElements.structuredArrowEquivalence = @CategoryTheory.Functor.Elements.structuredArrowEquivalence

@[deprecated CategoryTheory.Functor.Elements.toCostructuredArrow (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.toCostructuredArrow.

---

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

Equations

• @CategoryTheory.CategoryOfElements.toCostructuredArrow = @CategoryTheory.Functor.Elements.toCostructuredArrow

@[deprecated CategoryTheory.Functor.Elements.fromCostructuredArrow (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.fromCostructuredArrow.

---

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

Equations

• @CategoryTheory.CategoryOfElements.fromCostructuredArrow = @CategoryTheory.Functor.Elements.fromCostructuredArrow

@[deprecated CategoryTheory.Functor.Elements.fromCostructuredArrow_obj_mk (since := "2026-08-30")]

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) : (Functor.Elements.fromCostructuredArrow F).obj (Opposite.op (CostructuredArrow.mk f)) = F.elementsMk (Opposite.op X) (yonedaEquiv f)

Alias of CategoryTheory.Functor.Elements.fromCostructuredArrow_obj_mk.

@[deprecated CategoryTheory.Functor.Elements.costructuredArrowYonedaEquivalence (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.costructuredArrowYonedaEquivalence.

---

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

Equations

• @CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence = @CategoryTheory.Functor.Elements.costructuredArrowYonedaEquivalence

@[deprecated CategoryTheory.NatTrans.mapElements_op_comp_toCostructuredArrow (since := "2026-08-30")]

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

Alias of CategoryTheory.NatTrans.mapElements_op_comp_toCostructuredArrow.

@[deprecated CategoryTheory.Functor.Elements.costructuredArrowYonedaEquivalenceFunctorProj (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.costructuredArrowYonedaEquivalenceFunctorProj.

---

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

Equations

• @CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj = @CategoryTheory.Functor.Elements.costructuredArrowYonedaEquivalenceFunctorProj

@[deprecated CategoryTheory.Functor.Elements.costructuredArrowYonedaEquivalenceInverseπ (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.costructuredArrowYonedaEquivalenceInverseπ.

---

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

Equations

• @CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ = @CategoryTheory.Functor.Elements.costructuredArrowYonedaEquivalenceInverseπ

@[deprecated CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalence (since := "2026-08-30")]

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

Alias of CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalence.

---

The opposite of the category of elements of a presheaf of types is equivalent to a category of costructured arrows for the Yoneda embedding functor.

Equations

• @CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence = @CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalence

@[deprecated CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalenceFunctorCompProjIso (since := "2026-08-30")]

def CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalenceFunctorCompProjIso {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type (max w v))) : (Functor.Elements.costructuredArrowULiftYonedaEquivalence F).functor.comp (CostructuredArrow.proj uliftYoneda.{w, v, u} F) ≅ (Functor.Elements.π F).leftOp

Alias of CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalenceFunctorCompProjIso.

---

The functor of the equivalence costructuredArrowULiftYonedaEquivalence F followed by the projection CostructuredArrow uliftYoneda.{w} F ⥤ C identifies to (π F).leftOp.

Equations

• @CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalenceFunctorCompProjIso = @CategoryTheory.Functor.Elements.costructuredArrowULiftYonedaEquivalenceFunctorCompProjIso

@[deprecated "No replacement (this is proven `by dsimp`)" (since := "2026-08-30")]

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) : StructuredArrow.Hom.right ((Functor.Elements.toStructuredArrow F).map f) = f.hom