Documentation

Mathlib.CategoryTheory.Sites.Adjunction

In this file, we show that an adjunction F ⊣ G induces an adjunction between categories of sheaves, under certain hypotheses on F and G.

@[inline, reducible]

The forgetful functor from Sheaf J D to sheaves of types, for a concrete category D whose forgetful functor preserves the correct limits.

Instances For
    @[simp]
    theorem CategoryTheory.Sheaf.composeEquiv_symm_apply_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [(X : C) → (S : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (adj : G F) (X : CategoryTheory.Sheaf J E) (Y : CategoryTheory.Sheaf J D) (γ : X (CategoryTheory.sheafCompose J F).obj Y) :
    @[simp]
    theorem CategoryTheory.Sheaf.composeEquiv_apply_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [(X : C) → (S : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (adj : G F) (X : CategoryTheory.Sheaf J E) (Y : CategoryTheory.Sheaf J D) (η : (CategoryTheory.Sheaf.composeAndSheafify J G).obj X Y) :
    @[simp]
    theorem CategoryTheory.Sheaf.adjunction_counit_app_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [(X : C) → (S : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (adj : G F) (Y : CategoryTheory.Sheaf J D) :
    @[simp]
    theorem CategoryTheory.Sheaf.adjunction_unit_app_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [(X : C) → (S : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (adj : G F) (X : CategoryTheory.Sheaf J E) :

    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 F preserves the correct limits.

    Instances For