A sheaf is the right Kan extension of its restriction to a dense subsite

Let G : C ⥤ D exhibit (C, J) as a dense subsite of (D, K), and let A be a category with the limits indexed by the comma categories StructuredArrow X G.op. Mathlib proves that restriction along G is an equivalence Sheaf K A ≌ Sheaf J A (the comparison lemma), with inverse the right Kan extension G.op.ran. This file records the consequence for a single sheaf ℱ on D: the unit ℱ ⟶ G.op.ran.obj (G.op ⋙ ℱ) of the Kan-extension adjunction is an isomorphism, so ℱ itself, with the identity as counit, is the pointwise right Kan extension of its restriction G.op ⋙ ℱ along G.op. In other words, for every object X of D the value ℱ.obj (op X) is the limit of the values ℱ.obj (op (G.obj Y)) over the arrows G.obj Y ⟶ X, with the restriction maps of ℱ as the legs.

For the inclusion of a basis of a topological space into its opens, this says that a sheaf is determined on every open V by its values on the basic opens contained in V: it is the adaptedness of TopCat.Presheaf.IsAdapted for every sheaf.

Main results

• CategoryTheory.Functor.IsDenseSubsite.isIso_ranAdjunction_unit_app: the unit of the Kan-extension adjunction is an isomorphism at a sheaf.
• CategoryTheory.Functor.IsDenseSubsite.isRightKanExtension: a sheaf, with the identity as counit, is a right Kan extension of its restriction to a dense subsite.
• CategoryTheory.Functor.IsDenseSubsite.isPointwiseRightKanExtension: a sheaf is the pointwise right Kan extension of its restriction to a dense subsite.

References

• P. T. Johnstone, Sketches of an Elephant, C2.2, the comparison lemma, which Mathlib formalizes as CategoryTheory.Functor.IsDenseSubsite.sheafEquiv.

theorem CategoryTheory.Functor.IsDenseSubsite.isIso_ranAdjunction_unit_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (J : GrothendieckTopology C) (K : GrothendieckTopology D) {A : Type w} [Category.{w', w} A] [∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A] [IsDenseSubsite J K G] (ℱ : Sheaf K A) : IsIso ((G.op.ranAdjunction A).unit.app ℱ.obj)

The unit of the Kan-extension adjunction is an isomorphism at a sheaf. For a sheaf ℱ on a site with dense subsite G, the canonical map ℱ ⟶ G.op.ran.obj (G.op ⋙ ℱ) is an isomorphism: it is the unit of the sheaf equivalence of the comparison lemma, read in presheaves.

theorem CategoryTheory.Functor.IsDenseSubsite.isRightKanExtension {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (J : GrothendieckTopology C) (K : GrothendieckTopology D) {A : Type w} [Category.{w', w} A] [∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A] [IsDenseSubsite J K G] (ℱ : Sheaf K A) : ℱ.obj.IsRightKanExtension (CategoryStruct.id (G.op.comp ℱ.obj))

A sheaf ℱ, with the identity as counit, is a right Kan extension of its restriction G.op ⋙ ℱ along G.op.

noncomputable def CategoryTheory.Functor.IsDenseSubsite.isPointwiseRightKanExtension {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (J : GrothendieckTopology C) (K : GrothendieckTopology D) {A : Type w} [Category.{w', w} A] [∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A] [IsDenseSubsite J K G] (ℱ : Sheaf K A) : (RightExtension.mk ℱ.obj (CategoryStruct.id (G.op.comp ℱ.obj))).IsPointwiseRightKanExtension

A sheaf is the pointwise right Kan extension of its restriction to a dense subsite. For every object X of D, the restriction maps of ℱ exhibit ℱ.obj (op X) as the limit of the values ℱ.obj (op (G.obj Y)) over the arrows G.obj Y ⟶ X.

Equations

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