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).
Instances For
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₂ : C.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor x.fst y.fst
(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))
:
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.
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}
:
@[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}
:
noncomputable instance
CategoryTheory.groupoidOfElements
{G : Type u}
[CategoryTheory.Groupoid G]
(F : CategoryTheory.Functor G (Type w))
:
@[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))
:
The functor out of the category of elements which forgets the element.
Instances For
@[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
@[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_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 = C.app inst✝ (Type w) CategoryTheory.types F₁ F₂ α t.fst t.snd
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₂)
:
A natural transformation between functors induces a functor between the categories of elements.
Instances For
@[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₂)
:
def
CategoryTheory.CategoryOfElements.toStructuredArrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
:
The forward direction of the equivalence F.Elements ≅ (*, F).
Instances For
@[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 => 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))
:
The reverse direction of the equivalence F.Elements ≅ (*, F).
Instances For
@[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 :=
CategoryTheory.Comma.hom (CategoryTheory.Discrete PUnit.{1}) (CategoryTheory.discreteCategory PUnit.{1}) C inst✝
(Type w) CategoryTheory.types (CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ) F X 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 :=
(_ :
CategoryTheory.CategoryStruct.comp (Type w) CategoryTheory.Category.toCategoryStruct
((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).obj X.left) (F.obj X.right) (F.obj Y.right) X.hom
(F.map f.right) PUnit.unit = CategoryTheory.CategoryStruct.comp (Type w) CategoryTheory.Category.toCategoryStruct
((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).obj X.left)
((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).obj Y.left) (F.obj Y.right)
((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).map f.left) Y.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)
:
@[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.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.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.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_counitIso_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
:
(CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).counitIso.inv = CategoryTheory.NatTrans.mk fun X => (CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl X.right)).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 => X.snd
@[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.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.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.Iso.refl X).inv)))))
@[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 :=
CategoryTheory.Comma.hom (CategoryTheory.Discrete PUnit.{1}) (CategoryTheory.discreteCategory PUnit.{1}) C inst✝
(Type w) CategoryTheory.types (CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ) F X PUnit.unit }
@[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 = CategoryTheory.NatTrans.mk fun X => (CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl X.right)).hom
@[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 :=
(_ :
CategoryTheory.CategoryStruct.comp (Type w) CategoryTheory.Category.toCategoryStruct
((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).obj X.left) (F.obj X.right) (F.obj Y.right) X.hom
(F.map f.right) PUnit.unit = CategoryTheory.CategoryStruct.comp (Type w) CategoryTheory.Category.toCategoryStruct
((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).obj X.left)
((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).obj Y.left) (F.obj Y.right)
((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).map f.left) Y.hom PUnit.unit) }
def
CategoryTheory.CategoryOfElements.structuredArrowEquivalence
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
:
The equivalence between the category of elements F.Elements
and the comma category (*, F).
Instances For
@[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 })
@[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
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.
Instances For
@[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 = Equiv.toFun CategoryTheory.yonedaEquiv 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
@[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
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.
Instances For
@[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 := Equiv.toFun CategoryTheory.yonedaEquiv f }
theorem
CategoryTheory.CategoryOfElements.from_toCostructuredArrow_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
:
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))
:
The counit of the equivalence F.Elementsᵒᵖ ≅ (yoneda, F) is indeed iso.
@[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_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_counitIso_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
:
(CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).counitIso.hom = CategoryTheory.eqToHom
(_ :
CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp
(CategoryTheory.CategoryOfElements.toCostructuredArrow F) = CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F))
@[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).rightOp
(CategoryTheory.CategoryOfElements.fromCostructuredArrow F) = CategoryTheory.Functor.id (CategoryTheory.Functor.Elements F))))
(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.Functor.comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp
(CategoryTheory.CategoryOfElements.toCostructuredArrow F) = CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)))
(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
(_ :
CategoryTheory.Functor.id (CategoryTheory.Functor.Elements F) = CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F).rightOp
(CategoryTheory.CategoryOfElements.fromCostructuredArrow F)))))))))
@[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_inverse_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
(X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)
:
@[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
(_ :
CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F) = CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp
(CategoryTheory.CategoryOfElements.toCostructuredArrow F))
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.
Instances For
@[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.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F).rightOp
(CategoryTheory.CategoryOfElements.fromCostructuredArrow F) = CategoryTheory.Functor.id (CategoryTheory.Functor.Elements F))))
(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.Functor.id (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F) = CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp
(CategoryTheory.CategoryOfElements.toCostructuredArrow F)))
(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.id (CategoryTheory.Functor.Elements F) = CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F).rightOp
(CategoryTheory.CategoryOfElements.fromCostructuredArrow F))))
(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₂)
:
The equivalence (-.Elements)ᵒᵖ ≅ (yoneda, -) of is actually a natural isomorphism of functors.