Documentation

Mathlib.CategoryTheory.Sites.Sheafification

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]

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

Equations

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.

Instances
Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]

The sheafification of a presheaf P.

Equations
@[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
@[reducible, inline]

The sheafification of a presheaf P, as a functor.

Equations
@[reducible, inline]

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

Equations

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

Equations
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
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

A sheaf P is isomorphic to its own sheafification.

Equations