Documentation

Mathlib.CategoryTheory.Elements

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][riehl2017]
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

Instances For

@[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

Instances For

@[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

Instances For

@[reducible, inline]

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

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

Instances For

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) :

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

Instances For

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.

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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

Instances For

@[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.

Instances For

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.

Instances For

@[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

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

Instances For

@[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).

Instances For

@[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).

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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) :

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

Instances For

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.

Instances For

@[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) :

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

Instances For

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.

Instances For

@[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.

Instances For

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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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).

Instances For

@[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).

Instances For

@[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).

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

@[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