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.
@[reducible, inline]
abbrev
CategoryTheory.HasWeakSheafify
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
:
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
Instances For
class
CategoryTheory.HasSheafify
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
:
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 : Nonempty (Limits.PreservesFiniteLimits (sheafToPresheaf J A).leftAdjoint)
Instances
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]
:
The sheafification functor, left adjoint to the inclusion.
Equations
- CategoryTheory.presheafToSheaf J A = (CategoryTheory.sheafToPresheaf J A).leftAdjoint
Instances For
instance
CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
[HasSheafify 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
Instances For
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]
:
@[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)
:
The sheafification of a presheaf P.
Equations
- CategoryTheory.sheafify J P = ((CategoryTheory.presheafToSheaf J D).obj P).val
Instances For
@[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)
:
The canonical map from P to its sheafification.
Equations
- CategoryTheory.toSheafify J P = (CategoryTheory.sheafificationAdjunction J D).unit.app P
Instances For
@[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)
:
The canonical map on sheafifications induced by a morphism.
Equations
- CategoryTheory.sheafifyMap J η = ((CategoryTheory.presheafToSheaf J D).map η).val
Instances For
@[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]
:
The sheafification of a presheaf P, as a functor.
Equations
- CategoryTheory.sheafification J D = (CategoryTheory.presheafToSheaf J D).comp (CategoryTheory.sheafToPresheaf J D)
Instances For
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
Instances For
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)
:
If P is a sheaf, then P is isomorphic to sheafify J P.
Equations
Instances For
@[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)
:
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
Instances For
@[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 := ⋯ }
Instances For
@[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) ⋯
Instances For
@[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