Theorems · Definition · category theory

CategoryTheory.GrothendieckTopology.yonedaEquiv

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : J.Subcanonical] →
        {X : C} → {F : CategoryTheory.Sheaf J (Type v)} → (J.yoneda.obj X ⟶ F) ≃ F.obj.obj (Opposite.op X)

The equivalence between natural transformations from the yoneda embedding (to the sheaf category) and elements of F.val.obj X.

Defined in

Mathlib.CategoryTheory.Sites.Subcanonical

Cited by

18 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GrothendieckTopology.Subcanonical