# Zulip Chat Archive

## Stream: maths

### Topic: plus construction

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

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

#### 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

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

#### 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

#### Reid Barton (Aug 12 2019 at 14:13):

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

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

#### Reid Barton (Aug 12 2019 at 16:13):

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

#### Scott Morrison (Aug 12 2019 at 22:29):

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

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

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

#### 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

#### 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

#### 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)`

.

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

#### Scott Morrison (Aug 14 2019 at 07:55):

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

#### 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)`

.

#### Reid Barton (Aug 14 2019 at 13:18):

I feel like added generality almost always makes life simpler

#### Scott Morrison (Aug 14 2019 at 21:30):

:-)

Last updated: May 10 2021 at 07:15 UTC