Cover-preserving functors between sites. #
We define cover-preserving functors between sites as functors that push covering sieves to
covering sieves. A cover-preserving and compatible-preserving functor G : C ⥤ D then pulls
sheaves on D back to sheaves on C via G.op ⋙ -.
Main definitions #
category_theory.cover_preserving: a functor between sites is cover-preserving if it pushes covering sieves to covering sievescategory_theory.compatible_preserving: a functor between sites is compatible-preserving if it pushes compatible families of elements to compatible families.category_theory.pullback_sheaf: the pullback of a sheaf along a cover-preserving and compatible-preserving functor.category_theory.sites.pullback: the induced functorSheaf K A ⥤ Sheaf J Afor a cover-preserving and compatible-preserving functorG : (C, J) ⥤ (D, K).category_theory.sites.pushforward: the induced functorSheaf J A ⥤ Sheaf K Afor a cover-preserving and compatible-preserving functorG : (C, J) ⥤ (D, K).category_theory.sites.pushforward: the induced functorSheaf J A ⥤ Sheaf K Afor a cover-preserving and compatible-preserving functorG : (C, J) ⥤ (D, K).
Main results #
category_theory.sites.whiskering_left_is_sheaf_of_cover_preserving: IfG : C ⥤ Dis cover-preserving and compatible-preserving, thenG ⋙ -(uᵖ) as a functor(Dᵒᵖ ⥤ A) ⥤ (Cᵒᵖ ⥤ A)of presheaves maps sheaves to sheaves.
References #
- [Joh02]: Sketches of an Elephant, P. T. Johnstone: C2.3.
- https://stacks.math.columbia.edu/tag/00WW
@[nolint]
structure
category_theory.cover_preserving
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(J : category_theory.grothendieck_topology C)
(K : category_theory.grothendieck_topology D)
(G : C ⥤ D) :
Prop
- cover_preserve : ∀ {U : C} {S : category_theory.sieve U}, S ∈ ⇑J U → category_theory.sieve.functor_pushforward G S ∈ ⇑K (G.obj U)
A functor G : (C, J) ⥤ (D, K) between sites is cover-preserving
if for all covering sieves R in C, R.pushforward_functor G is a covering sieve in D.
theorem
category_theory.id_cover_preserving
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C) :
category_theory.cover_preserving J J (𝟭 C)
The identity functor on a site is cover-preserving.
theorem
category_theory.cover_preserving.comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{A : Type u₃}
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
(K : category_theory.grothendieck_topology D)
{L : category_theory.grothendieck_topology A}
{F : C ⥤ D}
(hF : category_theory.cover_preserving J K F)
{G : D ⥤ A}
(hG : category_theory.cover_preserving K L G) :
category_theory.cover_preserving J L (F ⋙ G)
The composition of two cover-preserving functors is cover-preserving.
@[nolint]
structure
category_theory.compatible_preserving
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(K : category_theory.grothendieck_topology D)
(G : C ⥤ D) :
Prop
- compatible : ∀ (ℱ : category_theory.SheafOfTypes K) {Z : C} {T : category_theory.presieve Z} {x : category_theory.presieve.family_of_elements (G.op ⋙ ℱ.val) T}, x.compatible → ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.obj Y₁) (f₂ : X ⟶ G.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁) (hg₂ : T g₂), f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ → ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
A functor G : (C, J) ⥤ (D, K) between sites is called compatible preserving if for each
compatible family of elements at C and valued in G.op ⋙ ℱ, and each commuting diagram
f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂, x g₁ and x g₂ coincide when restricted via fᵢ.
This is actually stronger than merely preserving compatible families because of the definition of
functor_pushforward used.
theorem
category_theory.presieve.family_of_elements.compatible.functor_pushforward
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{K : category_theory.grothendieck_topology D}
{G : C ⥤ D}
(hG : category_theory.compatible_preserving K G)
(ℱ : category_theory.SheafOfTypes K)
{Z : C}
{T : category_theory.presieve Z}
{x : category_theory.presieve.family_of_elements (G.op ⋙ ℱ.val) T}
(h : x.compatible) :
compatible_preserving functors indeed preserve compatible families.
@[simp]
theorem
category_theory.compatible_preserving.apply_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{K : category_theory.grothendieck_topology D}
{G : C ⥤ D}
(hG : category_theory.compatible_preserving K G)
(ℱ : category_theory.SheafOfTypes K)
{Z : C}
{T : category_theory.presieve Z}
{x : category_theory.presieve.family_of_elements (G.op ⋙ ℱ.val) T}
(h : x.compatible)
{Y : C}
{f : Y ⟶ Z}
(hf : T f) :
category_theory.presieve.family_of_elements.functor_pushforward G x (G.map f) _ = x f hf
theorem
category_theory.compatible_preserving_of_flat
{C : Type u₁}
[category_theory.category C]
{D : Type u₁}
[category_theory.category D]
(K : category_theory.grothendieck_topology D)
(G : C ⥤ D)
[category_theory.representably_flat G] :
theorem
category_theory.pullback_is_sheaf_of_cover_preserving
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{A : Type u₃}
[category_theory.category A]
{J : category_theory.grothendieck_topology C}
{K : category_theory.grothendieck_topology D}
{G : C ⥤ D}
(hG₁ : category_theory.compatible_preserving K G)
(hG₂ : category_theory.cover_preserving J K G)
(ℱ : category_theory.Sheaf K A) :
category_theory.presheaf.is_sheaf J (G.op ⋙ ℱ.val)
If G is cover-preserving and compatible-preserving,
then G.op ⋙ _ pulls sheaves back to sheaves.
This result is basically https://stacks.math.columbia.edu/tag/00WW.
def
category_theory.pullback_sheaf
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{A : Type u₃}
[category_theory.category A]
{J : category_theory.grothendieck_topology C}
{K : category_theory.grothendieck_topology D}
{G : C ⥤ D}
(hG₁ : category_theory.compatible_preserving K G)
(hG₂ : category_theory.cover_preserving J K G)
(ℱ : category_theory.Sheaf K A) :
The pullback of a sheaf along a cover-preserving and compatible-preserving functor.
@[simp]
theorem
category_theory.sites.pullback_obj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(A : Type u₃)
[category_theory.category A]
{J : category_theory.grothendieck_topology C}
{K : category_theory.grothendieck_topology D}
{G : C ⥤ D}
(hG₁ : category_theory.compatible_preserving K G)
(hG₂ : category_theory.cover_preserving J K G)
(ℱ : category_theory.Sheaf K A) :
(category_theory.sites.pullback A hG₁ hG₂).obj ℱ = category_theory.pullback_sheaf hG₁ hG₂ ℱ
@[simp]
theorem
category_theory.sites.pullback_map_val
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(A : Type u₃)
[category_theory.category A]
{J : category_theory.grothendieck_topology C}
{K : category_theory.grothendieck_topology D}
{G : C ⥤ D}
(hG₁ : category_theory.compatible_preserving K G)
(hG₂ : category_theory.cover_preserving J K G)
(_x _x_1 : category_theory.Sheaf K A)
(f : _x ⟶ _x_1) :
def
category_theory.sites.pullback
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(A : Type u₃)
[category_theory.category A]
{J : category_theory.grothendieck_topology C}
{K : category_theory.grothendieck_topology D}
{G : C ⥤ D}
(hG₁ : category_theory.compatible_preserving K G)
(hG₂ : category_theory.cover_preserving J K G) :
The induced functor from Sheaf K A ⥤ Sheaf J A given by G.op ⋙ _
if G is cover-preserving and compatible-preserving.
Equations
- category_theory.sites.pullback A hG₁ hG₂ = {obj := λ (ℱ : category_theory.Sheaf K A), category_theory.pullback_sheaf hG₁ hG₂ ℱ, map := λ (_x _x_1 : category_theory.Sheaf K A) (f : _x ⟶ _x_1), {val := ((category_theory.whiskering_left Cᵒᵖ Dᵒᵖ A).obj G.op).map f.val}, map_id' := _, map_comp' := _}
Instances for category_theory.sites.pullback
@[protected, instance]
noncomputable
def
category_theory.Sheaf_to_presheaf.creates_limits
{C : Type v₁}
[category_theory.small_category C]
(A : Type u₂)
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
[category_theory.limits.has_limits A] :
@[protected, instance]
def
category_theory.grothendieck_topology.cover.is_cofiltered
{C : Type v₁}
[category_theory.small_category C]
(J : category_theory.grothendieck_topology C)
{X : C} :
@[simp]
theorem
category_theory.sites.pushforward_map_val_app
{C : Type v₁}
[category_theory.small_category C]
{D : Type v₁}
[category_theory.small_category D]
(A : Type u₂)
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
(K : category_theory.grothendieck_topology D)
[category_theory.concrete_category A]
[category_theory.limits.preserves_limits (category_theory.forget A)]
[category_theory.limits.has_colimits A]
[category_theory.limits.has_limits A]
[category_theory.limits.preserves_filtered_colimits (category_theory.forget A)]
[category_theory.reflects_isomorphisms (category_theory.forget A)]
(G : C ⥤ D)
(_x _x_1 : category_theory.Sheaf J A)
(f : _x ⟶ _x_1)
(X : Dᵒᵖ) :
((category_theory.sites.pushforward A J K G).map f).val.app X = category_theory.limits.colim_map (K.diagram_nat_trans (K.plus_map ((category_theory.Lan G.op).map f.val)) (opposite.unop X))
noncomputable
def
category_theory.sites.pushforward
{C : Type v₁}
[category_theory.small_category C]
{D : Type v₁}
[category_theory.small_category D]
(A : Type u₂)
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
(K : category_theory.grothendieck_topology D)
[category_theory.concrete_category A]
[category_theory.limits.preserves_limits (category_theory.forget A)]
[category_theory.limits.has_colimits A]
[category_theory.limits.has_limits A]
[category_theory.limits.preserves_filtered_colimits (category_theory.forget A)]
[category_theory.reflects_isomorphisms (category_theory.forget A)]
(G : C ⥤ D) :
The pushforward functor Sheaf J A ⥤ Sheaf K A associated to a functor G : C ⥤ D in the
same direction as G.
Equations
Instances for category_theory.sites.pushforward
@[simp]
theorem
category_theory.sites.pushforward_obj_val_obj
{C : Type v₁}
[category_theory.small_category C]
{D : Type v₁}
[category_theory.small_category D]
(A : Type u₂)
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
(K : category_theory.grothendieck_topology D)
[category_theory.concrete_category A]
[category_theory.limits.preserves_limits (category_theory.forget A)]
[category_theory.limits.has_colimits A]
[category_theory.limits.has_limits A]
[category_theory.limits.preserves_filtered_colimits (category_theory.forget A)]
[category_theory.reflects_isomorphisms (category_theory.forget A)]
(G : C ⥤ D)
(X : category_theory.Sheaf J A)
(X_1 : Dᵒᵖ) :
((category_theory.sites.pushforward A J K G).obj X).val.obj X_1 = category_theory.limits.colimit (K.diagram (K.plus_obj ((category_theory.Lan G.op).obj X.val)) (opposite.unop X_1))
@[simp]
theorem
category_theory.sites.pushforward_obj_val_map
{C : Type v₁}
[category_theory.small_category C]
{D : Type v₁}
[category_theory.small_category D]
(A : Type u₂)
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
(K : category_theory.grothendieck_topology D)
[category_theory.concrete_category A]
[category_theory.limits.preserves_limits (category_theory.forget A)]
[category_theory.limits.has_colimits A]
[category_theory.limits.has_limits A]
[category_theory.limits.preserves_filtered_colimits (category_theory.forget A)]
[category_theory.reflects_isomorphisms (category_theory.forget A)]
(G : C ⥤ D)
(X : category_theory.Sheaf J A)
(X_1 Y : Dᵒᵖ)
(f : X_1 ⟶ Y) :
((category_theory.sites.pushforward A J K G).obj X).val.map f = category_theory.limits.colim_map (K.diagram_pullback (K.plus_obj ((category_theory.Lan G.op).obj X.val)) f.unop) ≫ category_theory.limits.colimit.pre (K.diagram (K.plus_obj ((category_theory.Lan G.op).obj X.val)) (opposite.unop Y)) (K.pullback f.unop).op
@[protected, instance]
noncomputable
def
category_theory.sites.pushforward.limits.preserves_finite_limits
{C : Type v₁}
[category_theory.small_category C]
{D : Type v₁}
[category_theory.small_category D]
(A : Type u₂)
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
(K : category_theory.grothendieck_topology D)
[category_theory.concrete_category A]
[category_theory.limits.preserves_limits (category_theory.forget A)]
[category_theory.limits.has_colimits A]
[category_theory.limits.has_limits A]
[category_theory.limits.preserves_filtered_colimits (category_theory.forget A)]
[category_theory.reflects_isomorphisms (category_theory.forget A)]
(G : C ⥤ D)
[category_theory.representably_flat G] :
noncomputable
def
category_theory.sites.pullback_pushforward_adjunction
{C : Type v₁}
[category_theory.small_category C]
{D : Type v₁}
[category_theory.small_category D]
(A : Type u₂)
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
(K : category_theory.grothendieck_topology D)
[category_theory.concrete_category A]
[category_theory.limits.preserves_limits (category_theory.forget A)]
[category_theory.limits.has_colimits A]
[category_theory.limits.has_limits A]
[category_theory.limits.preserves_filtered_colimits (category_theory.forget A)]
[category_theory.reflects_isomorphisms (category_theory.forget A)]
{G : C ⥤ D}
(hG₁ : category_theory.compatible_preserving K G)
(hG₂ : category_theory.cover_preserving J K G) :
category_theory.sites.pushforward A J K G ⊣ category_theory.sites.pullback A hG₁ hG₂
The pushforward functor is left adjoint to the pullback functor.
Equations
- category_theory.sites.pullback_pushforward_adjunction A J K hG₁ hG₂ = category_theory.adjunction.restrict_fully_faithful (category_theory.Sheaf_to_presheaf J A) (𝟭 (category_theory.Sheaf K A)) ((category_theory.Lan.adjunction A G.op).comp (category_theory.sheafification_adjunction K A)) (category_theory.nat_iso.of_components (λ (_x : category_theory.Sheaf J A), category_theory.iso.refl ((category_theory.Sheaf_to_presheaf J A ⋙ category_theory.Lan G.op ⋙ category_theory.presheaf_to_Sheaf K A).obj _x)) _) (category_theory.nat_iso.of_components (λ (_x : category_theory.Sheaf K A), category_theory.iso.refl ((𝟭 (category_theory.Sheaf K A) ⋙ category_theory.Sheaf_to_presheaf K A ⋙ (category_theory.whiskering_left Cᵒᵖ Dᵒᵖ A).obj G.op).obj _x)) _)