Cover-preserving functors between sites. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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).
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.compatible_preserving_of_downwards_closed
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{K : category_theory.grothendieck_topology D}
(F : C ⥤ D)
[category_theory.full F]
[category_theory.faithful F]
(hF : Π {c : C} {d : D}, (d ⟶ F.obj c) → (Σ (c' : C), F.obj c' ≅ d)) :
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' := _}