Theorems · Definition · category theory

CategoryTheory.OverPresheafAux.YonedaCollection

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v) → 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.

Defined in

Mathlib.CategoryTheory.Comma.Presheaf.Basic

Cited by

24 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category