[Merged by Bors] - feat(topology/sheaves): Induced map on stalks #7092

justus-springer · 2021-04-07T18:37:04Z

This PR defines stalk maps for morphisms of presheaves. We prove that a morphism of type-valued sheaves is an isomorphism if and only if all the stalk maps are isomorphisms.

A few more lemmas about unique gluing are also added, as well as docstrings.

Zulip:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/induced.20map.20on.20stalks

Some of this can obviously be extended or stated in greater generality. For example, we might want a Lemma saying that a morphism of sheaves is mono/epi if and only if all stalk maps are mono/epi (this should even hold in more general categories than Type I think). This wasn't necessary for the goal I had in mind, but I'm happy to continue working on stuff like this and I'm grateful for any feedback.

Also, this about doubled the size of the file stalks.lean, so I took the liberty to add myself to the authors list. I hope this is okay.

…nique gluing

jcommelin

Only quickly skimmed it. But at first sight this looks great!

src/topology/sheaves/stalks.lean

src/topology/sheaves/sheaf_condition/unique_gluing.lean

src/topology/sheaves/stalks.lean

src/topology/sheaves/sheaf_condition/unique_gluing.lean

Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>

src/topology/sheaves/stalks.lean

src/topology/sheaves/sheaf_condition/unique_gluing.lean

semorrison · 2021-04-10T02:12:08Z

There are still some names to fix up here. There are many appearances of stalk_maps, which probably should all be stalk_functor_map.

Otherwise, this is looking really good!

justus-springer · 2021-04-10T10:07:48Z

Okay, fixed the names. I also reordered things in the file a little. I think it makes more sense that way and now it lines up with the module docstring.

semorrison · 2021-04-11T11:20:26Z

src/topology/sheaves/sheaf_condition/unique_gluing.lean

+@[simp] lemma res_π_apply (i : ι) (s : F.obj (op (supr U))) :
+  limit.π (discrete.functor (λ i : ι, F.obj (op (U i)))) i (res F U s) =
+  F.map (opens.le_supr U i).op s :=
+congr_fun (res_π F U i) s


You should be able to get this lemma automatically now by just putting @[elementwise] on res_π.

semorrison · 2021-04-11T11:22:17Z

src/topology/sheaves/stalks.lean

+@[simp] lemma stalk_functor_map_germ_apply (U : opens X) (x : U) {F G : X.presheaf (Type v)}
+  (f : F ⟶ G) (s : F.obj (op U)) :
+  (stalk_functor (Type v) x.1).map f (germ F x s) = germ G x (f.app (op U) s) :=
+congr_fun (stalk_functor_map_germ U x f) s


Similarly this can also be by @[elementwise].

I tried this, unfortunately the generated simp lemmas don't fire where I would like them to. There seems to be some issue with the coercions coe_fn, not even erw worked. The only way I found was through some pretty annoying unfolding of definitions, before I could rewrite, like this:

lemma app_injective_of_stalk_functor_map_injective {F : sheaf (Type v) X} {G : presheaf (Type v) X} (f : F.presheaf ⟶ G) (h : ∀ x : X, injective ((stalk_functor (Type v) x).map f)) (U : opens X) : injective (f.app (op U)) := λ s t hst, begin apply section_ext, intro x, apply h x.1, have := stalk_functor_map_germ_apply U x f s, -- here, I need to explicitly unfold the coercions before I can rewrite... dsimp [coe_fn, concrete_category.has_coe_to_fun, forget, concrete_category.forget] at this, erw this, sorry end

Maybe we can try to solve this in a separate PR?

Sounds good!

semorrison · 2021-04-11T11:25:04Z

Once you've fixed up the @[elementwise] things, you can ask bors to merge.

bors d+

bors · 2021-04-11T11:25:05Z

✌️ justus-springer can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

semorrison · 2021-04-14T12:23:42Z

bors merge

This PR defines stalk maps for morphisms of presheaves. We prove that a morphism of type-valued sheaves is an isomorphism if and only if all the stalk maps are isomorphisms. A few more lemmas about unique gluing are also added, as well as docstrings.

bors · 2021-04-14T16:20:02Z

Build failed (retrying...):

Run tests

This PR defines stalk maps for morphisms of presheaves. We prove that a morphism of type-valued sheaves is an isomorphism if and only if all the stalk maps are isomorphisms. A few more lemmas about unique gluing are also added, as well as docstrings.

bors · 2021-04-14T23:14:05Z

Pull request successfully merged into master.

Build succeeded:

@justus-springer

These fixes, while an improvement, still don't fix the problem @justus-springer observed in #7092. Really we should generate a second copy of the `_apply` lemma, with the category specialized to `Type u`, and in that one remove all the coercions. Maybe later. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

…8000) Refactoring and speeding up some of my code on stalk maps from #7092.

justus-springer added 13 commits March 29, 2021 13:49

feat(topology/sheaves/sheaf_condition): Sheaf condition in terms of u…

7065a57

…nique gluing

make the linter happy

41f6722

fix typo in theorem name

41620ec

lint

d8b8aeb

fix another typo

2c9f99f

now its correct

4727852

refactor(topology/sheaves): Refactor proofs of the sheaf condition

8182398

lint

85e687d

feat(topology/sheaves): Induced map on stalks

cca77c6

Merge branch 'master' into stalk_map

59038a0

lint

8271556

some fixes

a0b3db5

change def to lemma

41b5750

justus-springer added the awaiting-review The author would like community review of the PR label Apr 7, 2021

justus-springer requested a review from semorrison April 7, 2021 19:05

jcommelin reviewed Apr 7, 2021

View reviewed changes

src/topology/sheaves/stalks.lean Outdated Show resolved Hide resolved

ericrbg reviewed Apr 7, 2021

View reviewed changes

src/topology/sheaves/stalks.lean Outdated Show resolved Hide resolved