Zulip Chat Archive

Stream: maths

Topic: plus construction


view this post on Zulip Scott Morrison (Aug 12 2019 at 14:10):

@Reid Barton, I just ran into what may be a universe problem, or may just be me being sleepy. I'm trying to do the plus construction, working towards sheafification.

view this post on Zulip Scott Morrison (Aug 12 2019 at 14:10):

Unfortunately the category of covers of an open set U looks to be one universe level too high for me to be able to take the colimit over it... :-(

view this post on Zulip Scott Morrison (Aug 12 2019 at 14:11):

I actually have to run now, but in case you're interested my work is at https://github.com/leanprover-community/mathlib/blob/sheaves/src/topology/Top/presheaf/plus.lean

view this post on Zulip Scott Morrison (Aug 12 2019 at 14:12):

and I'm following https://stacks.math.columbia.edu/tag/00W1 (but just for a topological space, not a site).

view this post on Zulip Reid Barton (Aug 12 2019 at 14:12):

If your covers are families indexed on a type then it sounds correct that the category of covers is only essentially small

view this post on Zulip Reid Barton (Aug 12 2019 at 14:13):

And that only if you restrict to finite covers or covers with some cardinality bound

view this post on Zulip Reid Barton (Aug 12 2019 at 16:13):

@Scott Morrison Have you looked through Section 7.6 (https://stacks.math.columbia.edu/tag/00VG) and in particular 7.6.3, 7.6.4 and https://stacks.math.columbia.edu/tag/000X?

view this post on Zulip Reid Barton (Aug 12 2019 at 16:13):

The last (Lemma 3.11.1) is an unabashedly set-theoretic way of addressing the issue

view this post on Zulip Scott Morrison (Aug 12 2019 at 22:29):

Thanks for the references. I hadn't been expecting this difficulty! :-)

view this post on Zulip Scott Morrison (Aug 12 2019 at 22:31):

Lemma 3.11.1 seems to really require working with general sites --- is it really the case that I can't do this "colimit of covers, of zeroth-Cech cohomology" version of plus construction while working solely with open sets in a topological space?

view this post on Zulip Scott Morrison (Aug 12 2019 at 22:35):

I really don't have the energy for such a set-theoretic diversion, so probably will either give up on trying to do sheafification, or try the "sections-of-stalks" approach given in https://stacks.math.columbia.edu/tag/007X. Hopefully that one has no set-theoretic issues?

view this post on Zulip Kevin Buzzard (Aug 12 2019 at 23:42):

I don't think Kenny or Ramon or any of us did sheafification using the more low level approach either

view this post on Zulip Kevin Buzzard (Aug 12 2019 at 23:43):

At some point we'll want higher cohomology of course. People are I guess already aware that cohomology of a space might end up one universe higher than the space if computed in certain ways

view this post on Zulip Reid Barton (Aug 13 2019 at 00:55):

I would suggest instead to work not directly with covers but with an arbitrary (small) collection of covering families. Then for the Zariski topology I think you can easily construct such a small collection with the correct sheaves by considering only "self-indexed" covers, that is, set (set X).

view this post on Zulip Scott Morrison (Aug 14 2019 at 07:54):

@Reid Barton, could you spell out a bit what you intended by

but with an arbitrary (small) collection of covering families.

Can I get away with just using the following poset?

def cover : Type v := set (opens X)

structure hom (c d : cover X) :=
(r : Π U, c U → ∃ V, U ⊆ V ∧ d V)

view this post on Zulip Scott Morrison (Aug 14 2019 at 07:55):

(I'm keen to avoid generality where possible on this first attempt at things. :-)

view this post on Zulip Scott Morrison (Aug 14 2019 at 10:08):

No, that goes wrong for other reasons... Think I sorted it out for now. I'm allowing covers indexed by arbitrary types, but when I do the plus construction I'm only doing the colimit over covers of the form set (opens X).

view this post on Zulip Reid Barton (Aug 14 2019 at 13:18):

I feel like added generality almost always makes life simpler

view this post on Zulip Scott Morrison (Aug 14 2019 at 21:30):

:-)


Last updated: May 10 2021 at 07:15 UTC