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.{v_1, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{v_2, u_2} A] : MorphismProperty (Functor Cᵒᵖ A)

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

theorem CategoryTheory.GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj {C : Type u_1} [Category.{v_1, u_1} C] (J : GrothendieckTopology C) (A : Type u_2) [Category.{v_2, u_2} A] : J.W = ObjectProperty.isLocal fun (x : Functor Cᵒᵖ A) => x ∈ Set.range (sheafToPresheaf J A).obj

@[deprecated CategoryTheory.GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj (since := "2025-11-20")]

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

Alias of CategoryTheory.GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj.

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

theorem CategoryTheory.GrothendieckTopology.W_adj_unit_app {C : Type u_1} [Category.{v_1, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{v_2, u_2} A] [HasWeakSheafify J A] (P : Functor Cᵒᵖ A) : J.W (CategoryTheory.toSheafify J P)

theorem CategoryTheory.GrothendieckTopology.W_iff {C : Type u_1} [Category.{v_1, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] (J : GrothendieckTopology C) (A : Type u_2) [Category.{v_2, 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.{v_1, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{v_2, u_2} A] [HasWeakSheafify J A] : (presheafToSheaf J A).IsLocalization J.W