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

theorem CategoryTheory.Sieve.W_shrinkFunctor_ι_of_mem {C : Type u_1} [Category.{v_1, u_1} C] (J : GrothendieckTopology C) [LocallySmall.{w, v_1, u_1} C] {X : C} (S : Sieve X) (hS : S ∈ J X) : J.W (shrinkFunctor.{w, v_1, u_1} S).ι

theorem CategoryTheory.Presieve.IsSheaf.comp_of_W_map_of_adjunction {C : Type u_1} [Category.{v_1, u_1} C] (J : GrothendieckTopology C) {D : Type u_3} [Category.{v_3, u_3} D] {K : GrothendieckTopology D} [LocallySmall.{w, v_1, u_1} C] {F : Functor C D} {H : Functor (Functor Cᵒᵖ (Type w)) (Functor Dᵒᵖ (Type w))} (adj : H ⊣ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)).obj F.op) (h : ∀ ⦃X : C⦄ ⦃S : Sieve X⦄, S ∈ J X → K.W (H.map (Sieve.shrinkFunctor.{w, v_1, u_1} S).ι)) (G : Functor Dᵒᵖ (Type w)) (hG : IsSheaf K G) : IsSheaf J (F.op.comp G)

SGA 4 III 1.2 (ii) => (i)