Skip to content

Commit 561064a

Browse files
joelrioujoelriou
committed
feat(Algebra/Category/ModuleCat/Presheaf): the colimit module of a presheaf of modules on a cofiltered category
1 parent b840598 commit 561064a

File tree

3 files changed

+254
-0
lines changed

3 files changed

+254
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -178,6 +178,7 @@ public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
178178
public import Mathlib.Algebra.Category.ModuleCat.Presheaf
179179
public import Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian
180180
public import Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
181+
public import Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
181182
public import Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
182183
public import Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
183184
public import Mathlib.Algebra.Category.ModuleCat.Presheaf.Free

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

Lines changed: 244 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,244 @@
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.Algebra.Category.ModuleCat.Presheaf
9+
public import Mathlib.Algebra.Category.Ring.FilteredColimits
10+
public import Mathlib.CategoryTheory.Filtered.FinallySmall
11+
public import Mathlib.CategoryTheory.Monoidal.Limits.Colimits
12+
13+
/-!
14+
# The colimit module of a presheaf of modules on a cofiltered category
15+
16+
Given a colimit cocone `cR` for a presheaf of rings `R` on a cofiltered category `C`,
17+
`M` a presheaf of modules over `R`, and a colimit cocone `cM` for the underlying
18+
functor `Cᵒᵖ ⥤ AddCommGrpCat` of `M`, we define a structure of module over `cR.pt`
19+
on a type-synonym `PresheafOfModules.ModuleColimit` for `cM.pt`. This extends to
20+
a functor `PresheafOfModules.colimitFunctor : PresheafOfModules R ⥤ ModuleCat cR.pt`.
21+
22+
## TODO (@joelriou)
23+
* Define fiber functors on categories of (pre)sheaves of modules
24+
* Refactor `Mathlib/Algebra/Category/ModuleCat/Stalk.lean` so that it uses
25+
this slightly more general construction.
26+
27+
-/
28+
29+
@[expose] public section
30+
31+
universe w v u
32+
33+
open CategoryTheory Limits MonoidalCategory
34+
35+
attribute [local instance] hasColimitsOfShape_of_finallySmall
36+
IsFiltered.isSifted FinallySmall.preservesColimitsOfShape_of_isFiltered
37+
38+
namespace PresheafOfModules
39+
40+
variable {C : Type u} [Category.{v} C] [LocallySmall.{w} C]
41+
[IsCofiltered C] [InitiallySmall.{w} C]
42+
{R : Cᵒᵖ ⥤ RingCat.{w}} {cR : Cocone R} (hcR : IsColimit cR)
43+
44+
section
45+
46+
variable {M : PresheafOfModules.{w} R} {cM : Cocone M.presheaf} (hcM : IsColimit cM)
47+
{M' : PresheafOfModules.{w} R} {cM' : Cocone M'.presheaf} (hcM' : IsColimit cM')
48+
{M'' : PresheafOfModules.{w} R} {cM'' : Cocone M''.presheaf} (hcM'' : IsColimit cM'')
49+
50+
/-- Given a colimit cocone for a presheaf of rings `R` on a cofiltered category `C`,
51+
`M` a presheaf of modules over `R`, and a colimit cocone `cM` for the underlying
52+
functor `Cᵒᵖ ⥤ AddCommGrpCat` of `M`, this is the type `cM.pt` on which we define
53+
a module structure below. -/
54+
@[nolint unusedArguments]
55+
def ModuleColimit (_ : IsColimit cR) (_ : IsColimit cM) : Type w := cM.pt
56+
57+
instance : AddCommGroup (ModuleColimit hcR hcM) :=
58+
inferInstanceAs (AddCommGroup cM.pt)
59+
60+
namespace ModuleColimit
61+
62+
/-- The cocone for `R ⋙ forget _ ⊗ M.presheaf ⋙ forget _` with point
63+
`ModuleColimit hcR hcM` which allows to define the scalar multiplication
64+
by `cR.pt` on `ModuleColimit hcR hcM`. -/
65+
@[simps]
66+
noncomputable def coconeSMul :
67+
Cocone (R ⋙ forget _ ⊗ M.presheaf ⋙ forget _) where
68+
pt := ModuleColimit hcR hcM
69+
ι.app U := fun ⟨(r : R.obj U), (m : M.obj U)⟩ ↦ by exact cM.ι.app U (r • m)
70+
ι.naturality V U f := by
71+
ext ⟨r, m⟩
72+
exact (ConcreteCategory.congr_arg (cM.ι.app U)
73+
(M.map_smul f r m).symm).trans (ConcreteCategory.congr_hom (cM.w f) _)
74+
75+
noncomputable instance : SMul cR.pt (ModuleColimit hcR hcM) where
76+
smul :=
77+
(((isColimitOfPreserves (forget _) hcR).tensor
78+
(isColimitOfPreserves (forget _) hcM)).desc (coconeSMul hcR hcM)).curry
79+
80+
variable (cR) in
81+
/-- The "inclusion" maps to the colimit ring. -/
82+
abbrev ιR {U : Cᵒᵖ} : R.obj U →+* cR.pt := (cR.ι.app U).hom
83+
84+
variable {hcR hcM} in
85+
/-- The "inclusion" maps to the colimit module, as an additive map. -/
86+
noncomputable abbrev ιM {U : Cᵒᵖ} : M.obj U →+ ModuleColimit hcR hcM :=
87+
(cM.ι.app U).hom
88+
89+
@[simp]
90+
lemma smul_eq {U : Cᵒᵖ} (r : R.obj U) (m : M.obj U) :
91+
ιR cR r • ιM (hcR := hcR) (hcM := hcM) m = ιM (r • m) :=
92+
congr_fun (((isColimitOfPreserves (forget _) hcR).tensor
93+
(isColimitOfPreserves (forget _) hcM)).fac (coconeSMul hcR hcM) U) ⟨r, m⟩
94+
95+
variable {hcR hcM} in
96+
lemma ιM_jointly_surjective (m : ModuleColimit hcR hcM) :
97+
∃ (U : Cᵒᵖ) (x : M.obj U), ιM x = m :=
98+
Types.jointly_surjective_of_isColimit
99+
(isColimitOfPreserves (forget AddCommGrpCat) hcM) m
100+
101+
set_option backward.isDefEq.respectTransparency false in
102+
variable {hcR hcM hcM'} in
103+
lemma ιM_jointly_surjective₂ (m : ModuleColimit hcR hcM) (m' : ModuleColimit hcR hcM') :
104+
∃ (U : Cᵒᵖ) (x : M.obj U) (x' : M'.obj U), ιM x = m ∧ ιM x' = m' := by
105+
obtain ⟨U, ⟨x, x'⟩, h⟩ := Types.jointly_surjective_of_isColimit
106+
((isColimitOfPreserves (forget AddCommGrpCat) hcM).tensor
107+
(isColimitOfPreserves (forget AddCommGrpCat) hcM')) ⟨m, m'⟩
108+
rw [Prod.ext_iff] at h
109+
obtain ⟨rfl, rfl⟩ := h
110+
exact ⟨U, x, x', rfl, rfl⟩
111+
112+
set_option backward.isDefEq.respectTransparency false in
113+
variable {hcR hcM hcM' hcM''} in
114+
lemma ιM_jointly_surjective₃ (m : ModuleColimit hcR hcM) (m' : ModuleColimit hcR hcM')
115+
(m'' : ModuleColimit hcR hcM'') :
116+
∃ (U : Cᵒᵖ) (x : M.obj U) (x' : M'.obj U) (x'' : M''.obj U),
117+
ιM x = m ∧ ιM x' = m' ∧ ιM x'' = m'' := by
118+
obtain ⟨U, ⟨x, x', x''⟩, h⟩ := Types.jointly_surjective_of_isColimit
119+
((isColimitOfPreserves (forget AddCommGrpCat) hcM).tensor
120+
((isColimitOfPreserves (forget AddCommGrpCat) hcM').tensor
121+
(isColimitOfPreserves (forget AddCommGrpCat) hcM''))) ⟨m, m', m''⟩
122+
rw [Prod.ext_iff, Prod.ext_iff] at h
123+
obtain ⟨rfl, rfl, rfl⟩ := h
124+
exact ⟨U, x, x', x'', rfl, rfl, rfl⟩
125+
126+
include hcR in
127+
lemma ιR_jointly_surjective (r : cR.pt) :
128+
∃ (U : Cᵒᵖ) (a : R.obj U), ιR cR a = r :=
129+
Types.jointly_surjective_of_isColimit
130+
(isColimitOfPreserves (forget RingCat) hcR) r
131+
132+
set_option backward.isDefEq.respectTransparency false in
133+
variable {hcR hcM} in
134+
lemma jointly_surjective₂ (r : cR.pt) (m : ModuleColimit hcR hcM) :
135+
∃ (U : Cᵒᵖ) (a : R.obj U) (x : M.obj U),
136+
ιR cR a = r ∧ ιM x = m := by
137+
obtain ⟨U, ⟨a, x⟩, h⟩ := Types.jointly_surjective_of_isColimit
138+
((isColimitOfPreserves (forget RingCat) hcR).tensor
139+
(isColimitOfPreserves (forget AddCommGrpCat) hcM)) ⟨r, m⟩
140+
rw [Prod.ext_iff] at h
141+
obtain ⟨rfl, rfl⟩ := h
142+
exact ⟨U, a, x, rfl, rfl⟩
143+
144+
set_option backward.isDefEq.respectTransparency false in
145+
variable {hcR hcM} in
146+
lemma jointly_surjective₃ (r₁ r₂ : cR.pt) (m : ModuleColimit hcR hcM) :
147+
∃ (U : Cᵒᵖ) (a₁ a₂ : R.obj U) (x : M.obj U),
148+
ιR cR a₁ = r₁ ∧ ιR cR a₂ = r₂ ∧ ιM x = m := by
149+
obtain ⟨U, ⟨a₁, a₂, x⟩, h⟩ := Types.jointly_surjective_of_isColimit
150+
((isColimitOfPreserves (forget RingCat) hcR).tensor
151+
((isColimitOfPreserves (forget RingCat) hcR).tensor
152+
(isColimitOfPreserves (forget AddCommGrpCat) hcM))) ⟨r₁, r₂, m⟩
153+
rw [Prod.ext_iff, Prod.ext_iff] at h
154+
obtain ⟨rfl, rfl, rfl⟩ := h
155+
exact ⟨U, a₁, a₂, x, rfl, rfl, rfl⟩
156+
157+
set_option backward.isDefEq.respectTransparency false in
158+
variable {hcR hcM hcM'} in
159+
lemma jointly_surjective₃' (r : cR.pt) (m₁ : ModuleColimit hcR hcM) (m₂ : ModuleColimit hcR hcM') :
160+
∃ (U : Cᵒᵖ) (a : R.obj U) (x₁ : M.obj U) (x₂ : M'.obj U),
161+
ιR cR a = r ∧ ιM x₁ = m₁ ∧ ιM x₂ = m₂ := by
162+
obtain ⟨U, ⟨a, x₁, x₂⟩, h⟩ := Types.jointly_surjective_of_isColimit
163+
((isColimitOfPreserves (forget RingCat) hcR).tensor
164+
((isColimitOfPreserves (forget AddCommGrpCat) hcM).tensor
165+
(isColimitOfPreserves (forget AddCommGrpCat) hcM'))) ⟨r, m₁, m₂⟩
166+
rw [Prod.ext_iff, Prod.ext_iff] at h
167+
obtain ⟨rfl, rfl, rfl⟩ := h
168+
exact ⟨U, a, x₁, x₂, rfl, rfl, rfl⟩
169+
170+
noncomputable instance : Module cR.pt (ModuleColimit hcR hcM) where
171+
mul_smul r₁ r₂ m := by
172+
obtain ⟨U, r₁, r₂, m, rfl, rfl, rfl⟩ := jointly_surjective₃ r₁ r₂ m
173+
simp only [smul_eq, ← mul_smul, ← map_mul]
174+
one_smul m := by
175+
obtain ⟨U, m, rfl⟩ := ιM_jointly_surjective m
176+
simpa using smul_eq hcR hcM 1 m
177+
zero_smul m := by
178+
obtain ⟨U, m, rfl⟩ := ιM_jointly_surjective m
179+
simpa using smul_eq hcR hcM 0 m
180+
smul_zero r := by
181+
obtain ⟨U, r, rfl⟩ := ιR_jointly_surjective hcR r
182+
simpa using smul_eq hcR hcM r 0
183+
smul_add r m₁ m₂ := by
184+
obtain ⟨U, r, m₁, m₂, rfl, rfl, rfl⟩ := jointly_surjective₃' r m₁ m₂
185+
simp only [smul_eq, smul_add, ← map_add]
186+
add_smul r₁ r₂ m := by
187+
obtain ⟨U, r₁, r₂, m, rfl, rfl, rfl⟩ := jointly_surjective₃ r₁ r₂ m
188+
simp only [smul_eq, ← map_add, add_smul]
189+
190+
section
191+
192+
variable {M' : PresheafOfModules.{w} R} {cM' : Cocone M'.presheaf}
193+
(hcM' : IsColimit cM')
194+
195+
/-- The linear map between the colimit modules induced by a morphism of modules. -/
196+
noncomputable def map (f : M ⟶ M') :
197+
ModuleColimit hcR hcM →ₗ[cR.pt] ModuleColimit hcR hcM' where
198+
toFun := hcM.desc ((Cocone.precompose ((toPresheaf _).map f)).obj cM')
199+
map_add' _ _ := map_add _ _ _
200+
map_smul' r m := by
201+
obtain ⟨U, r, m, rfl, rfl⟩ := ModuleColimit.jointly_surjective₂ r m
202+
let c := (Cocone.precompose ((toPresheaf _).map f)).obj cM'
203+
have h₁ := ConcreteCategory.congr_hom (hcM.fac c U) (r • m)
204+
have h₂ := ConcreteCategory.congr_hom (hcM.fac c U) m
205+
dsimp [c] at h₁ h₂ ⊢
206+
rw [ModuleColimit.smul_eq]
207+
erw [h₁, h₂, ModuleColimit.smul_eq, ← (f.app U).hom.map_smul]
208+
rfl
209+
210+
@[simp]
211+
lemma map_apply (f : M ⟶ M') {U : Cᵒᵖ} (m : M.obj U) :
212+
dsimp% map hcR hcM hcM' f (ιM m) = ιM (f.app _ m) :=
213+
ConcreteCategory.congr_hom (hcM.fac ((Cocone.precompose ((toPresheaf _).map f)).obj cM') U) m
214+
215+
@[simp]
216+
lemma map_id : map hcR hcM hcM (𝟙 M) = .id := by
217+
ext m
218+
obtain ⟨U, m, rfl⟩ := ιM_jointly_surjective m
219+
simp
220+
221+
lemma comp_map
222+
(f : M ⟶ M')
223+
{M'' : PresheafOfModules.{w} R} {cM'' : Cocone M''.presheaf}
224+
(hcM'' : IsColimit cM'') (g : M' ⟶ M'') :
225+
(map hcR hcM' hcM'' g).comp (map hcR hcM hcM' f) = map hcR hcM hcM'' (f ≫ g) := by
226+
ext m
227+
obtain ⟨U, m, rfl⟩ := ιM_jointly_surjective m
228+
simp
229+
230+
end
231+
232+
end ModuleColimit
233+
234+
end
235+
236+
/-- The colimit module functor from the category of presheaves of modules
237+
over a presheaf of rings `R` on a cofiltered category to the category
238+
of modules over a colimit of `R`. -/
239+
noncomputable def colimitFunctor : PresheafOfModules.{w} R ⥤ ModuleCat.{w} cR.pt where
240+
obj M := ModuleCat.of _ (ModuleColimit hcR (colimit.isColimit M.presheaf))
241+
map f := ModuleCat.ofHom (ModuleColimit.map _ _ _ f)
242+
map_comp f g := by ext : 1; exact (ModuleColimit.comp_map ..).symm
243+
244+
end PresheafOfModules

‎Mathlib/CategoryTheory/Filtered/FinallySmall.lean‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Joël Riou
66
module
77

88
public import Mathlib.CategoryTheory.Limits.FinallySmall
9+
public import Mathlib.CategoryTheory.Limits.Preserves.Filtered
910

1011
/-!
1112
# Finally small filtered categories
@@ -101,6 +102,14 @@ noncomputable def fromFilteredFinalModel : FilteredFinalModel.{w} C ⥤ C :=
101102
instance : (fromFilteredFinalModel.{w} C).Final :=
102103
(exists_of_isFiltered.{w} C).choose_spec.choose_spec.choose_spec.choose_spec
103104

105+
open Limits in
106+
lemma preservesColimitsOfShape_of_isFiltered
107+
{D E : Type*} [Category* D] [Category* E]
108+
(F : D ⥤ E) [PreservesFilteredColimitsOfSize.{w, w} F] :
109+
PreservesColimitsOfShape C F :=
110+
Functor.Final.preservesColimitsOfShape_of_final
111+
(FinallySmall.fromFilteredFinalModel.{w} C) _
112+
104113
end FinallySmall
105114

106115
namespace InitiallySmall

0 commit comments

Comments
 (0)