Theorems · Definition · category theory

CategoryTheory.sheafToPresheaf

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₂) →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Functor Cᵒᵖ A)

The inclusion functor of the category of sheaves in the category of presheaves.

Defined in

Mathlib.CategoryTheory.Sites.Sheaf

Cited by

142 results in Mathlib

Foundations

Depth 35 from the axioms, rests on 323 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category