The sheaf category as a localized category

In this file, it is shown that the category of sheaves Sheaf J A is a localization of the category Presheaf J A with respect to the class J.W of morphisms of presheaves which become isomorphisms after applying the sheafification functor.

@[reducible, inline]

abbrev CategoryTheory.GrothendieckTopology.W {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{u_4, u_2} A] : MorphismProperty (Functor Cᵒᵖ A)

The class of morphisms of presheaves which become isomorphisms after sheafification. (See GrothendieckTopology.W_iff.)

Equations

• J.W = CategoryTheory.Localization.LeftBousfield.W (CategoryTheory.Presheaf.IsSheaf J)

theorem CategoryTheory.GrothendieckTopology.W_eq_W_range_sheafToPresheaf_obj {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) (A : Type u_2) [Category.{u_4, u_2} A] : J.W = Localization.LeftBousfield.W fun (x : Functor Cᵒᵖ A) => x ∈ Set.range (sheafToPresheaf J A).obj

theorem CategoryTheory.GrothendieckTopology.W_sheafToPresheaf_map_iff_isIso {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{u_4, u_2} A] {F₁ F₂ : Sheaf J A} (φ : F₁ ⟶ F₂) : J.W ((sheafToPresheaf J A).map φ) ↔ IsIso φ

@[deprecated CategoryTheory.GrothendieckTopology.W_sheafToPresheaf_map_iff_isIso (since := "2025-07-27")]

theorem CategoryTheory.GrothendieckTopology.W_sheafToPreheaf_map_iff_isIso {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{u_4, u_2} A] {F₁ F₂ : Sheaf J A} (φ : F₁ ⟶ F₂) : J.W ((sheafToPresheaf J A).map φ) ↔ IsIso φ

Alias of CategoryTheory.GrothendieckTopology.W_sheafToPresheaf_map_iff_isIso.

theorem CategoryTheory.GrothendieckTopology.W_adj_unit_app {C : Type u_1} [Category.{u_4, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{u_3, u_2} A] {G : Functor (Functor Cᵒᵖ A) (Sheaf J A)} (adj : G ⊣ sheafToPresheaf J A) (P : Functor Cᵒᵖ A) : J.W (adj.unit.app P)

theorem CategoryTheory.GrothendieckTopology.W_iff_isIso_map_of_adjunction {C : Type u_1} [Category.{u_4, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{u_3, u_2} A] {G : Functor (Functor Cᵒᵖ A) (Sheaf J A)} (adj : G ⊣ sheafToPresheaf J A) {P₁ P₂ : Functor Cᵒᵖ A} (f : P₁ ⟶ P₂) : J.W f ↔ IsIso (G.map f)

theorem CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms_of_adjunction {C : Type u_1} [Category.{u_4, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{u_3, u_2} A] {G : Functor (Functor Cᵒᵖ A) (Sheaf J A)} (adj : G ⊣ sheafToPresheaf J A) : J.W = (MorphismProperty.isomorphisms (Sheaf J A)).inverseImage G

theorem CategoryTheory.GrothendieckTopology.W_toSheafify {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{u_4, u_2} A] [HasWeakSheafify J A] (P : Functor Cᵒᵖ A) : J.W (toSheafify J P)

theorem CategoryTheory.GrothendieckTopology.W_iff {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{u_4, u_2} A] [HasWeakSheafify J A] {P₁ P₂ : Functor Cᵒᵖ A} (f : P₁ ⟶ P₂) : J.W f ↔ IsIso ((presheafToSheaf J A).map f)

theorem CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) (A : Type u_2) [Category.{u_4, u_2} A] [HasWeakSheafify J A] : J.W = (MorphismProperty.isomorphisms (Sheaf J A)).inverseImage (presheafToSheaf J A)

instance CategoryTheory.GrothendieckTopology.instIsLocalizationFunctorOppositeSheafPresheafToSheafW {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{u_4, u_2} A] [HasWeakSheafify J A] : (presheafToSheaf J A).IsLocalization J.W