plus construction

Stream: maths

[Scott Morrison]

@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.

[Scott Morrison]

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... :-(

[Scott Morrison]

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

[Scott Morrison]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

@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?

[Reid Barton]

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

[Scott Morrison]

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

[Scott Morrison]

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?

[Scott Morrison]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

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).

[Scott Morrison]

@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)

[Scott Morrison]

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

[Scott Morrison]

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).

[Reid Barton]

I feel like added generality almost always makes life simpler

[Scott Morrison]

:-)