Theorems · Definition · category theory

CategoryTheory.Sheaf.adjunction

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          {E : Type u_1} →
            [inst_2 : CategoryTheory.Category.{v_1, u_1} E] →
              {F : CategoryTheory.Functor D E} →
                {G : CategoryTheory.Functor E D} →
                  [inst_3 : CategoryTheory.HasWeakSheafify J D] →
                    [inst_4 : J.HasSheafCompose F] →
                      (G ⊣ F) → (CategoryTheory.Sheaf.composeAndSheafify J G ⊣ CategoryTheory.sheafCompose J F)

An adjunction adj : G ⊣ F with F : D ⥤ E and G : E ⥤ D induces an adjunction between Sheaf J D and Sheaf J E, in contexts where one can sheafify D-valued presheaves, and postcomposing with F preserves the property of being a sheaf.

Defined in

Mathlib.CategoryTheory.Sites.Adjunction

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.HasWeakSheafifyCategoryTheory.GrothendieckTopology.HasSheafCompose