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} [CategoryTheory.Category.{u_3, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_4, u_2} A] : CategoryTheory.MorphismProperty (CategoryTheory.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} [CategoryTheory.Category.{u_3, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_2) [CategoryTheory.Category.{u_4, u_2} A] : J.W = CategoryTheory.Localization.LeftBousfield.W fun (x : CategoryTheory.Functor Cᵒᵖ A) => x ∈ Set.range (CategoryTheory.sheafToPresheaf J A).obj

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

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

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

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

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

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

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

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

Equations

• ⋯ = ⋯