Skip to content

Commit 01749d4

Browse files
chrisflavchrisflav
committed
chore(Algebra/Category/Sheaf): remove superfluous HasSheafCompose assumptions (leanprover-community#41152)
Since leanprover-community#41151, we have that the forgetful functor from `RingCat` to `AddCommGrpCat` has a left-adjoint, so it preserves limits of arbitrary size. This implies that `HasSheafCompose` is now automatic for this functor.
1 parent 8406f7a commit 01749d4

7 files changed

Lines changed: 12 additions & 38 deletions

File tree

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Joël Riou
55
-/
66
module
77

8+
public import Mathlib.Algebra.Category.AlgCat.TensorAlgebra
89
public import Mathlib.Algebra.Category.ModuleCat.Presheaf
910
public import Mathlib.Algebra.Category.ModuleCat.Limits
1011
public import Mathlib.CategoryTheory.Sites.LocallyBijective
@@ -166,8 +167,6 @@ def sectionsFunctor : SheafOfModules.{v} R ⥤ Type _ where
166167
obj M := M.sections
167168
map f := ↾(sectionsMap f)
168169

169-
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
170-
171170
variable (R) in
172171
/-- The obvious free sheaf of modules of rank `1`. -/
173172
@[simps]

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

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,6 @@ open CategoryTheory Limits
3232

3333
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C} {R : Sheaf J RingCat.{u}}
3434
[HasWeakSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
35-
[J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
3635

3736
namespace SheafOfModules
3837

@@ -175,7 +174,6 @@ section
175174

176175
variable {C' : Type u₂} [Category.{v₂} C'] {J' : GrothendieckTopology C'} {S : Sheaf J' RingCat.{u}}
177176
[HasSheafify J' AddCommGrpCat.{u}] [J'.WEqualsLocallyBijective AddCommGrpCat.{u}]
178-
[J'.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
179177
(F : SheafOfModules.{u} R ⥤ SheafOfModules.{u} S) (I : Type u)
180178

181179
/-- Let `F` be a functor from the category of sheaves of `R`-modules to sheaves of `S`-modules.

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

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,6 @@ open CategoryTheory Limits
3535

3636
variable {C : Type u'} [Category.{v'} C] {J : GrothendieckTopology C} {R : Sheaf J RingCat.{u}}
3737
[HasWeakSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
38-
[J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
3938

4039
namespace SheafOfModules
4140

@@ -108,7 +107,6 @@ section
108107

109108
variable [∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat.{u}]
110109
[∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
111-
[∀ (X : C), (J.over X).HasSheafCompose (forget₂ RingCat AddCommGrpCat.{u})]
112110

113111
/-- The data of generating sections of the restriction of a sheaf of modules
114112
over a covering of the terminal object. -/
@@ -151,7 +149,6 @@ noncomputable section
151149

152150
variable {C' : Type u₁} [Category.{v₁} C'] {J' : GrothendieckTopology C'} {S : Sheaf J' RingCat.{u}}
153151
[HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat]
154-
[J'.HasSheafCompose (forget₂ RingCat AddCommGrpCat)]
155152

156153
variable {M : SheafOfModules.{u} R} (G : M.GeneratingSections)
157154
(F : SheafOfModules.{u} R ⥤ SheafOfModules.{u} S) [PreservesColimitsOfSize.{u, u} F]
@@ -189,8 +186,7 @@ instance [IsIso G.π] : IsIso (G.map F η).π := by
189186
rw [GeneratingSections.map_π_eq]
190187
infer_instance
191188

192-
variable [∀ X, (J.over X).HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
193-
[∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}] [HasBinaryProducts C]
189+
variable [∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}] [HasBinaryProducts C]
194190
[∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
195191

196192
/-- Given `G : M.GeneratingSections`, we naturally obtain `M.LocalGeneratorsData` using the

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

Lines changed: 3 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -37,8 +37,7 @@ namespace SheafOfModules
3737

3838
section
3939

40-
variable [∀ X, (J.over X).HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
41-
[∀ X, HasWeakSheafify (J.over X) AddCommGrpCat.{u}]
40+
variable [∀ X, HasWeakSheafify (J.over X) AddCommGrpCat.{u}]
4241
[∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
4342

4443
namespace LocalGeneratorsData
@@ -70,7 +69,6 @@ end
7069
section
7170

7271
variable [HasWeakSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
73-
[J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
7472

7573
/-- The generating sections of the free sheaf of modules. -/
7674
@[expose, simps]
@@ -91,8 +89,7 @@ instance (I : Type u) : IsIso (free.generatingSections (R := R) I).π := by
9189
rw [free.generatingSections_π]
9290
infer_instance
9391

94-
variable [∀ X, (J.over X).HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
95-
[∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}] [HasBinaryProducts C]
92+
variable [∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}] [HasBinaryProducts C]
9693
[∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}] [HasSheafify J AddCommGrpCat]
9794

9895
set_option backward.defeqAttrib.useBackward true in
@@ -110,8 +107,7 @@ end
110107

111108
section
112109

113-
variable [∀ X, (J.over X).HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
114-
[∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}]
110+
variable [∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}]
115111
[∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
116112

117113
namespace LocalGeneratorsData

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

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -55,9 +55,6 @@ lemma bijective_pushforwardSections [F.Final] :
5555
Function.Bijective (pushforwardSections φ (M := M)) :=
5656
Functor.bijective_sectionsPrecomp _ _
5757

58-
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
59-
[K.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
60-
6158
/-- The canonical morphism `unit S ⟶ (pushforward.{u} φ).obj (unit R)`
6259
of sheaves of modules corresponding to a continuous map between ringed sites. -/
6360
noncomputable def unitToPushforwardObjUnit : unit S ⟶ (pushforward.{u} φ).obj (unit R) where

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

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -88,9 +88,7 @@ noncomputable def overFunctorMap {X Y : D} (f : X ⟶ Y) :
8888

8989
/-- The pushforward of `R.over Y` along `Over.map f` is isomorphic to `R.over X`. -/
9090
@[simps! +dsimpLhs]
91-
noncomputable def overMapUnitIso {X Y : D}
92-
[(K.over X).HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
93-
[(K.over Y).HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})] (f : X ⟶ Y) :
91+
noncomputable def overMapUnitIso {X Y : D} (f : X ⟶ Y) :
9492
(overMap.{u} R f).obj (.unit (R.over Y)) ≅ .unit (R.over X) :=
9593
Iso.refl _
9694

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

Lines changed: 6 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,6 @@ namespace SheafOfModules
3636
section
3737

3838
variable [HasWeakSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
39-
[J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
4039

4140
/-- A global presentation of a sheaf of modules `M` consists of a family `generators.s`
4241
of sections `s` which generate `M`, and a family of sections which generate
@@ -66,7 +65,7 @@ noncomputable section
6665

6766
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C} {R : Sheaf J RingCat.{u}}
6867
[HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat]
69-
[J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] {ι σ : Type u}
68+
{ι σ : Type u}
7069

7170
/-- Given two morphisms of sheaves of `R`-modules `f : free ι ⟶ free σ` and `g : free σ ⟶ M`
7271
satisfying `H : f ≫ g = 0` and `IsColimit (CokernelCofork.ofπ g H)`, we obtain
@@ -144,7 +143,6 @@ instance {M N : SheafOfModules.{u} R} (f : M ⟶ N) [IsIso f]
144143

145144
variable {C' : Type u₂} [Category.{v₂} C'] {J' : GrothendieckTopology C'} {S : Sheaf J' RingCat.{u}}
146145
[HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat]
147-
[J'.HasSheafCompose (forget₂ RingCat AddCommGrpCat)]
148146

149147
variable {M : SheafOfModules.{u} R} (P : Presentation M)
150148
(F : SheafOfModules.{u} R ⥤ SheafOfModules.{u} S) [PreservesColimitsOfSize.{u, u} F]
@@ -194,8 +192,7 @@ end
194192

195193
section
196194

197-
variable [∀ X, (J.over X).HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
198-
[∀ X, HasWeakSheafify (J.over X) AddCommGrpCat.{u}]
195+
variable [∀ X, HasWeakSheafify (J.over X) AddCommGrpCat.{u}]
199196
[∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
200197

201198
/-- This structure contains the data of a family of objects `X i` which cover
@@ -289,11 +286,8 @@ section map
289286

290287
variable {D : Type u₂} [Category.{v₂, u₂} D] {K : GrothendieckTopology D}
291288
{S : Sheaf K RingCat.{u}} [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat]
292-
[∀ (X : D), (K.over X).HasSheafCompose (forget₂ RingCat AddCommGrpCat)]
293289

294-
variable [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)]
295-
[K.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
296-
[∀ (X : C), HasSheafify (J.over X) AddCommGrpCat.{u}]
290+
variable [∀ (X : C), HasSheafify (J.over X) AddCommGrpCat.{u}]
297291
[∀ (X : D), HasSheafify (K.over X) AddCommGrpCat.{u}]
298292

299293
variable (G : D ⥤ C) [G.IsContinuous K J] [G.IsCocontinuous K J]
@@ -368,10 +362,8 @@ open CategoryTheory Limits
368362

369363
variable {C : Type u₁} [Category.{v₁} C] [HasBinaryProducts C] {J : GrothendieckTopology C}
370364
{R : Sheaf J RingCat.{u}} [HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat]
371-
[J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)]
372365

373-
variable [∀ X, (J.over X).HasSheafCompose (forget₂ RingCat AddCommGrpCat)]
374-
[∀ X, HasSheafify (J.over X) AddCommGrpCat]
366+
variable [∀ X, HasSheafify (J.over X) AddCommGrpCat]
375367
[∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat]
376368

377369
/-- Given a sheaf of `R`-modules `M` and a `Presentation M`, we may construct the quasi-coherent
@@ -422,10 +414,8 @@ end
422414

423415
section bind
424416

425-
variable [∀ X, (J.over X).HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
426-
[∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}]
417+
variable [∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}]
427418
[∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
428-
[∀ X Y, ((J.over X).over Y).HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
429419
[∀ X Y, HasSheafify ((J.over X).over Y) AddCommGrpCat.{u}]
430420
[∀ X Y, ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat.{u}]
431421

@@ -454,7 +444,7 @@ lemma IsQuasicoherent.of_coversTop {R : Sheaf J RingCat.{u}}
454444
IsQuasicoherent.nonempty_quasicoherentData.some).isQuasicoherent
455445

456446
set_option backward.isDefEq.respectTransparency false in
457-
lemma isQuasicoherent_over [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
447+
lemma isQuasicoherent_over
458448
[HasPullbacks C] [HasBinaryProducts C] (M : SheafOfModules.{u} R) (X : C) [IsQuasicoherent M] :
459449
IsQuasicoherent (M.over X) :=
460450
isQuasicoherent_pushforward_of_isLeftAdjoint _ _ (Iso.refl _)

0 commit comments

Comments
 (0)