Cocontinuous functors between sites. #
We define cocontinuous functors between sites as functors that pull covering sieves back to covering sieves. This concept is also known as cover-lifting or cover-reflecting functors. We use the original terminology and definition of SGA 4 III 2.1. However, the notion of cocontinuous functor should not be confused with the general definition of cocontinuous functors between categories as functors preserving small colimits.
Main definitions #
CategoryTheory.Functor.IsCocontinuous: a functor between sites is cocontinuous if it pulls back covering sieves to covering sievesCategoryTheory.Functor.sheafPushforwardCocontinuous: A cocontinuous functorG : (C, J) ⥤ (D, K)induces a functorSheaf J A ⥤ Sheaf K A.
Main results #
CategoryTheory.ran_isSheaf_of_isCocontinuous: IfG : C ⥤ Dis cocontinuous, thenG.op.ran(ₚu) as a functor(Cᵒᵖ ⥤ A) ⥤ (Dᵒᵖ ⥤ A)of presheaves maps sheaves to sheaves.CategoryTheory.Functor.sheafAdjunctionCocontinuous: IfG : (C, J) ⥤ (D, K)is cocontinuous and continuous, thenG.sheafPushforwardContinuous A J KandG.sheafPushforwardCocontinuous A J Kare adjoint.
References #
- [Elephant]: Sketches of an Elephant, P. T. Johnstone: C2.3.
- [S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic][MM92]
- https://stacks.math.columbia.edu/tag/00XI
class
CategoryTheory.Functor.IsCocontinuous
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_5, u_2} D]
(G : CategoryTheory.Functor C D)
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
:
A functor G : (C, J) ⥤ (D, K) between sites is called cocontinuous (SGA 4 III 2.1)
if for all covering sieves R in D, R.pullback G is a covering sieve in C.
- cover_lift : ∀ {U : C} {S : CategoryTheory.Sieve (G.obj U)}, S ∈ K.sieves (G.obj U) → CategoryTheory.Sieve.functorPullback G S ∈ J.sieves U
Instances
theorem
CategoryTheory.Functor.IsCocontinuous.cover_lift
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_5, u_2} D]
{G : CategoryTheory.Functor C D}
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
[self : G.IsCocontinuous J K]
{U : C}
{S : CategoryTheory.Sieve (G.obj U)}
:
S ∈ K.sieves (G.obj U) → CategoryTheory.Sieve.functorPullback G S ∈ J.sieves U
theorem
CategoryTheory.Functor.cover_lift
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_5, u_2} D]
(G : CategoryTheory.Functor C D)
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[G.IsCocontinuous J K]
{U : C}
{S : CategoryTheory.Sieve (G.obj U)}
(hS : S ∈ K.sieves (G.obj U))
:
CategoryTheory.Sieve.functorPullback G S ∈ J.sieves U
instance
CategoryTheory.isCocontinuous_id
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
(J : CategoryTheory.GrothendieckTopology C)
:
(CategoryTheory.Functor.id C).IsCocontinuous J J
The identity functor on a site is cocontinuous.
Equations
- ⋯ = ⋯
theorem
CategoryTheory.isCocontinuous_comp
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_5, u_2} D]
{E : Type u_3}
[CategoryTheory.Category.{u_6, u_3} E]
(G : CategoryTheory.Functor C D)
(G' : CategoryTheory.Functor D E)
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
{L : CategoryTheory.GrothendieckTopology E}
[G.IsCocontinuous J K]
[G'.IsCocontinuous K L]
:
(G.comp G').IsCocontinuous J L
The composition of two cocontinuous functors is cocontinuous.
We will now prove that G.op.ran : (Cᵒᵖ ⥤ A) ⥤ (Dᵒᵖ ⥤ A) maps sheaves
to sheaves when G : C ⥤ D is a cocontinuous functor.
We do not follow the proofs in SGA 4 III 2.2 or https://stacks.math.columbia.edu/tag/00XK.
Instead, we verify as directly as possible that if F : Cᵒᵖ ⥤ A is a sheaf,
then G.op.ran.obj F is a sheaf. in order to do this, we use the "multifork"
characterization of sheaves which involves limits in the category A.
As G.op.ran.obj F is the chosen right Kan extension of F along G.op : Cᵒᵖ ⥤ Dᵒᵖ,
we actually verify that any pointwise right Kan extension of F along G.op is a sheaf.
def
CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
{G : CategoryTheory.Functor C D}
{A : Type w}
[CategoryTheory.Category.{w', w} A]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
[G.IsCocontinuous J K]
{F : CategoryTheory.Functor Cᵒᵖ A}
(hF : CategoryTheory.Presheaf.IsSheaf J F)
{R : CategoryTheory.Functor Dᵒᵖ A}
(α : G.op.comp R ⟶ F)
{X : D}
{S : K.Cover X}
(s : CategoryTheory.Limits.Multifork (S.index R))
{Y : C}
(f : G.obj Y ⟶ X)
:
s.pt ⟶ F.obj (Opposite.op Y)
Auxiliary definition for lift.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
{G : CategoryTheory.Functor C D}
{A : Type w}
[CategoryTheory.Category.{w', w} A]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
[G.IsCocontinuous J K]
{F : CategoryTheory.Functor Cᵒᵖ A}
(hF : CategoryTheory.Presheaf.IsSheaf J F)
{R : CategoryTheory.Functor Dᵒᵖ A}
(α : G.op.comp R ⟶ F)
{X : D}
{S : K.Cover X}
(s : CategoryTheory.Limits.Multifork (S.index R))
{Y : C}
(f : G.obj Y ⟶ X)
{W : C}
(g : W ⟶ Y)
(i : S.Arrow)
(h : G.obj W ⟶ i.Y)
(w : CategoryTheory.CategoryStruct.comp h i.f = CategoryTheory.CategoryStruct.comp (G.map g) f)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f) (F.map g.op) = CategoryTheory.CategoryStruct.comp (s.ι i) (CategoryTheory.CategoryStruct.comp (R.map h.op) (α.app (Opposite.op W)))
theorem
CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
{G : CategoryTheory.Functor C D}
{A : Type w}
[CategoryTheory.Category.{w', w} A]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
[G.IsCocontinuous J K]
{F : CategoryTheory.Functor Cᵒᵖ A}
(hF : CategoryTheory.Presheaf.IsSheaf J F)
{R : CategoryTheory.Functor Dᵒᵖ A}
(α : G.op.comp R ⟶ F)
{X : D}
{S : K.Cover X}
(s : CategoryTheory.Limits.Multifork (S.index R))
{Y : C}
{Y' : C}
(f : G.obj Y ⟶ X)
(f' : G.obj Y' ⟶ X)
{W : C}
(a : W ⟶ Y)
(b : W ⟶ Y')
(w : CategoryTheory.CategoryStruct.comp (G.map a) f = CategoryTheory.CategoryStruct.comp (G.map b) f')
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f) (F.map a.op) = CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f') (F.map b.op)
def
CategoryTheory.RanIsSheafOfIsCocontinuous.lift
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
{G : CategoryTheory.Functor C D}
{A : Type w}
[CategoryTheory.Category.{w', w} A]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
[G.IsCocontinuous J K]
{F : CategoryTheory.Functor Cᵒᵖ A}
(hF : CategoryTheory.Presheaf.IsSheaf J F)
{R : CategoryTheory.Functor Dᵒᵖ A}
{α : G.op.comp R ⟶ F}
(hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension)
{X : D}
{S : K.Cover X}
(s : CategoryTheory.Limits.Multifork (S.index R))
:
s.pt ⟶ R.obj (Opposite.op X)
Auxiliary definition for isLimitMultifork
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.RanIsSheafOfIsCocontinuous.fac'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
{G : CategoryTheory.Functor C D}
{A : Type w}
[CategoryTheory.Category.{w', w} A]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
[G.IsCocontinuous J K]
{F : CategoryTheory.Functor Cᵒᵖ A}
(hF : CategoryTheory.Presheaf.IsSheaf J F)
{R : CategoryTheory.Functor Dᵒᵖ A}
{α : G.op.comp R ⟶ F}
(hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension)
{X : D}
{S : K.Cover X}
(s : CategoryTheory.Limits.Multifork (S.index R))
(j : CategoryTheory.StructuredArrow (Opposite.op X) G.op)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s)
(CategoryTheory.CategoryStruct.comp (R.map j.hom) (α.app j.right)) = CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s j.hom.unop
@[simp]
theorem
CategoryTheory.RanIsSheafOfIsCocontinuous.fac_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
{G : CategoryTheory.Functor C D}
{A : Type w}
[CategoryTheory.Category.{w', w} A]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
[G.IsCocontinuous J K]
{F : CategoryTheory.Functor Cᵒᵖ A}
(hF : CategoryTheory.Presheaf.IsSheaf J F)
{R : CategoryTheory.Functor Dᵒᵖ A}
{α : G.op.comp R ⟶ F}
(hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension)
{X : D}
{S : K.Cover X}
(s : CategoryTheory.Limits.Multifork (S.index R))
(i : S.Arrow)
{Z : A}
(h : R.obj (Opposite.op i.Y) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s)
(CategoryTheory.CategoryStruct.comp (R.map i.f.op) h) = CategoryTheory.CategoryStruct.comp (s.ι i) h
@[simp]
theorem
CategoryTheory.RanIsSheafOfIsCocontinuous.fac
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
{G : CategoryTheory.Functor C D}
{A : Type w}
[CategoryTheory.Category.{w', w} A]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
[G.IsCocontinuous J K]
{F : CategoryTheory.Functor Cᵒᵖ A}
(hF : CategoryTheory.Presheaf.IsSheaf J F)
{R : CategoryTheory.Functor Dᵒᵖ A}
{α : G.op.comp R ⟶ F}
(hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension)
{X : D}
{S : K.Cover X}
(s : CategoryTheory.Limits.Multifork (S.index R))
(i : S.Arrow)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s) (R.map i.f.op) = s.ι i
theorem
CategoryTheory.RanIsSheafOfIsCocontinuous.hom_ext
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
{G : CategoryTheory.Functor C D}
{A : Type w}
[CategoryTheory.Category.{w', w} A]
{J : CategoryTheory.GrothendieckTopology C}
(K : CategoryTheory.GrothendieckTopology D)
[G.IsCocontinuous J K]
{F : CategoryTheory.Functor Cᵒᵖ A}
(hF : CategoryTheory.Presheaf.IsSheaf J F)
{R : CategoryTheory.Functor Dᵒᵖ A}
{α : G.op.comp R ⟶ F}
(hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension)
{X : D}
{S : K.Cover X}
{W : A}
{f : W ⟶ R.obj (Opposite.op X)}
{g : W ⟶ R.obj (Opposite.op X)}
(h : ∀ (i : S.Arrow),
CategoryTheory.CategoryStruct.comp f (R.map i.f.op) = CategoryTheory.CategoryStruct.comp g (R.map i.f.op))
:
f = g
def
CategoryTheory.RanIsSheafOfIsCocontinuous.isLimitMultifork
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
{G : CategoryTheory.Functor C D}
{A : Type w}
[CategoryTheory.Category.{w', w} A]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
[G.IsCocontinuous J K]
{F : CategoryTheory.Functor Cᵒᵖ A}
(hF : CategoryTheory.Presheaf.IsSheaf J F)
{R : CategoryTheory.Functor Dᵒᵖ A}
{α : G.op.comp R ⟶ F}
(hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension)
{X : D}
(S : K.Cover X)
:
CategoryTheory.Limits.IsLimit (S.multifork R)
Auxiliary definition for ran_isSheaf_of_isCocontinuous: if G : C ⥤ D is a
cocontinuous functor,
Equations
- CategoryTheory.RanIsSheafOfIsCocontinuous.isLimitMultifork hF hR S = CategoryTheory.Limits.Multifork.IsLimit.mk (S.multifork R) (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR) ⋯ ⋯
Instances For
theorem
CategoryTheory.ran_isSheaf_of_isCocontinuous
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(G : CategoryTheory.Functor C D)
{A : Type w}
[CategoryTheory.Category.{w', w} A]
{J : CategoryTheory.GrothendieckTopology C}
(K : CategoryTheory.GrothendieckTopology D)
[G.IsCocontinuous J K]
[∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F]
(ℱ : CategoryTheory.Sheaf J A)
:
CategoryTheory.Presheaf.IsSheaf K (G.op.ran.obj ℱ.val)
If G is cocontinuous, then G.op.ran pushes sheaves to sheaves.
This is SGA 4 III 2.2. An alternative reference is
https://stacks.math.columbia.edu/tag/00XK (where results
are obtained under the additional assumption that
C and D have pullbacks).
def
CategoryTheory.Functor.sheafPushforwardCocontinuous
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(G : CategoryTheory.Functor C D)
(A : Type w)
[CategoryTheory.Category.{w', w} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[G.IsCocontinuous J K]
[∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F]
:
A cocontinuous functor induces a pushforward functor on categories of sheaves.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_hom
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(G : CategoryTheory.Functor C D)
(A : Type w)
[CategoryTheory.Category.{w', w} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[G.IsCocontinuous J K]
[∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F]
:
(G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).hom = CategoryTheory.CategoryStruct.id ((G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A))
@[simp]
theorem
CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_inv
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(G : CategoryTheory.Functor C D)
(A : Type w)
[CategoryTheory.Category.{w', w} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[G.IsCocontinuous J K]
[∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F]
:
(G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).inv = CategoryTheory.CategoryStruct.id ((G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A))
def
CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(G : CategoryTheory.Functor C D)
(A : Type w)
[CategoryTheory.Category.{w', w} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[G.IsCocontinuous J K]
[∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F]
:
(G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A) ≅ (CategoryTheory.sheafToPresheaf J A).comp G.op.ran
G.sheafPushforwardCocontinuous A J K : Sheaf J A ⥤ Sheaf K A is induced
by the right Kan extension functor G.op.ran on presheaves.
Equations
- G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K = CategoryTheory.Iso.refl ((G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A))
Instances For
noncomputable def
CategoryTheory.Functor.sheafAdjunctionCocontinuous
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(G : CategoryTheory.Functor C D)
(A : Type w)
[CategoryTheory.Category.{w', w} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F]
[G.IsCocontinuous J K]
[G.IsContinuous J K]
:
G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K
Given a functor between sites that is continuous and cocontinuous,
the pushforward for the continuous functor G is left adjoint to
the pushforward for the cocontinuous functor G.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_val
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
(G : CategoryTheory.Functor C D)
(A : Type w)
[CategoryTheory.Category.{w', w} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F]
[G.IsCocontinuous J K]
[G.IsContinuous J K]
(F : CategoryTheory.Sheaf K A)
:
((G.sheafAdjunctionCocontinuous A J K).unit.app F).val = (G.op.ranAdjunction A).unit.app F.val
theorem
CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_val
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(G : CategoryTheory.Functor C D)
(A : Type w)
[CategoryTheory.Category.{w', w} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F]
[G.IsCocontinuous J K]
[G.IsContinuous J K]
(F : CategoryTheory.Sheaf J A)
:
((G.sheafAdjunctionCocontinuous A J K).counit.app F).val = (G.op.ranAdjunction A).counit.app F.val
theorem
CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_val
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
(G : CategoryTheory.Functor C D)
(A : Type w)
[CategoryTheory.Category.{w', w} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F]
[G.IsCocontinuous J K]
[G.IsContinuous J K]
{F : CategoryTheory.Sheaf K A}
{H : CategoryTheory.Sheaf J A}
(f : (G.sheafPushforwardContinuous A J K).obj F ⟶ H)
:
(((G.sheafAdjunctionCocontinuous A J K).homEquiv F H) f).val = ((G.op.ranAdjunction A).homEquiv F.val H.val) f.val
def
CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(G : CategoryTheory.Functor C D)
(A : Type w)
[CategoryTheory.Category.{w', w} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F]
[CategoryTheory.HasWeakSheafify J A]
[CategoryTheory.HasWeakSheafify K A]
[G.IsCocontinuous J K]
[G.IsContinuous J K]
:
((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).comp (CategoryTheory.presheafToSheaf J A) ≅ (CategoryTheory.presheafToSheaf K A).comp (G.sheafPushforwardContinuous A J K)
The natural isomorphism exhibiting compatibility between pushforward and sheafification.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Functor.toSheafify_pullbackSheafificationCompatibility
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
(G : CategoryTheory.Functor C D)
(A : Type w)
[CategoryTheory.Category.{w', w} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F]
[CategoryTheory.HasWeakSheafify J A]
[CategoryTheory.HasWeakSheafify K A]
[G.IsCocontinuous J K]
[G.IsContinuous J K]
(F : CategoryTheory.Functor Dᵒᵖ A)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (G.op.comp F))
((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val = CategoryTheory.whiskerLeft G.op (CategoryTheory.toSheafify K F)
@[simp]
theorem
CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
(G : CategoryTheory.Functor C D)
(A : Type w)
[CategoryTheory.Category.{w', w} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F]
[CategoryTheory.HasWeakSheafify J A]
[CategoryTheory.HasWeakSheafify K A]
[G.IsCocontinuous J K]
[G.IsContinuous J K]
(F : CategoryTheory.Functor Dᵒᵖ A)
:
((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val = CategoryTheory.sheafifyLift J (CategoryTheory.whiskerLeft G.op (CategoryTheory.toSheafify K F)) ⋯