Theorems · Definition · category theory

CategoryTheory.equivCommuteConstant

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type u_2) →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.HasWeakSheafify J D] →
            {C' : Type u_3} →
              [inst_3 : CategoryTheory.Category.{v_3, u_3} C'] →
                (K : CategoryTheory.GrothendieckTopology C') →
                  [inst_4 : CategoryTheory.HasWeakSheafify K D] →
                    (G : CategoryTheory.Functor C C') →
                      [inst_5 :
                          ∀ (X : C'ᵒᵖ),
                            CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) D] →
                        [inst_6 : CategoryTheory.Functor.IsDenseSubsite J K G] →
                          {T : C} →
                            CategoryTheory.Limits.IsTerminal T →
                              CategoryTheory.Limits.IsTerminal (G.obj T) →
                                ((CategoryTheory.constantSheaf J D).comp
                                    (CategoryTheory.Functor.IsDenseSubsite.sheafEquiv J K G D).functor ≅
                                  CategoryTheory.constantSheaf K D)

The constant sheaf functor commutes up to isomorphism the equivalence of sheaf categories induced by a dense subsite.

Defined in

Mathlib.CategoryTheory.Sites.ConstantSheaf

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.HasWeakSheafifyCategoryTheory.CategoryCategoryTheory.HasWeakSheafifyCategoryTheory.Limits.HasLimitsOfShapeCategoryTheory.Functor.IsDenseSubsite