Skip to content

Commit 0e9ba7d

Browse files
joelrioujoelriou
committed
feat: the sheafification functor for presheaves of modules (#13441)
In this PR, we construct the sheafification functor for presheaves of modules, and show that it is a left adjoint functor.
1 parent 75349a6 commit 0e9ba7d

File tree

7 files changed

+284
-6
lines changed

7 files changed

+284
-6
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,7 @@ import Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
9696
import Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
9797
import Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
9898
import Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
99+
import Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
99100
import Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
100101
import Mathlib.Algebra.Category.ModuleCat.Products
101102
import Mathlib.Algebra.Category.ModuleCat.Projective

‎Mathlib/Algebra/Category/ModuleCat/Presheaf.lean‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -115,6 +115,13 @@ namespace Hom
115115

116116
variable {P Q T : PresheafOfModules R}
117117

118+
variable (P) in
119+
@[simp]
120+
lemma id_hom : Hom.hom (𝟙 P) = 𝟙 _ := rfl
121+
122+
@[simp, reassoc]
123+
lemma comp_hom (f : P ⟶ Q) (g : Q ⟶ T) : (f ≫ g).hom = f.hom ≫ g.hom := rfl
124+
118125
/--
119126
The `(X : Cᵒᵖ)`-component of morphism between presheaves of modules
120127
over a presheaf of rings `R`, as an `R.obj X`-linear map. -/

‎Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafification.lean‎

Lines changed: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
1+
/-
2+
Copyright (c) 2024 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+
import Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
7+
import Mathlib.CategoryTheory.Sites.LocallyBijective
8+
9+
/-!
10+
# The sheafification functor for presheaves of modules
11+
12+
In this file, we construct a functor
13+
`PresheafOfModules.sheafification α : PresheafOfModules R₀ ⥤ SheafOfModules R`
14+
for a locally bijective morphism `α : R₀ ⟶ R.val` where `R₀` is a presheaf of rings
15+
and `R` a sheaf of rings.
16+
In particular, if `α` is the identity of `R.val`, we obtain the
17+
sheafification functor `PresheafOfModules R.val ⥤ SheafOfModules R`.
18+
19+
-/
20+
21+
universe v v' u u'
22+
23+
open CategoryTheory Category
24+
25+
variable {C : Type u'} [Category.{v'} C] {J : GrothendieckTopology C}
26+
{R₀ : Cᵒᵖ ⥤ RingCat.{u}} {R : Sheaf J RingCat.{u}} (α : R₀ ⟶ R.val)
27+
[Presheaf.IsLocallyInjective J α] [Presheaf.IsLocallySurjective J α]
28+
[HasWeakSheafify J AddCommGroupCat.{v}]
29+
[J.WEqualsLocallyBijective AddCommGroupCat.{v}]
30+
31+
namespace PresheafOfModules
32+
33+
/-- Given a locally bijective morphism `α : R₀ ⟶ R.val` where `R₀` is a presheaf of rings
34+
and `R` a sheaf of rings (i.e. `R` identifies to the sheafification of `R₀`), this is
35+
the associated sheaf of modules functor `PresheafOfModules.{v} R₀ ⥤ SheafOfModules.{v} R`. -/
36+
@[simps! (config := .lemmasOnly) map]
37+
noncomputable def sheafification : PresheafOfModules.{v} R₀ ⥤ SheafOfModules.{v} R where
38+
obj M₀ := sheafify α (CategoryTheory.toSheafify J M₀.presheaf)
39+
map f := sheafifyMap _ _ _ f ((presheafToSheaf J AddCommGroupCat).map f.hom) (by simp)
40+
map_id M₀ := by
41+
ext1
42+
apply (toPresheaf _).map_injective
43+
simp [toPresheaf, sheafify]
44+
map_comp _ _ := by
45+
ext1
46+
apply (toPresheaf _).map_injective
47+
simp [toPresheaf, sheafify]
48+
49+
/-- The sheafification of presheaves of modules commutes with the functor which
50+
forgets the module structures. -/
51+
noncomputable def sheafificationCompToSheaf :
52+
sheafification.{v} α ⋙ SheafOfModules.toSheaf _ ≅
53+
toPresheaf _ ⋙ presheafToSheaf J AddCommGroupCat :=
54+
Iso.refl _
55+
56+
/-- The sheafification of presheaves of modules commutes with the functor which
57+
forgets the module structures. -/
58+
noncomputable def sheafificationCompForgetCompToPresheaf :
59+
sheafification.{v} α ⋙ SheafOfModules.forget _ ⋙ toPresheaf _ ≅
60+
toPresheaf _ ⋙ presheafToSheaf J AddCommGroupCat ⋙ sheafToPresheaf J AddCommGroupCat :=
61+
Iso.refl _
62+
63+
/-- The bijection between types of morphisms which is part of the adjunction
64+
`sheafificationAdjunction`. -/
65+
noncomputable def sheafificationHomEquiv
66+
{P : PresheafOfModules.{v} R₀} {F : SheafOfModules.{v} R} :
67+
((sheafification α).obj P ⟶ F) ≃
68+
(P ⟶ (restrictScalars α).obj ((SheafOfModules.forget _).obj F)) := by
69+
apply sheafifyHomEquiv
70+
71+
lemma sheafificationHomEquiv_hom'
72+
{P : PresheafOfModules.{v} R₀} {F : SheafOfModules.{v} R}
73+
(f : (sheafification α).obj P ⟶ F) :
74+
(sheafificationHomEquiv α f).hom =
75+
CategoryTheory.toSheafify J P.presheaf ≫ f.val.hom := rfl
76+
77+
lemma sheafificationHomEquiv_hom
78+
{P : PresheafOfModules.{v} R₀} {F : SheafOfModules.{v} R}
79+
(f : (sheafification α).obj P ⟶ F) :
80+
(sheafificationHomEquiv α f).hom =
81+
(sheafificationAdjunction J AddCommGroupCat).homEquiv P.presheaf
82+
((SheafOfModules.toSheaf _).obj F) ((SheafOfModules.toSheaf _).map f) := by
83+
rw [sheafificationHomEquiv_hom', Adjunction.homEquiv_unit]
84+
dsimp
85+
86+
lemma toSheaf_map_sheafificationHomEquiv_symm
87+
{P : PresheafOfModules.{v} R₀} {F : SheafOfModules.{v} R}
88+
(g : P ⟶ (restrictScalars α).obj ((SheafOfModules.forget _).obj F)) :
89+
(SheafOfModules.toSheaf _).map ((sheafificationHomEquiv α).symm g) =
90+
(((sheafificationAdjunction J AddCommGroupCat).homEquiv
91+
P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm g.hom) := by
92+
obtain ⟨f, rfl⟩ := (sheafificationHomEquiv α).surjective g
93+
apply ((sheafificationAdjunction J AddCommGroupCat).homEquiv _ _).injective
94+
rw [Equiv.apply_symm_apply, Adjunction.homEquiv_unit, Equiv.symm_apply_apply]
95+
rfl
96+
97+
/-- Given a locally bijective morphism `α : R₀ ⟶ R.val` where `R₀` is a presheaf of rings
98+
and `R` a sheaf of rings, this is the adjunction
99+
`sheafification.{v} α ⊣ SheafOfModules.forget R ⋙ restrictScalars α`. -/
100+
@[simps! (config := .lemmasOnly) homEquiv_apply]
101+
noncomputable def sheafificationAdjunction :
102+
sheafification.{v} α ⊣ SheafOfModules.forget R ⋙ restrictScalars α :=
103+
Adjunction.mkOfHomEquiv
104+
{ homEquiv := fun _ _ ↦ sheafificationHomEquiv α
105+
homEquiv_naturality_left_symm := fun {P₀ Q₀ N} f g ↦ by
106+
apply (SheafOfModules.toSheaf _).map_injective
107+
rw [Functor.map_comp]
108+
erw [toSheaf_map_sheafificationHomEquiv_symm,
109+
toSheaf_map_sheafificationHomEquiv_symm]
110+
apply Adjunction.homEquiv_naturality_left_symm
111+
homEquiv_naturality_right := fun {P₀ M N} f g ↦ by
112+
apply (toPresheaf _).map_injective
113+
dsimp [toPresheaf]
114+
erw [sheafificationHomEquiv_hom, sheafificationHomEquiv_hom]
115+
rw [Functor.map_comp]
116+
apply Adjunction.homEquiv_naturality_right }
117+
118+
@[simp]
119+
lemma sheafificationAdjunction_unit_app_hom (M₀ : PresheafOfModules.{v} R₀) :
120+
((sheafificationAdjunction α).unit.app M₀).hom = CategoryTheory.toSheafify J M₀.presheaf := by
121+
rfl
122+
123+
end PresheafOfModules

‎Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean‎

Lines changed: 68 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joël Riou. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Joël Riou
55
-/
6-
import Mathlib.Algebra.Category.ModuleCat.Sheaf
6+
import Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings
77
import Mathlib.CategoryTheory.Sites.LocallySurjective
88

99
/-!
@@ -20,11 +20,6 @@ In many application, the morphism `α` shall be the identity, but this more
2020
general construction allows the sheafification of both the presheaf of rings
2121
and the presheaf of modules.
2222
23-
## TODO
24-
25-
- promote this construction to a functor from presheaves of modules over `R₀`
26-
to sheaves of modules over `R`, and construct an adjunction.
27-
2823
-/
2924

3025
universe w v v₁ u₁ u
@@ -317,4 +312,71 @@ noncomputable def sheafify : SheafOfModules.{v} R where
317312
map_smul := fun _ _ _ => by apply Sheafify.map_smul }
318313
isSheaf := A.cond
319314

315+
/-- The canonical morphism from a presheaf of modules to its associated sheaf. -/
316+
@[simps]
317+
def toSheafify : M₀ ⟶ (restrictScalars α).obj (sheafify α φ).val where
318+
hom := φ
319+
map_smul X r₀ m₀ := by
320+
simpa using (Sheafify.map_smul_eq α φ (α.app _ r₀) (φ.app _ m₀) (𝟙 _)
321+
r₀ (by aesop) m₀ (by simp)).symm
322+
323+
instance : Presheaf.IsLocallyInjective J (toSheafify α φ).hom :=
324+
by dsimp; infer_instance
325+
326+
instance : Presheaf.IsLocallySurjective J (toSheafify α φ).hom :=
327+
by dsimp; infer_instance
328+
329+
variable [J.WEqualsLocallyBijective AddCommGroupCat.{v}]
330+
331+
/-- The bijection `((sheafify α φ).val ⟶ F) ≃ (M₀ ⟶ (restrictScalars α).obj F)` which
332+
is part of the universal property of the sheafification of the presheaf of modules `M₀`,
333+
when `F` is a presheaf of modules which is a sheaf. -/
334+
noncomputable def sheafifyHomEquiv' {F : PresheafOfModules.{v} R.val}
335+
(hF : Presheaf.IsSheaf J F.presheaf) :
336+
((sheafify α φ).val ⟶ F) ≃ (M₀ ⟶ (restrictScalars α).obj F) :=
337+
(restrictHomEquivOfIsLocallySurjective α hF).trans
338+
(homEquivOfIsLocallyBijective (f := toSheafify α φ)
339+
(N := (restrictScalars α).obj F) hF)
340+
341+
lemma comp_sheafifyHomEquiv'_symm_hom {F : PresheafOfModules.{v} R.val}
342+
(hF : Presheaf.IsSheaf J F.presheaf) (f : M₀ ⟶ (restrictScalars α).obj F) :
343+
φ ≫ ((sheafifyHomEquiv' α φ hF).symm f).hom = f.hom :=
344+
congr_arg Hom.hom ((sheafifyHomEquiv' α φ hF).apply_symm_apply f)
345+
346+
/-- The bijection
347+
`(sheafify α φ ⟶ F) ≃ (M₀ ⟶ (restrictScalars α).obj ((SheafOfModules.forget _).obj F))`
348+
which is part of the universal property of the sheafification of the presheaf of modules `M₀`,
349+
for any sheaf of modules `F`, see `PresheafOfModules.sheafificationAdjunction` -/
350+
noncomputable def sheafifyHomEquiv {F : SheafOfModules.{v} R} :
351+
(sheafify α φ ⟶ F) ≃
352+
(M₀ ⟶ (restrictScalars α).obj ((SheafOfModules.forget _).obj F)) :=
353+
(SheafOfModules.fullyFaithfulForget R).homEquiv.trans
354+
(sheafifyHomEquiv' α φ F.isSheaf)
355+
356+
section
357+
358+
variable {M₀' : PresheafOfModules.{v} R₀} {A' : Sheaf J AddCommGroupCat.{v}}
359+
(φ' : M₀'.presheaf ⟶ A'.val)
360+
[Presheaf.IsLocallyInjective J φ'] [Presheaf.IsLocallySurjective J φ']
361+
(τ₀ : M₀ ⟶ M₀') (τ : A ⟶ A')
362+
(fac : τ₀.hom ≫ φ' = φ ≫ τ.val)
363+
364+
/-- The morphism of sheaves of modules `sheafify α φ ⟶ sheafify α φ'`
365+
induced by morphisms `τ₀ : M₀ ⟶ M₀'` and `τ : A ⟶ A'`
366+
which satisfy `τ₀.hom ≫ φ' = φ ≫ τ.val`. -/
367+
@[simps]
368+
def sheafifyMap : sheafify α φ ⟶ sheafify α φ' where
369+
val :=
370+
{ hom := τ.val
371+
map_smul := by
372+
let f := (sheafifyHomEquiv' α φ (by exact A'.cond)).symm (τ₀ ≫ toSheafify α φ')
373+
have eq : τ.val = f.hom := ((J.W_of_isLocallyBijective φ).homEquiv _ A'.cond).injective
374+
(by
375+
dsimp [f]
376+
erw [comp_sheafifyHomEquiv'_symm_hom]
377+
simp only [← fac, toSheafify_hom, Hom.comp_hom])
378+
convert f.map_smul }
379+
380+
end
381+
320382
end PresheafOfModules

‎Mathlib/Algebra/Category/ModuleCat/Sheaf.lean‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Joël Riou
55
-/
66

77
import Mathlib.Algebra.Category.ModuleCat.Presheaf
8+
import Mathlib.CategoryTheory.Sites.LocallyBijective
89
import Mathlib.CategoryTheory.Sites.Whiskering
910

1011
/-!
@@ -83,6 +84,22 @@ instance : (forget.{v} R).Full := (fullyFaithfulForget R).full
8384
def evaluation (X : Cᵒᵖ) : SheafOfModules.{v} R ⥤ ModuleCat.{v} (R.val.obj X) :=
8485
forget _ ⋙ PresheafOfModules.evaluation _ X
8586

87+
/-- The forget functor `SheafOfModules R ⥤ Sheaf J AddCommGroupCat`. -/
88+
@[simps]
89+
def toSheaf : SheafOfModules.{v} R ⥤ Sheaf J AddCommGroupCat.{v} where
90+
obj M := ⟨_, M.isSheaf⟩
91+
map f := { val := f.val.hom }
92+
93+
/-- The canonical isomorphism between
94+
`SheafOfModules.toSheaf R ⋙ sheafToPresheaf J AddCommGroupCat.{v}`
95+
and `SheafOfModules.forget R ⋙ PresheafOfModules.toPresheaf R.val`. -/
96+
def toSheafCompSheafToPresheafIso :
97+
toSheaf R ⋙ sheafToPresheaf J AddCommGroupCat.{v} ≅
98+
forget R ⋙ PresheafOfModules.toPresheaf R.val := Iso.refl _
99+
100+
instance : (toSheaf.{v} R).Faithful :=
101+
Functor.Faithful.of_comp_iso (toSheafCompSheafToPresheafIso.{v} R)
102+
86103
/-- The type of sections of a sheaf of modules. -/
87104
abbrev sections (M : SheafOfModules.{v} R) : Type _ := M.val.sections
88105

@@ -106,3 +123,39 @@ lemma unitHomEquiv_apply_coe (M : SheafOfModules R) (f : unit R ⟶ M) (X : Cᵒ
106123
(M.unitHomEquiv f).val X = f.val.app X (1 : R.val.obj X) := rfl
107124

108125
end SheafOfModules
126+
127+
namespace PresheafOfModules
128+
129+
variable {R : Cᵒᵖ ⥤ RingCat.{u}} {M₁ M₂ : PresheafOfModules.{v} R}
130+
(f : M₁ ⟶ M₂) {N : PresheafOfModules.{v} R}
131+
(hN : Presheaf.IsSheaf J N.presheaf)
132+
[J.WEqualsLocallyBijective AddCommGroupCat.{v}]
133+
[Presheaf.IsLocallySurjective J f.hom]
134+
[Presheaf.IsLocallyInjective J f.hom]
135+
136+
/-- The bijection `(M₂ ⟶ N) ≃ (M₁ ⟶ N)` induced by a locally bijective morphism
137+
`f : M₁ ⟶ M₂` of presheaves of modules, when `N` is a sheaf. -/
138+
@[simps]
139+
noncomputable def homEquivOfIsLocallyBijective : (M₂ ⟶ N) ≃ (M₁ ⟶ N) where
140+
toFun φ := f ≫ φ
141+
invFun ψ :=
142+
{ hom := ((J.W_of_isLocallyBijective f.hom).homEquiv _ hN).symm ψ.hom
143+
map_smul := by
144+
obtain ⟨φ, hφ⟩ := ((J.W_of_isLocallyBijective f.hom).homEquiv _ hN).surjective ψ.hom
145+
simp only [← hφ, Equiv.symm_apply_apply]
146+
dsimp at hφ
147+
intro X r y
148+
apply hN.isSeparated _ _ (Presheaf.imageSieve_mem J f.hom y)
149+
rintro Y p ⟨x, hx⟩
150+
have eq := ψ.map_smul _ (R.map p.op r) x
151+
simp only [← hφ] at eq
152+
dsimp at eq
153+
erw [← NatTrans.naturality_apply φ p.op (r • y), N.map_smul, M₂.map_smul,
154+
← NatTrans.naturality_apply φ p.op y, ← hx, ← eq, f.map_smul]
155+
rfl }
156+
left_inv φ := (toPresheaf _).map_injective
157+
(((J.W_of_isLocallyBijective f.hom).homEquiv _ hN).left_inv φ.hom)
158+
right_inv ψ := (toPresheaf _).map_injective
159+
(((J.W_of_isLocallyBijective f.hom).homEquiv _ hN).right_inv ψ.hom)
160+
161+
end PresheafOfModules

‎Mathlib/Algebra/Category/ModuleCat/Sheaf/ChangeOfRings.lean‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Joël Riou
55
-/
66
import Mathlib.Algebra.Category.ModuleCat.Sheaf
77
import Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
8+
import Mathlib.CategoryTheory.Sites.LocallySurjective
89

910
/-!
1011
# Change of sheaf of rings
@@ -36,3 +37,29 @@ noncomputable def restrictScalars :
3637
map φ := { val := (PresheafOfModules.restrictScalars α.val).map φ.val }
3738

3839
end SheafOfModules
40+
41+
namespace PresheafOfModules
42+
43+
variable {R R' : Cᵒᵖ ⥤ RingCat.{u}} (α : R ⟶ R')
44+
{M₁ M₂ : PresheafOfModules.{v} R'} (hM₂ : Presheaf.IsSheaf J M₂.presheaf)
45+
[Presheaf.IsLocallySurjective J α]
46+
47+
/-- The functor `PresheafOfModules.restrictScalars α` induces bijection on
48+
morphisms if `α` is locally surjective and the target presheaf is a sheaf. -/
49+
noncomputable def restrictHomEquivOfIsLocallySurjective :
50+
(M₁ ⟶ M₂) ≃ ((restrictScalars α).obj M₁ ⟶ (restrictScalars α).obj M₂) where
51+
toFun f := (restrictScalars α).map f
52+
invFun g :=
53+
{ hom := g.hom
54+
map_smul := fun X r' m => by
55+
apply hM₂.isSeparated _ _ (Presheaf.imageSieve_mem J α r')
56+
rintro Y p ⟨r : R.obj _, hr⟩
57+
erw [M₂.map_smul, ← NatTrans.naturality_apply g.hom p.op m,
58+
← hr, ← g.map_smul _ r (M₁.presheaf.map p.op m),
59+
← NatTrans.naturality_apply g.hom p.op (r' • m),
60+
M₁.map_smul p.op r' m, ← hr]
61+
rfl }
62+
left_inv _ := rfl
63+
right_inv _ := rfl
64+
65+
end PresheafOfModules

‎Mathlib/CategoryTheory/Sites/LocallyBijective.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -109,6 +109,11 @@ lemma W_iff_isLocallyBijective :
109109
J.W f ↔ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f := by
110110
apply WEqualsLocallyBijective.iff
111111

112+
lemma W_of_isLocallyBijective [Presheaf.IsLocallyInjective J f]
113+
[Presheaf.IsLocallySurjective J f] : J.W f := by
114+
rw [W_iff_isLocallyBijective]
115+
constructor <;> infer_instance
116+
112117
variable {J f}
113118

114119
lemma W.isLocallyInjective (hf : J.W f) : Presheaf.IsLocallyInjective J f :=

0 commit comments

Comments
 (0)