Computation of Over A for a presheaf A

Let A : Cᵒᵖ ⥤ Type v be a presheaf. In this file, we construct an equivalence e : Over A ≌ (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v and show that there is a quasi-commutative diagram

CostructuredArrow yoneda A      ⥤      Over A

                             ⇘           ⥥

                               PSh(CostructuredArrow yoneda A)

where the top arrow is the forgetful functor forgetting the yoneda-costructure, the right arrow is the aforementioned equivalence and the diagonal arrow is the Yoneda embedding.

In the notation of Kashiwara-Schapira, the type of the equivalence is written C^ₐ ≌ Cₐ^, where ·ₐ is CostructuredArrow (with the functor S being either the identity or the Yoneda embedding) and ^ is taking presheaves. The equivalence is a key ingredient in various results in Kashiwara-Schapira.

The proof is somewhat long and technical, in part due to the construction inherently involving a sigma type which comes with the usual DTT issues. However, a user of this result should not need to interact with the actual construction, the mere existence of the equivalence and the commutative triangle should generally be sufficient.

Main results

• overEquivPresheafCostructuredArrow: the equivalence Over A ≌ (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
• CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow: the natural isomorphism CostructuredArrow.toOver yoneda A ⋙ (overEquivPresheafCostructuredArrow A).functor ≅ yoneda

Implementation details

The proof needs to introduce "correction terms" in various places in order to overcome DTT issues, and these need to be canceled against each other when appropriate. It is important to deal with these in a structured manner, otherwise you get large goals containing many correction terms which are very tedious to manipulate. We avoid this blowup by carefully controlling which definitions (d)simp is allowed to unfold and stating many lemmas explicitly before they are required. This leads to manageable goals containing only a small number of correction terms. Generally, we use the form F.map (eqToHom _) for these correction terms and try to push them as far outside as possible.

Future work

• If needed, it should be possible to show that the equivalence is natural in A.

References

• [M. Kashiwara, P. Schapira, Categories and Sheaves][Kashiwara2006], Lemma 1.4.12

Tags

presheaf, over category, coyoneda

Construction of the forward functor Over A ⥤ (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v

structure CategoryTheory.OverPresheafAux.MakesOverArrow {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) {X : C} (s : CategoryTheory.yoneda.obj X ⟶ A) (u : F.obj (Opposite.op X)) : Prop

Via the Yoneda lemma, u : F.obj (op X) defines a natural transformation yoneda.obj X ⟶ F and via the element η.app (op X) u also a morphism yoneda.obj X ⟶ A. This structure witnesses the fact that these morphisms from a commutative triangle with η : F ⟶ A, i.e., that yoneda.obj X ⟶ F lifts to a morphism in Over A.

• app : η.app (Opposite.op X) u = CategoryTheory.yonedaEquiv s

theorem CategoryTheory.OverPresheafAux.MakesOverArrow.app {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} {u : F.obj (Opposite.op X)} (self : CategoryTheory.OverPresheafAux.MakesOverArrow η s u) : η.app (Opposite.op X) u = CategoryTheory.yonedaEquiv s

theorem CategoryTheory.OverPresheafAux.MakesOverArrow.map₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {μ : G ⟶ A} {ε : F ⟶ G} (hε : CategoryTheory.CategoryStruct.comp ε μ = η) {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} {u : F.obj (Opposite.op X)} (h : CategoryTheory.OverPresheafAux.MakesOverArrow η s u) : CategoryTheory.OverPresheafAux.MakesOverArrow μ s (ε.app (Opposite.op X) u)

"Functoriality" of MakesOverArrow η s in η.

theorem CategoryTheory.OverPresheafAux.MakesOverArrow.map₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {X : C} {Y : C} (f : X ⟶ Y) {s : CategoryTheory.yoneda.obj X ⟶ A} {t : CategoryTheory.yoneda.obj Y ⟶ A} (hst : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s) {u : F.obj (Opposite.op Y)} (h : CategoryTheory.OverPresheafAux.MakesOverArrow η t u) : CategoryTheory.OverPresheafAux.MakesOverArrow η s (F.map f.op u)

"Functoriality of MakesOverArrow η s in s.

theorem CategoryTheory.OverPresheafAux.MakesOverArrow.of_arrow {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} {f : CategoryTheory.yoneda.obj X ⟶ F} (hf : CategoryTheory.CategoryStruct.comp f η = s) : CategoryTheory.OverPresheafAux.MakesOverArrow η s (CategoryTheory.yonedaEquiv f)

theorem CategoryTheory.OverPresheafAux.MakesOverArrow.of_yoneda_arrow {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} {η : CategoryTheory.yoneda.obj Y ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} {f : X ⟶ Y} (hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) η = s) : CategoryTheory.OverPresheafAux.MakesOverArrow η s f

def CategoryTheory.OverPresheafAux.OverArrows {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) {X : C} (s : CategoryTheory.yoneda.obj X ⟶ A) : Type v

This is equivalent to the type Over.mk s ⟶ Over.mk η, but that lives in the wrong universe. However, if F = yoneda.obj Y for some Y, then (using that the Yoneda embedding is fully faithful) we get a good statement, see OverArrow.costructuredArrowIso.

Equations

• CategoryTheory.OverPresheafAux.OverArrows η s = Subtype (CategoryTheory.OverPresheafAux.MakesOverArrow η s)

def CategoryTheory.OverPresheafAux.OverArrows.val {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} : CategoryTheory.OverPresheafAux.OverArrows η s → F.obj (Opposite.op X)

Since OverArrows η s can be thought of to contain certain morphisms yoneda.obj X ⟶ F, the Yoneda lemma yields elements F.obj (op X).

Equations

• CategoryTheory.OverPresheafAux.OverArrows.val = Subtype.val

@[simp]

theorem CategoryTheory.OverPresheafAux.OverArrows.val_mk {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) {X : C} (s : CategoryTheory.yoneda.obj X ⟶ A) (u : F.obj (Opposite.op X)) (h : CategoryTheory.OverPresheafAux.MakesOverArrow η s u) : CategoryTheory.OverPresheafAux.OverArrows.val ⟨u, h⟩ = u

theorem CategoryTheory.OverPresheafAux.OverArrows.ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} {u : CategoryTheory.OverPresheafAux.OverArrows η s} {v : CategoryTheory.OverPresheafAux.OverArrows η s} : u = v ↔ u.val = v.val

theorem CategoryTheory.OverPresheafAux.OverArrows.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} {u : CategoryTheory.OverPresheafAux.OverArrows η s} {v : CategoryTheory.OverPresheafAux.OverArrows η s} : u.val = v.val → u = v

theorem CategoryTheory.OverPresheafAux.OverArrows.app_val {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} (p : CategoryTheory.OverPresheafAux.OverArrows η s) : η.app (Opposite.op X) p.val = CategoryTheory.yonedaEquiv s

The defining property of OverArrows.val.

@[simp]

theorem CategoryTheory.OverPresheafAux.OverArrows.map_val {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} {η : CategoryTheory.yoneda.obj Y ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} (p : CategoryTheory.OverPresheafAux.OverArrows η s) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map p.val) η = s

In the special case F = yoneda.obj Y, the element p.val for p : OverArrows η s is itself a morphism X ⟶ Y.

def CategoryTheory.OverPresheafAux.OverArrows.map₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {μ : G ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} (u : CategoryTheory.OverPresheafAux.OverArrows η s) (ε : F ⟶ G) (hε : CategoryTheory.CategoryStruct.comp ε μ = η) : CategoryTheory.OverPresheafAux.OverArrows μ s

Functoriality of OverArrows η s in η.

Equations

• u.map₁ ε hε = ⟨ε.app (Opposite.op X) u.val, ⋯⟩

@[simp]

theorem CategoryTheory.OverPresheafAux.OverArrows.map₁_val {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {μ : G ⟶ A} {X : C} (s : CategoryTheory.yoneda.obj X ⟶ A) (u : CategoryTheory.OverPresheafAux.OverArrows η s) (ε : F ⟶ G) (hε : CategoryTheory.CategoryStruct.comp ε μ = η) : (u.map₁ ε hε).val = ε.app (Opposite.op X) u.val

def CategoryTheory.OverPresheafAux.OverArrows.map₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {X : C} {Y : C} {s : CategoryTheory.yoneda.obj X ⟶ A} {t : CategoryTheory.yoneda.obj Y ⟶ A} (u : CategoryTheory.OverPresheafAux.OverArrows η t) (f : X ⟶ Y) (hst : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s) : CategoryTheory.OverPresheafAux.OverArrows η s

Functoriality of OverArrows η s in s.

Equations

• u.map₂ f hst = ⟨F.map f.op u.val, ⋯⟩

@[simp]

theorem CategoryTheory.OverPresheafAux.OverArrows.map₂_val {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {X : C} {Y : C} (f : X ⟶ Y) {s : CategoryTheory.yoneda.obj X ⟶ A} {t : CategoryTheory.yoneda.obj Y ⟶ A} (hst : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s) (u : CategoryTheory.OverPresheafAux.OverArrows η t) : (u.map₂ f hst).val = F.map f.op u.val

@[simp]

theorem CategoryTheory.OverPresheafAux.OverArrows.map₁_map₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {μ : G ⟶ A} (ε : F ⟶ G) (hε : CategoryTheory.CategoryStruct.comp ε μ = η) {X : C} {Y : C} {s : CategoryTheory.yoneda.obj X ⟶ A} {t : CategoryTheory.yoneda.obj Y ⟶ A} (f : X ⟶ Y) (hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s) (u : CategoryTheory.OverPresheafAux.OverArrows η t) : (u.map₁ ε hε).map₂ f hf = (u.map₂ f hf).map₁ ε hε

def CategoryTheory.OverPresheafAux.OverArrows.yonedaArrow {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} {η : CategoryTheory.yoneda.obj Y ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} (f : X ⟶ Y) (hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) η = s) : CategoryTheory.OverPresheafAux.OverArrows η s

Construct an element of OverArrows η s with F = yoneda.obj Y from a suitable morphism f : X ⟶ Y.

Equations

• CategoryTheory.OverPresheafAux.OverArrows.yonedaArrow f hf = ⟨f, ⋯⟩

@[simp]

theorem CategoryTheory.OverPresheafAux.OverArrows.yonedaArrow_val {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} {η : CategoryTheory.yoneda.obj Y ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} {f : X ⟶ Y} (hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) η = s) : (CategoryTheory.OverPresheafAux.OverArrows.yonedaArrow f hf).val = f

def CategoryTheory.OverPresheafAux.OverArrows.costructuredArrowIso {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) (t : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) : CategoryTheory.OverPresheafAux.OverArrows s.hom t.hom ≅ t ⟶ s

If η is also yoneda-costructured, then OverArrows η s is just morphisms of costructured arrows.

Equations

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

@[simp]

theorem CategoryTheory.OverPresheafAux.restrictedYonedaObj_map {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) : ∀ {X Y : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ} (f : X ⟶ Y) (u : CategoryTheory.OverPresheafAux.OverArrows η (Opposite.unop X).hom), (CategoryTheory.OverPresheafAux.restrictedYonedaObj η).map f u = u.map₂ f.unop.left ⋯

@[simp]

theorem CategoryTheory.OverPresheafAux.restrictedYonedaObj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (s : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ) : (CategoryTheory.OverPresheafAux.restrictedYonedaObj η).obj s = CategoryTheory.OverPresheafAux.OverArrows η (Opposite.unop s).hom

def CategoryTheory.OverPresheafAux.restrictedYonedaObj {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)

This is basically just yoneda.obj η : (Over A)ᵒᵖ ⥤ Type (max u v) restricted along the forgetful functor CostructuredArrow yoneda A ⥤ Over A, but done in a way that we land in a smaller universe.

Equations

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

@[simp]

theorem CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁_app {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {μ : G ⟶ A} (ε : F ⟶ G) (hε : CategoryTheory.CategoryStruct.comp ε μ = η) (s : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ) (u : (CategoryTheory.OverPresheafAux.restrictedYonedaObj η).obj s) : (CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁ ε hε).app s u = CategoryTheory.OverPresheafAux.OverArrows.map₁ u ε hε

def CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {μ : G ⟶ A} (ε : F ⟶ G) (hε : CategoryTheory.CategoryStruct.comp ε μ = η) : CategoryTheory.OverPresheafAux.restrictedYonedaObj η ⟶ CategoryTheory.OverPresheafAux.restrictedYonedaObj μ

Functoriality of restrictedYonedaObj η in η.

Equations

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

@[simp]

theorem CategoryTheory.OverPresheafAux.restrictedYoneda_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) (η : CategoryTheory.Over A) : (CategoryTheory.OverPresheafAux.restrictedYoneda A).obj η = CategoryTheory.OverPresheafAux.restrictedYonedaObj η.hom

@[simp]

theorem CategoryTheory.OverPresheafAux.restrictedYoneda_map {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) : ∀ {X Y : CategoryTheory.Over A} (ε : X ⟶ Y), (CategoryTheory.OverPresheafAux.restrictedYoneda A).map ε = CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁ ε.left ⋯

def CategoryTheory.OverPresheafAux.restrictedYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) : CategoryTheory.Functor (CategoryTheory.Over A) (CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v))

This is basically just yoneda : Over A ⥤ (Over A)ᵒᵖ ⥤ Type (max u v) restricted in the second argument along the forgetful functor CostructuredArrow yoneda A ⥤ Over A, but done in a way that we land in a smaller universe.

This is one direction of the equivalence we're constructing.

Equations

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

def CategoryTheory.OverPresheafAux.toOverYonedaCompRestrictedYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) : (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).comp (CategoryTheory.OverPresheafAux.restrictedYoneda A) ≅ CategoryTheory.yoneda

Further restricting the functor restrictedYoneda : Over A ⥤ (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v along the forgetful functor in the first argument recovers the Yoneda embedding CostructuredArrow yoneda A ⥤ (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v. This basically follows from the fact that the Yoneda embedding on C is fully faithful.

Equations

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

Construction of the backward functor ((CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) ⥤ Over A

theorem CategoryTheory.OverPresheafAux.map_mkPrecomp_eqToHom {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} {Y : C} {f : X ⟶ Y} {g : CategoryTheory.yoneda.obj Y ⟶ A} {g' : CategoryTheory.yoneda.obj Y ⟶ A} (h : g = g') {x : F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk g'))} : F.map (CategoryTheory.CostructuredArrow.mkPrecomp g f).op (F.map (CategoryTheory.eqToHom ⋯) x) = F.map (CategoryTheory.eqToHom ⋯) (F.map (CategoryTheory.CostructuredArrow.mkPrecomp g' f).op x)

This lemma will be key to establishing good simp normal forms.

def CategoryTheory.OverPresheafAux.YonedaCollection {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (X : C) : Type v

To give an object of Over A, we will in particular need a presheaf Cᵒᵖ ⥤ Type v. This is the definition of that presheaf on objects.

We would prefer to think of this sigma type to be indexed by natural transformations yoneda.obj X ⟶ A instead of A.obj (op X). These are equivalent by the Yoneda lemma, but we cannot use the former because that type lives in the wrong universe. Hence, we will provide a lot of API that will enable us to pretend that we are really indexing over yoneda.obj X ⟶ A.

Equations

• CategoryTheory.OverPresheafAux.YonedaCollection F X = ((s : A.obj (Opposite.op X)) × F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk (CategoryTheory.yonedaEquiv.symm s))))

def CategoryTheory.OverPresheafAux.YonedaCollection.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} (s : CategoryTheory.yoneda.obj X ⟶ A) (x : F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk s))) : CategoryTheory.OverPresheafAux.YonedaCollection F X

Given a costructured arrow s : yoneda.obj X ⟶ A and an element x : F.obj s, construct an element of YonedaCollection F X.

Equations

• CategoryTheory.OverPresheafAux.YonedaCollection.mk s x = ⟨CategoryTheory.yonedaEquiv s, F.map (CategoryTheory.eqToHom ⋯) x⟩

def CategoryTheory.OverPresheafAux.YonedaCollection.fst {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} (p : CategoryTheory.OverPresheafAux.YonedaCollection F X) : CategoryTheory.yoneda.obj X ⟶ A

Access the first component of an element of YonedaCollection F X.

Equations

• p.fst = CategoryTheory.yonedaEquiv.symm p.fst

def CategoryTheory.OverPresheafAux.YonedaCollection.snd {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} (p : CategoryTheory.OverPresheafAux.YonedaCollection F X) : F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk p.fst))

Access the second component of an element of YonedaCollection F X.

Equations

• p.snd = p.snd

def CategoryTheory.OverPresheafAux.YonedaCollection.yonedaEquivFst {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} (p : CategoryTheory.OverPresheafAux.YonedaCollection F X) : A.obj (Opposite.op X)

This is a definition because it will be helpful to be able to control precisely when this definition is unfolded.

Equations

• p.yonedaEquivFst = CategoryTheory.yonedaEquiv p.fst

theorem CategoryTheory.OverPresheafAux.YonedaCollection.yonedaEquivFst_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} (p : CategoryTheory.OverPresheafAux.YonedaCollection F X) : p.yonedaEquivFst = CategoryTheory.yonedaEquiv p.fst

@[simp]

theorem CategoryTheory.OverPresheafAux.YonedaCollection.mk_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} (s : CategoryTheory.yoneda.obj X ⟶ A) (x : F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk s))) : (CategoryTheory.OverPresheafAux.YonedaCollection.mk s x).fst = s

@[simp]

theorem CategoryTheory.OverPresheafAux.YonedaCollection.mk_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} (s : CategoryTheory.yoneda.obj X ⟶ A) (x : F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk s))) : (CategoryTheory.OverPresheafAux.YonedaCollection.mk s x).snd = F.map (CategoryTheory.eqToHom ⋯) x

theorem CategoryTheory.OverPresheafAux.YonedaCollection.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} {p : CategoryTheory.OverPresheafAux.YonedaCollection F X} {q : CategoryTheory.OverPresheafAux.YonedaCollection F X} (h : p.fst = q.fst) (h' : F.map (CategoryTheory.eqToHom ⋯) q.snd = p.snd) : p = q

def CategoryTheory.OverPresheafAux.YonedaCollection.map₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G) : CategoryTheory.OverPresheafAux.YonedaCollection F X → CategoryTheory.OverPresheafAux.YonedaCollection G X

Functoriality of YonedaCollection F X in F.

Equations

• CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η p = CategoryTheory.OverPresheafAux.YonedaCollection.mk p.fst (η.app (Opposite.op (CategoryTheory.CostructuredArrow.mk p.fst)) p.snd)

@[simp]

theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₁_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G) (p : CategoryTheory.OverPresheafAux.YonedaCollection F X) : (CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η p).fst = p.fst

@[simp]

theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₁_yonedaEquivFst {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G) (p : CategoryTheory.OverPresheafAux.YonedaCollection F X) : (CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η p).yonedaEquivFst = p.yonedaEquivFst

@[simp]

theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₁_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G) (p : CategoryTheory.OverPresheafAux.YonedaCollection F X) : (CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η p).snd = G.map (CategoryTheory.eqToHom ⋯) (η.app (Opposite.op (CategoryTheory.CostructuredArrow.mk p.fst)) p.snd)

def CategoryTheory.OverPresheafAux.YonedaCollection.map₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {X : C} (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) {Y : C} (f : X ⟶ Y) (p : CategoryTheory.OverPresheafAux.YonedaCollection F Y) : CategoryTheory.OverPresheafAux.YonedaCollection F X

Functoriality of YonedaCollection F X in X.

Equations

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

@[simp]

theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₂_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} {Y : C} (f : X ⟶ Y) (p : CategoryTheory.OverPresheafAux.YonedaCollection F Y) : (CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f p).fst = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) p.fst

@[simp]

theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₂_yonedaEquivFst {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} {Y : C} (f : X ⟶ Y) (p : CategoryTheory.OverPresheafAux.YonedaCollection F Y) : (CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f p).yonedaEquivFst = A.map f.op p.yonedaEquivFst

@[simp]

theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₂_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} {Y : C} (f : X ⟶ Y) (p : CategoryTheory.OverPresheafAux.YonedaCollection F Y) : (CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f p).snd = F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CostructuredArrow.mkPrecomp p.fst f).op (CategoryTheory.eqToHom ⋯)) p.snd

@[simp]

theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₁_id {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} : CategoryTheory.OverPresheafAux.YonedaCollection.map₁ (CategoryTheory.CategoryStruct.id F) = id

@[simp]

theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₁_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {H : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G) (μ : G ⟶ H) : CategoryTheory.OverPresheafAux.YonedaCollection.map₁ (CategoryTheory.CategoryStruct.comp η μ) = CategoryTheory.OverPresheafAux.YonedaCollection.map₁ μ ∘ CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η

@[simp]

theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₂_id {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} : CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F (CategoryTheory.CategoryStruct.id X) = id

@[simp]

theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₂_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f ∘ CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F g

@[simp]

theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₁_map₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G) {Y : C} (f : X ⟶ Y) (p : CategoryTheory.OverPresheafAux.YonedaCollection F Y) : CategoryTheory.OverPresheafAux.YonedaCollection.map₂ G f (CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η p) = CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η (CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f p)

@[simp]

theorem CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf_map {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (p : CategoryTheory.OverPresheafAux.YonedaCollection F (Opposite.unop X)), (CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A F).map f p = CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f.unop p

@[simp]

theorem CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (X : Cᵒᵖ) : (CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A F).obj X = CategoryTheory.OverPresheafAux.YonedaCollection F (Opposite.unop X)

def CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) : CategoryTheory.Functor Cᵒᵖ (Type v)

Given F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v, this is the presheaf that is given by YonedaCollection F X on objects.

Equations

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

@[simp]

theorem CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁_app {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G) (X : Cᵒᵖ) : ∀ (a : CategoryTheory.OverPresheafAux.YonedaCollection F (Opposite.unop X)), (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ η).app X a = CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η a

def CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G) : CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A F ⟶ CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A G

Functoriality of yonedaCollectionPresheaf A F in F.

Equations

• CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ η = { app := fun (X : Cᵒᵖ) => CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η, naturality := ⋯ }

@[simp]

theorem CategoryTheory.OverPresheafAux.yonedaCollectionFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) : (CategoryTheory.OverPresheafAux.yonedaCollectionFunctor A).obj F = CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A F

@[simp]

theorem CategoryTheory.OverPresheafAux.yonedaCollectionFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) : ∀ {X Y : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : X ⟶ Y), (CategoryTheory.OverPresheafAux.yonedaCollectionFunctor A).map η = CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ η

def CategoryTheory.OverPresheafAux.yonedaCollectionFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) : CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (CategoryTheory.Functor Cᵒᵖ (Type v))

This is the functor F ↦ X ↦ YonedaCollection F X.

Equations

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

@[simp]

theorem CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA_app {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (X : Cᵒᵖ) (p : CategoryTheory.OverPresheafAux.YonedaCollection F (Opposite.unop X)) : (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F).app X p = p.yonedaEquivFst

def CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) : CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A F ⟶ A

The Yoneda lemma yields a natural transformation yonedaCollectionPresheaf A F ⟶ A.

Equations

• CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F = { app := fun (X : Cᵒᵖ) => CategoryTheory.OverPresheafAux.YonedaCollection.yonedaEquivFst, naturality := ⋯ }

@[simp]

theorem CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver_map {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) : ∀ {X Y : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (g : X ⟶ Y), (CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver A).map g = CategoryTheory.CostructuredArrow.homMk (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ g) ⋯

@[simp]

theorem CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) (Y : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) : (CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver A).obj Y = CategoryTheory.CostructuredArrow.mk (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA Y)

def CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) : CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (CategoryTheory.Over A)

This is the reverse direction of the equivalence we're constructing.

Equations

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

Construction of the unit

def CategoryTheory.OverPresheafAux.unitForward {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : C) : CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) X → F.obj (Opposite.op X)

Forward direction of the unit.

Equations

• CategoryTheory.OverPresheafAux.unitForward η X p = CategoryTheory.OverPresheafAux.OverArrows.val p.snd

@[simp]

theorem CategoryTheory.OverPresheafAux.unitForward_naturality₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {μ : G ⟶ A} (ε : F ⟶ G) (hε : CategoryTheory.CategoryStruct.comp ε μ = η) (X : C) (p : CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) X) : CategoryTheory.OverPresheafAux.unitForward μ X (CategoryTheory.OverPresheafAux.YonedaCollection.map₁ (CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁ ε hε) p) = ε.app (Opposite.op X) (CategoryTheory.OverPresheafAux.unitForward η X p)

@[simp]

theorem CategoryTheory.OverPresheafAux.unitForward_naturality₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : C) (Y : C) (f : X ⟶ Y) (p : CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) Y) : CategoryTheory.OverPresheafAux.unitForward η X (CategoryTheory.OverPresheafAux.YonedaCollection.map₂ (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) f p) = F.map f.op (CategoryTheory.OverPresheafAux.unitForward η Y p)

@[simp]

theorem CategoryTheory.OverPresheafAux.app_unitForward {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : Cᵒᵖ) (p : CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) (Opposite.unop X)) : η.app X (CategoryTheory.OverPresheafAux.unitForward η (Opposite.unop X) p) = p.yonedaEquivFst

def CategoryTheory.OverPresheafAux.unitBackward {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : C) : F.obj (Opposite.op X) → CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) X

Backward direction of the unit.

Equations

• CategoryTheory.OverPresheafAux.unitBackward η X x = CategoryTheory.OverPresheafAux.YonedaCollection.mk (CategoryTheory.yonedaEquiv.symm (η.app (Opposite.op X) x)) ⟨x, ⋯⟩

theorem CategoryTheory.OverPresheafAux.unitForward_unitBackward {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : C) : CategoryTheory.OverPresheafAux.unitForward η X ∘ CategoryTheory.OverPresheafAux.unitBackward η X = id

theorem CategoryTheory.OverPresheafAux.unitBackward_unitForward {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : C) : CategoryTheory.OverPresheafAux.unitBackward η X ∘ CategoryTheory.OverPresheafAux.unitForward η X = id

@[simp]

theorem CategoryTheory.OverPresheafAux.unitAuxAuxAux_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : C) : ∀ (a : F.obj (Opposite.op X)), (CategoryTheory.OverPresheafAux.unitAuxAuxAux η X).inv a = CategoryTheory.OverPresheafAux.unitBackward η X a

@[simp]

theorem CategoryTheory.OverPresheafAux.unitAuxAuxAux_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : C) : ∀ (a : CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) X), (CategoryTheory.OverPresheafAux.unitAuxAuxAux η X).hom a = CategoryTheory.OverPresheafAux.unitForward η X a

def CategoryTheory.OverPresheafAux.unitAuxAuxAux {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : C) : CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) X ≅ F.obj (Opposite.op X)

Intermediate stage of assembling the unit.

Equations

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

@[simp]

theorem CategoryTheory.OverPresheafAux.unitAuxAux_inv_app_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : Cᵒᵖ) : ∀ (a : F.obj X), ((CategoryTheory.OverPresheafAux.unitAuxAux η).inv.app X a).fst = η.app X a

@[simp]

theorem CategoryTheory.OverPresheafAux.unitAuxAux_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : Cᵒᵖ) : ∀ (a : (CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A (CategoryTheory.OverPresheafAux.restrictedYonedaObj η)).obj X), (CategoryTheory.OverPresheafAux.unitAuxAux η).hom.app X a = CategoryTheory.OverPresheafAux.unitForward η (Opposite.unop X) a

@[simp]

theorem CategoryTheory.OverPresheafAux.unitAuxAux_inv_app_snd_coe {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : Cᵒᵖ) : ∀ (a : F.obj X), ↑((CategoryTheory.OverPresheafAux.unitAuxAux η).inv.app X a).snd = CategoryTheory.OverPresheafAux.OverArrows.val ⟨a, ⋯⟩

def CategoryTheory.OverPresheafAux.unitAuxAux {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) : CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) ≅ F

Intermediate stage of assembling the unit.

Equations

• CategoryTheory.OverPresheafAux.unitAuxAux η = CategoryTheory.NatIso.ofComponents (fun (X : Cᵒᵖ) => CategoryTheory.OverPresheafAux.unitAuxAuxAux η (Opposite.unop X)) ⋯

@[simp]

theorem CategoryTheory.OverPresheafAux.unitAux_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : CategoryTheory.Over A) : (CategoryTheory.OverPresheafAux.unitAux η).hom = { left := (CategoryTheory.OverPresheafAux.unitAuxAux η.hom).hom, right := CategoryTheory.CategoryStruct.id { as := PUnit.unit }, w := ⋯ }

def CategoryTheory.OverPresheafAux.unitAux {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : CategoryTheory.Over A) : ((CategoryTheory.OverPresheafAux.restrictedYoneda A).comp (CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver A)).obj η ≅ η

Intermediate stage of assembling the unit.

Equations

• CategoryTheory.OverPresheafAux.unitAux η = CategoryTheory.Over.isoMk (CategoryTheory.OverPresheafAux.unitAuxAux η.hom) ⋯

def CategoryTheory.OverPresheafAux.unit {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) : CategoryTheory.Functor.id (CategoryTheory.Over A) ≅ (CategoryTheory.OverPresheafAux.restrictedYoneda A).comp (CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver A)

The unit of the equivalence we're constructing.

Equations

• CategoryTheory.OverPresheafAux.unit A = (CategoryTheory.NatIso.ofComponents CategoryTheory.OverPresheafAux.unitAux ⋯).symm

Construction of the counit

@[simp]

theorem CategoryTheory.OverPresheafAux.OverArrows.yonedaCollectionPresheafToA_val_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} (s : CategoryTheory.yoneda.obj X ⟶ A) (p : CategoryTheory.OverPresheafAux.OverArrows (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F) s) : CategoryTheory.OverPresheafAux.YonedaCollection.fst p.val = s

def CategoryTheory.OverPresheafAux.counitForward {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) : F.obj (Opposite.op s) → CategoryTheory.OverPresheafAux.OverArrows (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F) s.hom

Forward direction of the counit.

Equations

• CategoryTheory.OverPresheafAux.counitForward F s x = ⟨CategoryTheory.OverPresheafAux.YonedaCollection.mk s.hom x, ⋯⟩

theorem CategoryTheory.OverPresheafAux.counitForward_val_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) (x : F.obj (Opposite.op s)) : CategoryTheory.OverPresheafAux.YonedaCollection.fst (CategoryTheory.OverPresheafAux.counitForward F s x).val = s.hom

@[simp]

theorem CategoryTheory.OverPresheafAux.counitForward_val_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) (x : F.obj (Opposite.op s)) : CategoryTheory.OverPresheafAux.YonedaCollection.snd (CategoryTheory.OverPresheafAux.counitForward F s x).val = F.map (CategoryTheory.eqToHom ⋯) x

@[simp]

theorem CategoryTheory.OverPresheafAux.counitForward_naturality₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G) (s : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ) (x : F.obj s) : CategoryTheory.OverPresheafAux.counitForward G (Opposite.unop s) (η.app s x) = (CategoryTheory.OverPresheafAux.counitForward F (Opposite.unop s) x).map₁ (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ η) ⋯

@[simp]

theorem CategoryTheory.OverPresheafAux.counitForward_naturality₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (s : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ) (t : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ) (f : t ⟶ s) (x : F.obj t) : CategoryTheory.OverPresheafAux.counitForward F (Opposite.unop s) (F.map f x) = (CategoryTheory.OverPresheafAux.counitForward F (Opposite.unop t) x).map₂ f.unop.left ⋯

def CategoryTheory.OverPresheafAux.counitBackward {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) : CategoryTheory.OverPresheafAux.OverArrows (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F) s.hom → F.obj (Opposite.op s)

Backward direction of the counit.

Equations

• CategoryTheory.OverPresheafAux.counitBackward F s p = F.map (CategoryTheory.eqToHom ⋯) (CategoryTheory.OverPresheafAux.YonedaCollection.snd p.val)

theorem CategoryTheory.OverPresheafAux.counitForward_counitBackward {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) : CategoryTheory.OverPresheafAux.counitForward F s ∘ CategoryTheory.OverPresheafAux.counitBackward F s = id

theorem CategoryTheory.OverPresheafAux.counitBackward_counitForward {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) : CategoryTheory.OverPresheafAux.counitBackward F s ∘ CategoryTheory.OverPresheafAux.counitForward F s = id

@[simp]

theorem CategoryTheory.OverPresheafAux.counitAuxAux_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) : ∀ (a : F.obj (Opposite.op s)), (CategoryTheory.OverPresheafAux.counitAuxAux F s).hom a = CategoryTheory.OverPresheafAux.counitForward F s a

@[simp]

theorem CategoryTheory.OverPresheafAux.counitAuxAux_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) : ∀ (a : CategoryTheory.OverPresheafAux.OverArrows (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F) s.hom), (CategoryTheory.OverPresheafAux.counitAuxAux F s).inv a = CategoryTheory.OverPresheafAux.counitBackward F s a

def CategoryTheory.OverPresheafAux.counitAuxAux {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) : F.obj (Opposite.op s) ≅ CategoryTheory.OverPresheafAux.OverArrows (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F) s.hom

Intermediate stage of assembling the counit.

Equations

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

@[simp]

theorem CategoryTheory.OverPresheafAux.counitAux_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) : (CategoryTheory.OverPresheafAux.counitAux F).hom = { app := fun (X : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ) => (CategoryTheory.OverPresheafAux.counitAuxAux F (Opposite.unop X)).hom, naturality := ⋯ }

def CategoryTheory.OverPresheafAux.counitAux {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) : F ≅ CategoryTheory.OverPresheafAux.restrictedYonedaObj (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F)

Intermediate stage of assembling the counit.

Equations

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

def CategoryTheory.OverPresheafAux.counit {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) : (CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver A).comp (CategoryTheory.OverPresheafAux.restrictedYoneda A) ≅ CategoryTheory.Functor.id (CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v))

The counit of the equivalence we're constructing.

Equations

• CategoryTheory.OverPresheafAux.counit A = (CategoryTheory.NatIso.ofComponents CategoryTheory.OverPresheafAux.counitAux ⋯).symm

def CategoryTheory.overEquivPresheafCostructuredArrow {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) : CategoryTheory.Over A ≌ CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)

If A : Cᵒᵖ ⥤ Type v is a presheaf, then we have an equivalence between presheaves lying over A and the category of presheaves on CostructuredArrow yoneda A. There is a quasicommutative triangle involving this equivalence, see CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow.

This is Lemma 1.4.12 in [Kashiwara2006].

Equations

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

def CategoryTheory.CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) : (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).comp (CategoryTheory.overEquivPresheafCostructuredArrow A).functor ≅ CategoryTheory.yoneda

If A : Cᵒᵖ ⥤ Type v is a presheaf, then the Yoneda embedding for CostructuredArrow yoneda A factors through Over A via a forgetful functor and an equivalence.

This is Lemma 1.4.12 in [Kashiwara2006].

Equations

• CategoryTheory.CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A = CategoryTheory.OverPresheafAux.toOverYonedaCompRestrictedYoneda A