Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 85d6221

Browse files
alreadydoneerdOne
alreadydone
and
erdOne
committed
refactor(topology/sheaf_condition): remove redundant constructions (#17378)
The constructions used to prove `is_sheaf_iff_is_sheaf_equalizer_products` in *sites.lean* is redundant because the equivalence can now be achieved via `is_sheaf` (site version) ↔ opens_le_cover ↔ pairwise_intersections ↔ equalizer_products. Refactoring the proof of this equivalence after removal of these constructions, however, requires rearranging the import chain and moving things around, explaining the large diff. The author @justus-springer of the constructions has previously [approved the removal](#11706 (comment)) in #11706. The universe levels in *equalizer_products.lean* are also fixed and generalized (a cover of a space should be indexed by a type in the same universe), leading to the addition of a few universe ascriptions. - [x] depends on: #17361 Co-authored-by: erd1 <the.erd.one@gmail.com> Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
1 parent a6d9c65 commit 85d6221

10 files changed

Lines changed: 483 additions & 835 deletions

File tree

‎src/category_theory/sites/cover_preserving.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -163,7 +163,7 @@ begin
163163
end
164164

165165
lemma compatible_preserving_of_downwards_closed (F : C ⥤ D) [full F] [faithful F]
166-
(hF : ∀ {c : C} {d : D} (f : d ⟶ F.obj c), Σ c', F.obj c' ≅ d) : compatible_preserving K F :=
166+
(hF : Π {c : C} {d : D} (f : d ⟶ F.obj c), Σ c', F.obj c' ≅ d) : compatible_preserving K F :=
167167
begin
168168
constructor,
169169
introv hx he,

‎src/topology/sheaves/forget.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Scott Morrison
55
-/
66
import category_theory.limits.preserves.shapes.products
7-
import topology.sheaves.sheaf_condition.sites
7+
import topology.sheaves.sheaf_condition.equalizer_products
88

99
/-!
1010
# Checking the sheaf condition on the underlying presheaf of types.
@@ -54,7 +54,7 @@ When `G` preserves limits, the sheaf condition diagram for `F` composed with `G`
5454
naturally isomorphic to the sheaf condition diagram for `F ⋙ G`.
5555
-/
5656
def diagram_comp_preserves_limits :
57-
diagram F U ⋙ G ≅ diagram (F ⋙ G) U :=
57+
diagram F U ⋙ G ≅ diagram.{v} (F ⋙ G) U :=
5858
begin
5959
fapply nat_iso.of_components,
6060
rintro ⟨j⟩,
@@ -82,7 +82,7 @@ When `G` preserves limits, the image under `G` of the sheaf condition fork for `
8282
is the sheaf condition fork for `F ⋙ G`,
8383
postcomposed with the inverse of the natural isomorphism `diagram_comp_preserves_limits`.
8484
-/
85-
def map_cone_fork : G.map_cone (fork F U) ≅
85+
def map_cone_fork : G.map_cone (fork.{v} F U) ≅
8686
(cones.postcompose (diagram_comp_preserves_limits G F U).inv).obj (fork (F ⋙ G) U) :=
8787
cones.ext (iso.refl _) (λ j,
8888
begin
@@ -168,7 +168,7 @@ begin
168168
-- image under `G` of the equalizer cone for the sheaf condition diagram.
169169
let c := fork (F ⋙ G) U,
170170
obtain ⟨hc⟩ := S U,
171-
let d := G.map_cone (equalizer.fork (left_res F U) (right_res F U)),
171+
let d := G.map_cone (equalizer.fork (left_res.{v} F U) (right_res F U)),
172172
letI := preserves_smallest_limits_of_preserves_limits G,
173173
have hd : is_limit d := preserves_limit.preserves (limit.is_limit _),
174174
-- Since both of these are limit cones

‎src/topology/sheaves/functors.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Junyan Xu
55
-/
66

7-
import topology.sheaves.sheaf_condition.opens_le_cover
7+
import topology.sheaves.sheaf_condition.pairwise_intersections
88

99
/-!
1010
# functors between categories of sheaves

‎src/topology/sheaves/limits.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Scott Morrison
55
-/
6-
import topology.sheaves.sheaf_condition.sites
6+
import topology.sheaves.sheaf
77
import category_theory.sites.limits
88
import category_theory.adjunction
99
import category_theory.limits.functor_category

‎src/topology/sheaves/operations.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@ import algebra.category.Ring.filtered_colimits
99
import algebra.category.Group.limits
1010
import ring_theory.localization.basic
1111
import topology.sheaves.sheafify
12-
import topology.sheaves.sheaf_condition.sites
1312

1413
/-!
1514

‎src/topology/sheaves/sheaf.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Scott Morrison
55
-/
6-
import topology.sheaves.sheaf_condition.equalizer_products
6+
import topology.sheaves.presheaf
77
import category_theory.full_subcategory
88
import category_theory.limits.unit
99
import category_theory.sites.sheaf
@@ -44,8 +44,6 @@ variables {X : Top.{w}} (F : presheaf C X) {ι : Type v} (U : ι → opens X)
4444

4545
namespace presheaf
4646

47-
open sheaf_condition_equalizer_products
48-
4947
/--
5048
The sheaf condition has several different equivalent formulations.
5149
The official definition chosen here is in terms of grothendieck topologies so that the results on
@@ -64,11 +62,13 @@ The equivalent formulations of the sheaf condition on `presheaf C X` are as foll
6462
See `Top.presheaf.is_sheaf_iff_is_sheaf_equalizer_products`.
6563
6664
3. `Top.presheaf.is_sheaf_opens_le_cover`:
67-
Each `F(U)` is the (inverse) limit of all `F(V)` with `V ⊆ U`.
65+
For each open cover `{ Uᵢ }` of `U`, `F(U)` is the limit of the diagram consisting of arrows
66+
`F(V₁) ⟶ F(V₂)` for every pair of open sets `V₁ ⊇ V₂` that are contained in some `Uᵢ`.
6867
See `Top.presheaf.is_sheaf_iff_is_sheaf_opens_le_cover`.
6968
7069
4. `Top.presheaf.is_sheaf_pairwise_intersections`:
71-
For each open cover `{ Uᵢ }` of `U`, `F(U)` is the limit of all `F(Uᵢ)` and all `F(Uᵢ ∩ Uⱼ)`.
70+
For each open cover `{ Uᵢ }` of `U`, `F(U)` is the limit of the diagram consisting of arrows
71+
from `F(Uᵢ)` and `F(Uⱼ)` to `F(Uᵢ ∩ Uⱼ)` for each pair `(i, j)`.
7272
See `Top.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections`.
7373
7474
The following requires `C` to be concrete and complete, and `forget C` to reflect isomorphisms and

0 commit comments

Comments
 (0)