Theorems · Definition · category theory

CategoryTheory.Functor.sheafInducedTopologyEquivOfIsCoverDense

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (G : CategoryTheory.Functor C D) →
          (K : CategoryTheory.GrothendieckTopology D) →
            (A : Type v) →
              [inst_2 : CategoryTheory.Category.{u, v} A] →
                [G.LocallyCoverDense K] →
                  [G.IsLocallyFull K] →
                    [G.IsLocallyFaithful K] →
                      [G.IsCoverDense K] →
                        [∀ (X : Dᵒᵖ),
                              CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] →
                          CategoryTheory.Sheaf (G.inducedTopology K) A ≌ CategoryTheory.Sheaf K A

Cover-dense functors induce an equivalence of categories of sheaves. This is known as the comparison lemma. It requires that the sites are small and the value category is complete.

Defined in

Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.LocallyCoverDenseCategoryTheory.Functor.IsLocallyFullCategoryTheory.Functor.IsLocallyFaithfulCategoryTheory.Functor.IsCoverDenseCategoryTheory.Limits.HasLimitsOfShape