Sheafification

Given a site (C, J) we define a typeclass HasSheafify J A saying that the inclusion functor from A-valued sheaves on C to presheaves admits a left exact left adjoint (sheafification).

Note: to access the HasSheafify instance for suitable concrete categories, import the file Mathlib/CategoryTheory/Sites/LeftExact.lean.

@[reducible, inline]

abbrev CategoryTheory.HasWeakSheafify {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] : Prop

A proposition saying that the inclusion functor from sheaves to presheaves admits a left adjoint.

Equations

• CategoryTheory.HasWeakSheafify J A = (CategoryTheory.sheafToPresheaf J A).IsRightAdjoint

class CategoryTheory.HasSheafify {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] : Prop

HasSheafify means that the inclusion functor from sheaves to presheaves admits a left exact left adjiont (sheafification).

Given a finite limit preserving functor F : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A and an adjunction adj : F ⊣ sheafToPresheaf J A, use HasSheafify.mk' to construct a HasSheafify instance.

• isRightAdjoint : HasWeakSheafify J A
• isLeftExact : Limits.PreservesFiniteLimits (sheafToPresheaf J A).leftAdjoint

instance CategoryTheory.instHasWeakSheafifyOfHasSheafify {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasSheafify J A] : HasWeakSheafify J A

instance CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafLeftAdjointSheafToPresheaf {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasSheafify J A] : Limits.PreservesFiniteLimits (sheafToPresheaf J A).leftAdjoint

theorem CategoryTheory.HasSheafify.mk' {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] {F : Functor (Functor Cᵒᵖ A) (Sheaf J A)} (adj : F ⊣ sheafToPresheaf J A) [Limits.PreservesFiniteLimits F] : HasSheafify J A

def CategoryTheory.presheafToSheaf {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] : Functor (Functor Cᵒᵖ A) (Sheaf J A)

The sheafification functor, left adjoint to the inclusion.

Equations

• CategoryTheory.presheafToSheaf J A = (CategoryTheory.sheafToPresheaf J A).leftAdjoint

instance CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasSheafify J A] : Limits.PreservesFiniteLimits (presheafToSheaf J A)

def CategoryTheory.sheafificationAdjunction {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] : presheafToSheaf J A ⊣ sheafToPresheaf J A

The sheafification-inclusion adjunction.

Equations

• CategoryTheory.sheafificationAdjunction J A = CategoryTheory.Adjunction.ofIsRightAdjoint (CategoryTheory.sheafToPresheaf J A)

instance CategoryTheory.instIsLeftAdjointFunctorOppositeSheafPresheafToSheaf {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] : (presheafToSheaf J A).IsLeftAdjoint

instance CategoryTheory.instReflectiveFunctorOppositeSheafSheafToPresheafOfHasWeakSheafify {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasWeakSheafify J A] : Reflective (sheafToPresheaf J A)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafReflectorSheafToPresheaf {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₂) [Category.{v₂, u₂} A] [HasSheafify J A] : Limits.PreservesFiniteLimits (reflector (sheafToPresheaf J A))

@[reducible, inline]

noncomputable abbrev CategoryTheory.sheafify {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] (P : Functor Cᵒᵖ D) : Functor Cᵒᵖ D

The sheafification of a presheaf P.

Equations

• CategoryTheory.sheafify J P = ((CategoryTheory.presheafToSheaf J D).obj P).val

@[reducible, inline]

noncomputable abbrev CategoryTheory.toSheafify {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] (P : Functor Cᵒᵖ D) : P ⟶ sheafify J P

The canonical map from P to its sheafification.

Equations

• CategoryTheory.toSheafify J P = (CategoryTheory.sheafificationAdjunction J D).unit.app P

@[simp]

theorem CategoryTheory.sheafificationAdjunction_unit_app {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] (P : Functor Cᵒᵖ D) : (sheafificationAdjunction J D).unit.app P = toSheafify J P

@[reducible, inline]

noncomputable abbrev CategoryTheory.sheafifyMap {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) : sheafify J P ⟶ sheafify J Q

The canonical map on sheafifications induced by a morphism.

Equations

• CategoryTheory.sheafifyMap J η = ((CategoryTheory.presheafToSheaf J D).map η).val

@[simp]

theorem CategoryTheory.sheafifyMap_id {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] (P : Functor Cᵒᵖ D) : sheafifyMap J (CategoryStruct.id P) = CategoryStruct.id (sheafify J P)

@[simp]

theorem CategoryTheory.sheafifyMap_comp {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P Q R : Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) : sheafifyMap J (CategoryStruct.comp η γ) = CategoryStruct.comp (sheafifyMap J η) (sheafifyMap J γ)

@[simp]

theorem CategoryTheory.toSheafify_naturality {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) : CategoryStruct.comp η (toSheafify J Q) = CategoryStruct.comp (toSheafify J P) (sheafifyMap J η)

@[simp]

theorem CategoryTheory.toSheafify_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) {Z : Functor Cᵒᵖ D} (h : sheafify J Q ⟶ Z) : CategoryStruct.comp η (CategoryStruct.comp (toSheafify J Q) h) = CategoryStruct.comp (toSheafify J P) (CategoryStruct.comp (sheafifyMap J η) h)

@[reducible, inline]

noncomputable abbrev CategoryTheory.sheafification {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (D : Type u_1) [Category.{u_2, u_1} D] [HasWeakSheafify J D] : Functor (Functor Cᵒᵖ D) (Functor Cᵒᵖ D)

The sheafification of a presheaf P, as a functor.

Equations

• CategoryTheory.sheafification J D = (CategoryTheory.presheafToSheaf J D).comp (CategoryTheory.sheafToPresheaf J D)

theorem CategoryTheory.sheafification_obj {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (D : Type u_1) [Category.{u_2, u_1} D] [HasWeakSheafify J D] (P : Functor Cᵒᵖ D) : (sheafification J D).obj P = sheafify J P

theorem CategoryTheory.sheafification_map {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (D : Type u_1) [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) : (sheafification J D).map η = sheafifyMap J η

@[reducible, inline]

noncomputable abbrev CategoryTheory.toSheafification {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (D : Type u_1) [Category.{u_2, u_1} D] [HasWeakSheafify J D] : Functor.id (Functor Cᵒᵖ D) ⟶ sheafification J D

The canonical map from P to its sheafification, as a natural transformation.

Equations

• CategoryTheory.toSheafification J D = (CategoryTheory.sheafificationAdjunction J D).unit

theorem CategoryTheory.toSheafification_app {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (D : Type u_1) [Category.{u_2, u_1} D] [HasWeakSheafify J D] (P : Functor Cᵒᵖ D) : (toSheafification J D).app P = toSheafify J P

theorem CategoryTheory.isIso_toSheafify {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P : Functor Cᵒᵖ D} (hP : Presheaf.IsSheaf J P) : IsIso (toSheafify J P)

noncomputable def CategoryTheory.isoSheafify {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P : Functor Cᵒᵖ D} (hP : Presheaf.IsSheaf J P) : P ≅ sheafify J P

If P is a sheaf, then P is isomorphic to sheafify J P.

Equations

• CategoryTheory.isoSheafify J hP = CategoryTheory.asIso (CategoryTheory.toSheafify J P)

@[simp]

theorem CategoryTheory.isoSheafify_hom {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P : Functor Cᵒᵖ D} (hP : Presheaf.IsSheaf J P) : (isoSheafify J hP).hom = toSheafify J P

noncomputable def CategoryTheory.sheafifyLift {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) : sheafify J P ⟶ Q

Given a sheaf Q and a morphism P ⟶ Q, construct a morphism from sheafify J P to Q.

Equations

• CategoryTheory.sheafifyLift J η hQ = (((CategoryTheory.sheafificationAdjunction J D).homEquiv P { val := Q, cond := hQ }).symm η).val

@[simp]

theorem CategoryTheory.sheafificationAdjunction_counit_app_val {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] (P : Sheaf J D) : ((sheafificationAdjunction J D).counit.app P).val = sheafifyLift J (CategoryStruct.id P.val) ⋯

@[simp]

theorem CategoryTheory.toSheafify_sheafifyLift {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) : CategoryStruct.comp (toSheafify J P) (sheafifyLift J η hQ) = η

@[simp]

theorem CategoryTheory.toSheafify_sheafifyLift_assoc {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) {Z : Functor Cᵒᵖ D} (h : Q ⟶ Z) : CategoryStruct.comp (toSheafify J P) (CategoryStruct.comp (sheafifyLift J η hQ) h) = CategoryStruct.comp η h

theorem CategoryTheory.sheafifyLift_unique {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) (γ : sheafify J P ⟶ Q) : CategoryStruct.comp (toSheafify J P) γ = η → γ = sheafifyLift J η hQ

@[simp]

theorem CategoryTheory.isoSheafify_inv {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P : Functor Cᵒᵖ D} (hP : Presheaf.IsSheaf J P) : (isoSheafify J hP).inv = sheafifyLift J (CategoryStruct.id P) hP

theorem CategoryTheory.sheafify_hom_ext {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P Q : Functor Cᵒᵖ D} (η γ : sheafify J P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) (h : CategoryStruct.comp (toSheafify J P) η = CategoryStruct.comp (toSheafify J P) γ) : η = γ

@[simp]

theorem CategoryTheory.sheafifyMap_sheafifyLift {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P Q R : Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : Presheaf.IsSheaf J R) : CategoryStruct.comp (sheafifyMap J η) (sheafifyLift J γ hR) = sheafifyLift J (CategoryStruct.comp η γ) hR

@[simp]

theorem CategoryTheory.sheafifyMap_sheafifyLift_assoc {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] {P Q R : Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : Presheaf.IsSheaf J R) {Z : Functor Cᵒᵖ D} (h : R ⟶ Z) : CategoryStruct.comp (sheafifyMap J η) (CategoryStruct.comp (sheafifyLift J γ hR) h) = CategoryStruct.comp (sheafifyLift J (CategoryStruct.comp η γ) hR) h

noncomputable def CategoryTheory.sheafificationIso {C : Type u₁} [Category.{v₁, u₁} C] {J : GrothendieckTopology C} {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] (P : Sheaf J D) : P ≅ (presheafToSheaf J D).obj P.val

A sheaf P is isomorphic to its own sheafification.

Equations

• CategoryTheory.sheafificationIso P = { hom := { val := (CategoryTheory.isoSheafify J ⋯).hom }, inv := { val := (CategoryTheory.isoSheafify J ⋯).inv }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.sheafificationIso_hom_val {C : Type u₁} [Category.{v₁, u₁} C] {J : GrothendieckTopology C} {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] (P : Sheaf J D) : (sheafificationIso P).hom.val = (isoSheafify J ⋯).hom

@[simp]

theorem CategoryTheory.sheafificationIso_inv_val {C : Type u₁} [Category.{v₁, u₁} C] {J : GrothendieckTopology C} {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] (P : Sheaf J D) : (sheafificationIso P).inv.val = (isoSheafify J ⋯).inv

instance CategoryTheory.isIso_sheafificationAdjunction_counit {C : Type u₁} [Category.{v₁, u₁} C] {J : GrothendieckTopology C} {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] (P : Sheaf J D) : IsIso ((sheafificationAdjunction J D).counit.app P)

instance CategoryTheory.sheafification_reflective {C : Type u₁} [Category.{v₁, u₁} C] {J : GrothendieckTopology C} {D : Type u_1} [Category.{u_2, u_1} D] [HasWeakSheafify J D] : IsIso (sheafificationAdjunction J D).counit

noncomputable def CategoryTheory.sheafificationNatIso {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (D : Type u_1) [Category.{u_2, u_1} D] [HasWeakSheafify J D] : Functor.id (Sheaf J D) ≅ (sheafToPresheaf J D).comp (presheafToSheaf J D)

The natural isomorphism 𝟭 (Sheaf J D) ≅ sheafToPresheaf J D ⋙ presheafToSheaf J D.

Equations

• CategoryTheory.sheafificationNatIso J D = CategoryTheory.NatIso.ofComponents (fun (P : CategoryTheory.Sheaf J D) => CategoryTheory.sheafificationIso P) ⋯

@[simp]

theorem CategoryTheory.sheafificationNatIso_inv_app_val {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (D : Type u_1) [Category.{u_2, u_1} D] [HasWeakSheafify J D] (X : Sheaf J D) : ((sheafificationNatIso J D).inv.app X).val = sheafifyLift J (CategoryStruct.id X.val) ⋯

@[simp]

theorem CategoryTheory.sheafificationNatIso_hom_app_val {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (D : Type u_1) [Category.{u_2, u_1} D] [HasWeakSheafify J D] (X : Sheaf J D) : ((sheafificationNatIso J D).hom.app X).val = toSheafify J X.val