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

Tags

category of elements, Grothendieck construction, comma category

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

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

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

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

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

• CategoryTheory.categoryOfElements F = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

def CategoryTheory.CategoryOfElements.toStructuredArrow {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) : CategoryTheory.Functor (CategoryTheory.Functor.Elements F) (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Functor.Elements F) : (CategoryTheory.CategoryOfElements.toStructuredArrow F).obj X = { left := { as := PUnit.unit }, right := X.fst, hom := fun (x : (CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).obj { as := PUnit.unit }) => X.snd }

@[simp]

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

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_counitIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) : (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).counitIso.inv = { app := fun (X : CategoryTheory.StructuredArrow PUnit.{w + 1} F) => (CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl X.right) ⋯).inv, naturality := ⋯ }

@[simp]

theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_counitIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) : (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).counitIso.hom = { app := fun (X : CategoryTheory.StructuredArrow PUnit.{w + 1} F) => (CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl X.right) ⋯).hom, naturality := ⋯ }

@[simp]

theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_unitIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) : (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).unitIso.inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.leftUnitor (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.Functor.Elements F) => CategoryTheory.Iso.refl X) ⋯).hom (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F) (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.fromStructuredArrow F) (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.StructuredArrow PUnit.{w + 1} F) => CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl X.right) ⋯) ⋯).hom (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.Functor.leftUnitor (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).hom) (CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.Functor.Elements F) => CategoryTheory.Iso.refl X) ⋯).inv)))))

@[simp]

theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_functor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Functor.Elements F) : (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).functor.obj X = CategoryTheory.StructuredArrow.mk fun (x : PUnit.{w + 1} ) => X.snd

@[simp]

theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_unitIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) : (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).unitIso.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.Functor.Elements F) => CategoryTheory.Iso.refl X) ⋯).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.Functor.leftUnitor (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.StructuredArrow PUnit.{w + 1} F) => CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl X.right) ⋯) ⋯).inv (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.fromStructuredArrow F) (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F) (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.Functor.Elements F) => CategoryTheory.Iso.refl X) ⋯).inv (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) (CategoryTheory.Functor.leftUnitor (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F))).hom)))))

@[simp]

theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_inverse_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.StructuredArrow PUnit.{w + 1} F) : (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).inverse.obj X = { fst := X.right, snd := X.hom PUnit.unit }

@[simp]

theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_functor_map {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X : CategoryTheory.Functor.Elements F} {Y : CategoryTheory.Functor.Elements F} (f : X ⟶ Y) : (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).functor.map f = CategoryTheory.StructuredArrow.homMk ↑f ⋯

@[simp]

theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_inverse_map {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) : ∀ {X Y : CategoryTheory.StructuredArrow PUnit.{w + 1} F} (f : X ⟶ Y), (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).inverse.map f = { val := f.right, property := ⋯ }

def CategoryTheory.CategoryOfElements.structuredArrowEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) : CategoryTheory.Functor.Elements F ≌ CategoryTheory.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.toCostructuredArrow_map {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) : ∀ {X Y : (CategoryTheory.Functor.Elements F)ᵒᵖ} (f : X ⟶ Y), (CategoryTheory.CategoryOfElements.toCostructuredArrow F).map f = CategoryTheory.CostructuredArrow.homMk (↑f.unop).unop ⋯

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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_obj_mk {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) {X : C} (f : CategoryTheory.yoneda.obj X ⟶ F) : (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj (Opposite.op (CategoryTheory.CostructuredArrow.mk f)) = { fst := Opposite.op X, snd := CategoryTheory.yonedaEquiv.toFun f }

theorem CategoryTheory.CategoryOfElements.from_toCostructuredArrow_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) : CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F).rightOp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F) = CategoryTheory.Functor.id (CategoryTheory.Functor.Elements F)

The unit of the equivalence F.Elementsᵒᵖ ≅ (yoneda, F) is indeed iso.

theorem CategoryTheory.CategoryOfElements.to_fromCostructuredArrow_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) : CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) = CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)

The counit of the equivalence F.Elementsᵒᵖ ≅ (yoneda, F) is indeed iso.

@[simp]

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

@[simp]

theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_counitIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) : (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).counitIso.hom = CategoryTheory.eqToHom ⋯

@[simp]

theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_inverse_map {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) : ∀ {X Y : CategoryTheory.CostructuredArrow CategoryTheory.yoneda F} (f : X ⟶ Y), (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).inverse.map f = ((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).map f.op).op

@[simp]

theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_counitIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) : (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).counitIso.inv = CategoryTheory.eqToHom ⋯

@[simp]

theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_functor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) (X : (CategoryTheory.Functor.Elements F)ᵒᵖ) : (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).functor.obj X = CategoryTheory.CostructuredArrow.mk ((CategoryTheory.yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })

@[simp]

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

@[simp]

theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_unitIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) : (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).unitIso.inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.leftUnitor (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatTrans.op (CategoryTheory.eqToHom ⋯)) (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.whiskerRight (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.Functor.leftUnitor (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).hom) (CategoryTheory.NatTrans.op (CategoryTheory.eqToHom ⋯)))))))

def CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) : (CategoryTheory.Functor.Elements F)ᵒᵖ ≌ CategoryTheory.CostructuredArrow CategoryTheory.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_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) : (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).unitIso.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.op (CategoryTheory.eqToHom ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.Functor.leftUnitor (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.whiskerRight (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatTrans.op (CategoryTheory.eqToHom ⋯)) (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)) (CategoryTheory.Functor.leftUnitor (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)).hom)))))

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

def CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) : CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).inverse (CategoryTheory.CategoryOfElements.π F).leftOp ≅ CategoryTheory.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.