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]
• https://en.wikipedia.org/wiki/Category_of_elements
• https://ncatlab.org/nlab/show/category+of+elements

Tags

category of elements, Grothendieck construction, comma category

def CategoryTheory.Functor.Elements {C : Type u} [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

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

@[reducible, inline]

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

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

Equations

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

theorem CategoryTheory.Functor.Elements.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x : F.Elements) (y : F.Elements) (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} 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

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

@[simp]

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

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

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

Equations

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

theorem CategoryTheory.CategoryOfElements.ext {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {x : F.Elements} {y : F.Elements} (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 : F.Elements} {q : F.Elements} {r : F.Elements} {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 : F.Elements} : ↑(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 : F.Elements} {q : F.Elements} (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 F.Elements

Equations

• CategoryTheory.groupoidOfElements F = CategoryTheory.Groupoid.mk (fun {p q : F.Elements} (f : p ⟶ q) => ⟨CategoryTheory.Groupoid.inv ↑f, ⋯⟩) ⋯ ⋯

@[simp]

theorem CategoryTheory.CategoryOfElements.π_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (X : F.Elements) : (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 : F.Elements} (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 F.Elements C

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[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₁ : F₁.Elements} {t₂ : F₁.Elements} (k : t₁ ⟶ t₂) : ↑((CategoryTheory.CategoryOfElements.map α).map k) = ↑k

@[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 : F₁.Elements) : ((CategoryTheory.CategoryOfElements.map α).obj t).snd = α.app t.fst t.snd

@[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 : F₁.Elements) : ((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 F₁.Elements F₂.Elements

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

Equations

• CategoryTheory.CategoryOfElements.map α = { obj := fun (t : F₁.Elements) => ⟨t.fst, α.app t.fst t.snd⟩, map := fun {t₁ t₂ : F₁.Elements} (k : t₁ ⟶ t₂) => ⟨↑k, ⋯⟩, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.CategoryOfElements.map_π {C : Type u} [CategoryTheory.Category.{v, u} C] {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (α : F₁ ⟶ F₂) : (CategoryTheory.CategoryOfElements.map α).comp (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 F.Elements (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 : F.Elements) : (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 : F.Elements} {Y : F.Elements} (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) F.Elements

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

Equations

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

@[simp]

theorem CategoryTheory.CategoryOfElements.fromStructuredArrow_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.StructuredArrow PUnit.{w + 1} F) : (CategoryTheory.CategoryOfElements.fromStructuredArrow F).obj X = ⟨X.right, 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 = ⟨f.right, ⋯⟩

@[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_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_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 = ⟨X.right, X.hom PUnit.unit⟩

@[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.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).leftUnitor.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents (fun (X : F.Elements) => CategoryTheory.Iso.refl X) ⋯).hom ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryOfElements.toStructuredArrow F).associator (CategoryTheory.CategoryOfElements.fromStructuredArrow F) ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) ((CategoryTheory.CategoryOfElements.fromStructuredArrow F).associator (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.CategoryOfElements.fromStructuredArrow F).leftUnitor.hom) (CategoryTheory.NatIso.ofComponents (fun (X : F.Elements) => CategoryTheory.Iso.refl X) ⋯).inv)))))

@[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 : F.Elements) => CategoryTheory.Iso.refl X) ⋯).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F).leftUnitor.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.CategoryOfElements.fromStructuredArrow F).associator (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).hom) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryOfElements.toStructuredArrow F).associator (CategoryTheory.CategoryOfElements.fromStructuredArrow F) ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents (fun (X : F.Elements) => CategoryTheory.Iso.refl X) ⋯).inv ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).leftUnitor.hom)))))

@[simp]

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

@[simp]

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

@[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 = ⟨f.right, ⋯⟩

def CategoryTheory.CategoryOfElements.structuredArrowEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) : F.Elements ≌ 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 : F.Elementsᵒᵖ} (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 : F.Elementsᵒᵖ) : (CategoryTheory.CategoryOfElements.toCostructuredArrow F).obj X = CategoryTheory.CostructuredArrow.mk (CategoryTheory.yonedaEquiv.symm (Opposite.unop X).snd)

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

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

@[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 (Opposite.unop X).hom

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)ᵒᵖ F.Elements

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

Equations

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

@[simp]

theorem CategoryTheory.CategoryOfElements.fromCostructuredArrow_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)) = ⟨Opposite.op X, 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.CategoryOfElements.toCostructuredArrow F).rightOp.comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F) = CategoryTheory.Functor.id F.Elements

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.CategoryOfElements.fromCostructuredArrow F).rightOp.comp (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_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) (X : F.Elementsᵒᵖ) : (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).functor.obj X = CategoryTheory.CostructuredArrow.mk (CategoryTheory.yonedaEquiv.symm (Opposite.unop X).snd)

@[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_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_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.CategoryOfElements.toCostructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).leftUnitor.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatTrans.op (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).associator (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) ((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp.associator (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.CategoryOfElements.fromCostructuredArrow F).rightOp.leftUnitor.hom) (CategoryTheory.NatTrans.op (CategoryTheory.eqToHom ⋯)))))))

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

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

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

@[simp]

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

@[simp]

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

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

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

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

def CategoryTheory.Functor.Elements.initial {C : Type u} [CategoryTheory.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.initial A = ⟨Opposite.op A, CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op A))⟩

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

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

Equations

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