Skip to content

Commit 3c2700d

Browse files
joelrioujoelriou
committed
feat(CategoryTheory/Sites): skyscraper sheaves (#35719)
Let `Φ` be a point of a site `(C, J)`. In this file, we construct the skyscraper sheaf functor `skyscraperSheafFunctor : A ⥤ Sheaf J A` and show that it is a right adjoint to `Φ.sheafFiber : Sheaf J A ⥤ A`.
1 parent af1b8b4 commit 3c2700d

5 files changed

Lines changed: 257 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3169,6 +3169,7 @@ public import Mathlib.CategoryTheory.Sites.Point.Basic
31693169
public import Mathlib.CategoryTheory.Sites.Point.Category
31703170
public import Mathlib.CategoryTheory.Sites.Point.Conservative
31713171
public import Mathlib.CategoryTheory.Sites.Point.Over
3172+
public import Mathlib.CategoryTheory.Sites.Point.Skyscraper
31723173
public import Mathlib.CategoryTheory.Sites.Precoverage
31733174
public import Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
31743175
public import Mathlib.CategoryTheory.Sites.Preserves

‎Mathlib/CategoryTheory/Limits/Shapes/Products.lean‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -940,4 +940,24 @@ def Cofan.IsColimit.prod (c : ∀ i : ι, Cofan (fun j : ι' ↦ X i j)) (hc :
940940

941941
end Fubini
942942

943+
/-- The functor `C ⥤ (Type w)ᵒᵖ ⥤ C` which sends `X : C` and `α : Type w` to
944+
the product of copies of `X` indexed by `α`. -/
945+
@[simps]
946+
def piFunctor [HasProducts.{w} C] :
947+
C ⥤ (Type w)ᵒᵖ ⥤ C where
948+
obj X :=
949+
{ obj α := ∏ᶜ (fun (t : α.unop) ↦ X)
950+
map f := Pi.map' f.unop (fun _ ↦ 𝟙 _) }
951+
map f := { app T := Pi.map (fun _ ↦ f) }
952+
953+
/-- The functor `C ⥤ Type w ⥤ C` which sends `X : C` and `α : Type w` to
954+
the coproduct of copies of `X` indexed by `α`. -/
955+
@[simps]
956+
def sigmaFunctor [HasCoproducts.{w} C] :
957+
C ⥤ Type w ⥤ C where
958+
obj X :=
959+
{ obj α := ∐ (fun (t : α) ↦ X)
960+
map f := Sigma.map' f (fun _ ↦ 𝟙 _) }
961+
map f := { app T := Sigma.map (fun _ ↦ f) }
962+
943963
end CategoryTheory.Limits

‎Mathlib/CategoryTheory/Sites/Point/Skyscraper.lean‎

Lines changed: 228 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,228 @@
1+
/-
2+
Copyright (c) 2026 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou
5+
-/
6+
module
7+
8+
public import Mathlib.CategoryTheory.Sites.Point.Basic
9+
10+
/-!
11+
# Skyscraper sheaves
12+
13+
Let `Φ` be a point of a site `(C, J)`. In this file, we construct the
14+
skyscraper sheaf functor `skyscraperSheafFunctor : A ⥤ Sheaf J A` and
15+
show that it is a right adjoint to `Φ.sheafFiber : Sheaf J A ⥤ A`.
16+
17+
-/
18+
19+
@[expose] public section
20+
21+
universe w v' v u' u
22+
23+
namespace CategoryTheory.GrothendieckTopology.Point
24+
25+
open Limits Opposite
26+
27+
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
28+
(Φ : Point.{w} J) {A : Type u'} [Category.{v'} A]
29+
[HasProducts.{w} A]
30+
31+
/-- Given a point `Φ` on a site `(C, J)`, this is the skyscraper presheaf functor
32+
`A ⥤ Cᵒᵖ ⥤ A`. -/
33+
@[simps!]
34+
noncomputable def skyscraperPresheafFunctor : A ⥤ Cᵒᵖ ⥤ A :=
35+
Functor.flip (Φ.fiber.op ⋙ piFunctor.{w}.flip)
36+
37+
/-- Given a point `Φ` on a site `(C, J)`, and an object `M` of a category `A`,
38+
this is the skyscraper presheaf with value `M`: it sends `X : C` to the
39+
product of copies of `M` indexed by `Φ.fiber.obj X`. -/
40+
noncomputable abbrev skyscraperPresheaf (M : A) :
41+
Cᵒᵖ ⥤ A :=
42+
Φ.skyscraperPresheafFunctor.obj M
43+
44+
section
45+
46+
variable {P Q : Cᵒᵖ ⥤ A} {M N : A} [HasColimitsOfSize.{w, w} A]
47+
48+
/-- If `Φ` is a point of a site `(C, J)`, `P : Cᵒᵖ ⥤ A` and `M : A`, this is
49+
the bijection `(Φ.presheafFiber.obj P ⟶ M) ≃ (P ⟶ Φ.skyscraperPresheaf M)`
50+
that is part of the adjunction `skyscraperPresheafAdjunction`. -/
51+
@[simps -isSimp apply_app symm_apply]
52+
noncomputable def skyscraperPresheafHomEquiv :
53+
(Φ.presheafFiber.obj P ⟶ M) ≃ (P ⟶ Φ.skyscraperPresheaf M) where
54+
toFun f :=
55+
{ app X := Pi.lift (fun x ↦ Φ.toPresheafFiber X.unop x P ≫ f)
56+
naturality {X Y} g := by
57+
dsimp
58+
ext y
59+
have := Φ.toPresheafFiber_w g.unop y P
60+
dsimp at this
61+
simp [reassoc_of% this] }
62+
invFun g := Φ.presheafFiberDesc (fun X x ↦ g.app (op X) ≫ Pi.π _ x) (by simp)
63+
left_inv f := by cat_disch
64+
right_inv g := by cat_disch
65+
66+
@[reassoc (attr := simp)]
67+
lemma toPresheafFiber_skyscraperPresheafHomEquiv_symm
68+
(g : P ⟶ Φ.skyscraperPresheaf M) (X : C) (x : Φ.fiber.obj X) :
69+
Φ.toPresheafFiber X x P ≫ Φ.skyscraperPresheafHomEquiv.symm g =
70+
g.app (op X) ≫ Pi.π _ x := by
71+
simp [skyscraperPresheafHomEquiv_symm_apply]
72+
73+
@[reassoc]
74+
lemma skyscraperPresheafHomEquiv_naturality_left_symm
75+
(f : P ⟶ Q) (g : Q ⟶ Φ.skyscraperPresheaf M) :
76+
Φ.skyscraperPresheafHomEquiv.symm (f ≫ g) =
77+
Φ.presheafFiber.map f ≫ Φ.skyscraperPresheafHomEquiv.symm g := by
78+
cat_disch
79+
80+
@[reassoc (attr := simp)]
81+
lemma skyscraperPresheafHomEquiv_app_π
82+
(f : Φ.presheafFiber.obj P ⟶ M) (X : C) (x : Φ.fiber.obj X) :
83+
(Φ.skyscraperPresheafHomEquiv f).app (op X) ≫ Pi.π (fun (_ : Φ.fiber.obj X) ↦ M) x =
84+
Φ.toPresheafFiber X x P ≫ f := by
85+
simp [skyscraperPresheafHomEquiv_apply_app]
86+
87+
@[reassoc]
88+
lemma skyscraperPresheafHomEquiv_naturality_right
89+
(f : Φ.presheafFiber.obj P ⟶ M) (g : M ⟶ N) :
90+
Φ.skyscraperPresheafHomEquiv (f ≫ g) =
91+
Φ.skyscraperPresheafHomEquiv f ≫ Φ.skyscraperPresheafFunctor.map g := by
92+
ext
93+
dsimp
94+
ext
95+
dsimp
96+
rw [skyscraperPresheafHomEquiv_app_π]
97+
dsimp
98+
rw [Category.assoc, Pi.map_π, skyscraperPresheafHomEquiv_app_π_assoc]
99+
100+
end
101+
102+
section
103+
104+
variable [HasColimitsOfSize.{w, w} A]
105+
106+
/-- Given a point of a site, the skyscraper presheaf functor is right adjoint
107+
to the fiber functor on presheaves. -/
108+
noncomputable def skyscraperPresheafAdjunction [HasColimitsOfSize.{w, w} A] :
109+
Φ.presheafFiber (A := A) ⊣ Φ.skyscraperPresheafFunctor :=
110+
Adjunction.mkOfHomEquiv
111+
{ homEquiv _ _ := Φ.skyscraperPresheafHomEquiv
112+
homEquiv_naturality_left_symm _ _ := Φ.skyscraperPresheafHomEquiv_naturality_left_symm _ _
113+
homEquiv_naturality_right _ _ := Φ.skyscraperPresheafHomEquiv_naturality_right _ _ }
114+
115+
@[simp]
116+
lemma skyscraperPresheafAdjunction_homEquiv_apply {P : Cᵒᵖ ⥤ A} {M : A}
117+
(f : Φ.presheafFiber.obj P ⟶ M) :
118+
Φ.skyscraperPresheafAdjunction.homEquiv _ _ f =
119+
Φ.skyscraperPresheafHomEquiv f := by
120+
simp [skyscraperPresheafAdjunction]
121+
122+
@[simp]
123+
lemma skyscraperPresheafAdjunction_homEquiv_symm_apply {P : Cᵒᵖ ⥤ A} {M : A}
124+
(f : P ⟶ Φ.skyscraperPresheaf M) :
125+
(Φ.skyscraperPresheafAdjunction.homEquiv _ _).symm f =
126+
Φ.skyscraperPresheafHomEquiv.symm f := by
127+
simp [skyscraperPresheafAdjunction]
128+
129+
end
130+
131+
variable {Φ} in
132+
private lemma isSheaf_skyscraperPresheaf_aux
133+
{M : A} {X : C} (R : Sieve X) (hR : R ∈ J X)
134+
(s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)) :
135+
∃ (l : s.pt ⟶ ∏ᶜ fun (_ : Φ.fiber.obj X) ↦ M),
136+
∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj.left),
137+
l ≫ Pi.π _ (Φ.fiber.map j.obj.hom y) = s.π.app (op j) ≫ Pi.π _ y := by
138+
suffices ∀ (x : Φ.fiber.obj X), ∃ (l : s.pt ⟶ M),
139+
∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R g) (y : Φ.fiber.obj Y) (hy : Φ.fiber.map g y = x),
140+
s.π.app (op (Presieve.categoryMk _ _ hg)) ≫ Pi.π _ y = l by
141+
choose l hl using this
142+
exact ⟨Pi.lift l, fun j y ↦ by simpa using (hl _ j.obj.hom j.property y rfl).symm⟩
143+
intro x
144+
obtain ⟨Y₁, f₁, hf₁, y₁, hy₁⟩ := Φ.jointly_surjective _ hR x
145+
refine ⟨s.π.app (op (Presieve.categoryMk _ _ hf₁)) ≫ Pi.π _ y₁,
146+
fun Y₂ f₂ hf₂ y₂ hy₂ ↦ ?_⟩
147+
obtain ⟨Z, p₁, p₂, z, fac, hz₁, hz₂⟩ :
148+
∃ (Z : C) (p₁ : Z ⟶ Y₁) (p₂ : Z ⟶ Y₂) (z : Φ.fiber.obj Z), p₁ ≫ f₁ = p₂ ≫ f₂ ∧
149+
Φ.fiber.map p₁ z = y₁ ∧ Φ.fiber.map p₂ z = y₂ := by
150+
let α₁ : Φ.fiber.elementsMk _ y₁ ⟶ Φ.fiber.elementsMk _ x := ⟨f₁, hy₁⟩
151+
let α₂ : Φ.fiber.elementsMk _ y₂ ⟶ Φ.fiber.elementsMk _ x := ⟨f₂, hy₂⟩
152+
obtain ⟨z, q₁, q₂, fac⟩ := IsCofiltered.cospan α₁ α₂
153+
rw [Subtype.ext_iff] at fac
154+
exact ⟨z.1, q₁.1, q₂.1, z.2, fac, by simp, by simp⟩
155+
let φ₁ : Presieve.categoryMk _ _ (R.downward_closed hf₁ p₁) ⟶
156+
Presieve.categoryMk _ _ hf₁ :=
157+
ObjectProperty.homMk (Over.homMk p₁)
158+
let φ₂ : Presieve.categoryMk _ _ (R.downward_closed hf₁ p₁) ⟶
159+
Presieve.categoryMk _ _ hf₂ :=
160+
ObjectProperty.homMk (Over.homMk p₂)
161+
simpa [hz₁, hz₂, φ₁, φ₂] using
162+
(Cone.w s φ₂.op =≫ Pi.π _ z).trans (Cone.w s φ₁.op =≫ Pi.π _ z).symm
163+
164+
lemma isSheaf_skyscraperPresheaf (M : A) :
165+
Presheaf.IsSheaf J (Φ.skyscraperPresheaf M) := by
166+
rw [Presheaf.isSheaf_iff_isLimit]
167+
intro X R hR
168+
exact ⟨{
169+
lift s := (isSheaf_skyscraperPresheaf_aux R hR s).choose
170+
fac s j := by
171+
dsimp
172+
ext y
173+
simpa using (isSheaf_skyscraperPresheaf_aux R hR s).choose_spec _ y
174+
uniq s m hm := by
175+
dsimp at hm ⊢
176+
ext x
177+
obtain ⟨Y, g, hg, y, rfl⟩ := Φ.jointly_surjective _ hR x
178+
have := (isSheaf_skyscraperPresheaf_aux R hR s).choose_spec
179+
(Presieve.categoryMk _ _ hg) y
180+
dsimp at this
181+
simp [this, ← hm (op (Presieve.categoryMk _ _ hg))] }⟩
182+
183+
/-- Given a point `Φ` of a site `(C, J)`, this is the skyscraper sheaf functor
184+
`A ⥤ Sheaf J A`. -/
185+
@[simps]
186+
noncomputable def skyscraperSheafFunctor : A ⥤ Sheaf J A where
187+
obj M := ⟨Φ.skyscraperPresheaf M, Φ.isSheaf_skyscraperPresheaf M⟩
188+
map f := ⟨Φ.skyscraperPresheafFunctor.map f⟩
189+
190+
/-- Given a point `Φ` on a site `(C, J)`, and an object `M` of a category `A`,
191+
this is the skyscraper sheaf with value `M`: it sends `X : C` to the
192+
product of copies of `M` indexed by `Φ.fiber.obj X`. -/
193+
noncomputable abbrev skyscraperSheaf (M : A) :
194+
Sheaf J A :=
195+
Φ.skyscraperSheafFunctor.obj M
196+
197+
variable [HasColimitsOfSize.{w, w} A]
198+
199+
/-- Given a point of a site, the skyscraper sheaf functor is right adjoint
200+
to the fiber functor on sheaves. -/
201+
noncomputable def skyscraperSheafAdjunction :
202+
Φ.sheafFiber (A := A) ⊣ Φ.skyscraperSheafFunctor :=
203+
Adjunction.mkOfHomEquiv
204+
{ homEquiv F M :=
205+
Φ.skyscraperPresheafHomEquiv.trans
206+
((fullyFaithfulSheafToPresheaf J A).homEquiv (Y := Φ.skyscraperSheaf M)).symm
207+
homEquiv_naturality_left_symm f g :=
208+
Φ.skyscraperPresheafHomEquiv_naturality_left_symm f.val g.val
209+
homEquiv_naturality_right f g := by
210+
ext : 1
211+
exact Φ.skyscraperPresheafHomEquiv_naturality_right f g }
212+
213+
@[simp]
214+
lemma skyscraperSheafAdjunction_homEquiv_apply_val {F : Sheaf J A} {M : A}
215+
(f : Φ.presheafFiber.obj F.val ⟶ M) :
216+
letI e : (Φ.presheafFiber.obj F.val ⟶ M) ≃ _ := Φ.skyscraperSheafAdjunction.homEquiv F M
217+
letI a : F.val ⟶ Φ.skyscraperPresheaf M := (e f).val
218+
a = Φ.skyscraperPresheafHomEquiv f := by
219+
simp [skyscraperSheafAdjunction, Functor.FullyFaithful.homEquiv]
220+
221+
@[simp]
222+
lemma skyscraperSheafAdjunction_homEquiv_symm_apply {F : Sheaf J A} {M : A}
223+
(f : F ⟶ Φ.skyscraperSheaf M) :
224+
letI e : (Φ.presheafFiber.obj F.val ⟶ M) ≃ _ := Φ.skyscraperSheafAdjunction.homEquiv F M
225+
e.symm f = Φ.skyscraperPresheafHomEquiv.symm f.val := by
226+
simp [skyscraperSheafAdjunction, Functor.FullyFaithful.homEquiv]
227+
228+
end CategoryTheory.GrothendieckTopology.Point

‎Mathlib/Topology/Sheaves/Skyscraper.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,10 @@ of `p₀`, i.e. if `p₀ ⤳ x` then `𝓕ₓ ≅ A` and if `¬ p₀ ⤳ x` then
3131
`skyscraperPresheaf p₀ A` at `y` is `*` the terminal object.
3232
3333
TODO: generalize universe level when calculating stalks, after generalizing universe level of stalk.
34+
TODO(@joelriou): refactor the definitions in this file so as to make them
35+
particular cases of general constructions for points of sites from
36+
`Mathlib/CategoryTheory/Sites/Point/Skyscraper.lean`.
37+
3438
-/
3539

3640
@[expose] public section

‎Mathlib/Topology/Sheaves/Stalks.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,10 @@ isomorphisms.
3838
See also the definition of "algebraic structures" in the stacks project:
3939
https://stacks.math.columbia.edu/tag/007L
4040
41+
TODO(@joelriou): refactor the definitions in this file so as to make them
42+
particular cases of general constructions for points of sites from
43+
`Mathlib/CategoryTheory/Sites/Point/Basic.lean`.
44+
4145
-/
4246

4347
@[expose] public section

0 commit comments

Comments
 (0)