Gluing topological spaces

Stream: maths

[Andrew Yang]

Now that the road to the Spec-adjunction seems quite clear, I started thinking about how one would define fibered products of schemes.
The first road block is probably gluing topological spaces.
The most straightforward way is probably giving some glue_data such as

structure glue_data :=
  (ι : Type*)
  (U : ι → Type*)
  (h₁ : ∀ i, topological_space (U i))
  (V : Π i, ι → opens (U i))
  (f : Π i j, C(V i j, V j i))
  (h₂ : ∀ i, V i i = ⊤)
  (h₃ : ∀ i, (f i i).to_fun = id)
  (h₄ : ∀ ⦃i j⦄ k (x : V i j), x.val ∈ V i k → (f i j x).val ∈ V j k)
  (h₅ : ∀ i j k (x : V i j) (h : x.val ∈ V i k),
    (f j k ⟨(f i j x).val, h₄ k x h⟩).val = (f i k ⟨x.val, h⟩).val)

and spitting out a topological space (by quot), together with the immersions into it that covers it, the universal property, and the descriptions of the intersections of the image.

I believe that this approach would be quite messy as I would quite often need to consider elements of one subset as another, but I suppose that it doesn't really matter how it is constructed as long as the properties are proved. That said, I'm not experienced enough with Lean to make such a claim. Thus the questions are as follows.

1. Is there a better way to define the glue_data? (Of course the names of the conditions will change)
2. Is there a better (cleaner?) way to glue the data? (e.g. constructing diagrams and taking colimits, though I doubt this particular way would be better)

[Johan Commelin]

Note that mathlib knows that Top has arbitrary colimits.

[Johan Commelin]

Let me repost http://math.stanford.edu/~vakil/d/FOAG/BOfiber-prods.pdf which I think could serve as an informal blueprint to this result.

[Johan Commelin]

What is nice about these notes by Osserman is that he employs Zariski sheaves. This means that you can cut the problem into two steps: first you show that a Zariski sheaf is representable if it is locally representable. And secondly, you show that the fibre product is a Zariski sheaf that is locally representable by Spec(A ⊗ B).

[Andrew Yang]

Johan Commelin said:

Note that mathlib knows that Top has arbitrary colimits.

I did see that, but there is still some work needed on drawing out the diagrams and proving the other properties of the glued space. I'm not sure if this would be better.

[Scott Morrison]

It would be nice to use the colimits in Top. This application (gluing sheaves) is why they were implemented in the first place. :-)

I'm not sure if you've seen, but we in fact already have colimits in PresheafedSpace as well.

[Scott Morrison]

But regarding your glue_data above: I would hope that none of the .to_fun and .vals are required. Coercions should be taking care of all of those (and indeed, I'd hope that using coercions are the simp normal form, so you'll actually find it harder if you write out the data with explicit .to_funs).

[Andrew Yang]

If that's the case, I could use the colimits instead.
I've also edited the original post in regard to your suggestion. Hope that it looks better now.

[Scott Morrison]

I'm not promising that using colimits will be nice. After all I never did gluing of sheaves following this path. :-)

[Johan Commelin]

If we already have colimits in PresheafedSpace, I'm hoping we can use that + zariski sheaves to get a nice statement for schemes.

[Andrew Yang]

The draft is about done at #9864. I'm not sure if there are some crucial properties that I'm missing. Feel free to request some more.

[Reid Barton]

I feel like it's probably too "strict" to require the $V_{ij}$ to be actual subsets of the $U_i$. It would be better to glue along open immersions.

[Reid Barton]

One argument for this is that the maps $U_i \to X$ to the glued space should have the same sort of status as the original gluing maps $V_{ij} \to U_i$. However, we can't arrange to have $U_i \to X$ literally be an open subset.

[Reid Barton]

One thing that might be a bit annoying is expressing the condition that $\coprod_{i,j} V_{i,j} \to \coprod_i U_i$ is an equivalence relation. In ordinary math, the simplest general definition is that $\mathrm{Hom}(Z, -)$ takes it to an equivalence relation of sets for any object $Z$. If you unwind that using what it means to map into an (open) embedding, it turns into a set-theoretic condition of the type you have here, plus the statements that $V_{ij} \to U_i$ and $V_{ij} \to U_j$ are jointly monic for each $(i,j)$--which is automatic if $V_{ij} \to U_i$ is already an embedding, but that doesn't have to be the case for more general kinds of gluing. Maybe it would be worth isolating this condition "is equivalence relation" and proving several equivalent characterizations.

[Reid Barton]

I note that one of the first things you do is define "The family of V i j as topological spaces indexed by ι × ι", so maybe it wouldn't be that big a change to take the V i j as spaces from the start.

[Reid Barton]

I think even for the sorts of constructions you'll want to do in AG you would rather be gluing along open immersions of schemes, e.g., prove that the map $\mathrm{Spec}\, R[1/a] \to \mathrm{Spec}\, R$ defined by functoriality of $\mathrm{Spec}$ is an open immersion, rather than poking around the construction of $\mathrm{Spec}\, R$ to find an open subset that you can identify with $\mathrm{Spec}\, R[1/a]$

[Andrew Yang]

Reid Barton said:

One thing that might be a bit annoying is expressing the condition that $\coprod_{i,j} V_{i,j} \to \coprod_i U_i$ is an equivalence relation. In ordinary math, the simplest general definition is that $\mathrm{Hom}(Z, -)$ takes it to an equivalence relation of sets for any object $Z$. If you unwind that using what it means to map into an (open) embedding, it turns into a set-theoretic condition of the type you have here, plus the statements that $V_{ij} \to U_i$ and $V_{ij} \to U_j$ are jointly monic for each $(i,j)$--which is automatic if $V_{ij} \to U_i$ is already an embedding, but that doesn't have to be the case for more general kinds of gluing. Maybe it would be worth isolating this condition "is equivalence relation" and proving several equivalent characterizations.

I'm not really sure what you mean by this section. Are you suggesting that we should do the followings?

1. Remove the cocycle condition from the structure gluing_data.
2. Let gluing_data be valued in arbitrary categories.
3. Prove that If $\mathrm{Hom}(Z, \coprod_{i,j} V_{i,j}) \rightrightarrows\mathrm{Hom}(Z, \coprod_i U_i)$ is an equivalence relation for each $Z$ then the immersions $U_i\to X$ is mono (or something similar as I'm not even sure if this is true)
4. Write out explicitly what 3. actually means in Top and provide suitable APIs.

[Andrew Yang]

I'm still not sure how to state the cocycle condition properly. As a parity with the case of glueing schemes would be better, I'm thinking them in terms of schemes.
Suppose we have scheme structures on $U_i$ and $V_{ij}$ with open immersions $f_{ij} : V_{ij} \to U_i$ and isomorphisms $t_{ij} : V_{ij} \cong V_{ji}$
Would it be better to state it in terms of the open subscheme of $U_i$ induced on $\mathrm{im}\,f_i \cap \mathrm{im}\,f_j$ and somehow lifting $t_{ij}$ onto these schemes, or about $V_{ij}$ restricted on $f_i^{-1}(\mathrm{im}\,f_j)$?

[Kevin Buzzard]

My instinct is that you should avoid subobjects if at all possible. When we tried gluing sheaves in 2018 we used subobjects and all it does is makes matters worse -- now as well as $V_{i,j}$ you have its image in $U_i$ and its image in $U_j$ as well as the corresponding images for $V_{j,i}$.

[Andrew Yang]

Would it be possible or practical to introduce $W_{i,j,k} \hookrightarrow V_{i, j}$ representing $U_{i, j} \cap U_{i, k}$ and assert that they (under permutations of indices) are all isomorphic to each other and these isomorphisms commutes with the transition maps?

[Adam Topaz]

You can use pullbacks for $W_{i,j,k}$

[Andrew Yang]

But I suppose I don't have pullbacks in schemes yet?

[Adam Topaz]

Oh, I thought were discussing topological spaces

[Andrew Yang]

Oh yes. But I think it would be better to have a parity between gluing spaces and gluing schemes, and using pullbacks here seems to only postpone the problem to when we are gluing schemes.

[Johan Commelin]

But if you want to abstract the notion of "gluing things", don't you just end up with some form of colimit?

[Adam Topaz]

Yes, it's a colimit, but you can't just take some random colimit of schemes

[Adam Topaz]

As for schemes, it should be easy to show that the pullback of two open immersions exist, even before showing that all pullbacks exist

[Adam Topaz]

And besides you would need this just for affine schemes for the pullback construction of schemes

[Adam Topaz]

https://stacks.math.columbia.edu/tag/023U

[Reid Barton]

The way I would think about it is that you need a map from $W_{i,j,k}$ to $V_{j,k}$ (both being subobjects of $U_j \times U_k$)

[Reid Barton]

Another way to phrase it is that if you apply the Yoneda embedding to everything in sight, you get a equivalence relation (in presheaves on whatever category). If the pullbacks happen to exist in the original category, then their images will be the pullbacks in the category of presheaves, but even if not, there's still a pullback in presheaves which knows the correct thing

[Reid Barton]

then, when the quotient presheaf is representable we call it the quotient $X$ in the original category, the properties of the glued thing are the ones you can read off from an equivalence relation quotient in a presheaf category (e.g., $V_{i,j} = U_i \times_X U_j$)

[Reid Barton]

wait that's totally not true

[Reid Barton]

It's true though if instead of presheaves, you work with sheaves for the topology which is generated by gluings of this kind

[Andrew Yang]

I would start looking into the option of stating the cocycle condition in terms of $V_{i,j} \times_{U_i} V_{i, k}$.
But I suppose there is still an option to require $V_{i, j}$ to be actual subsets of $U_i$ and manually identify the open immersions with the subscheme on the image when we actually want to glue things, since subobjects indeed complicate matters a lot as mentioned by Kevin Buzzard, and if the cocycle condition is stated in terms of subschemes, we would still have to do the identification one way or another when gluing.

[Reid Barton]

Wait @Kevin Buzzard what do you mean by "subobject"?

[Adam Topaz]

I assume Kevin means docs#open_embedding for Top.

[Kevin Buzzard]

I just meant some kind of V : set U

[Kevin Buzzard]

Because then you get V i j : set U i and V i j : set U j and they're not at all the same thing. That was the problem we ran into

[Reid Barton]

right, that's what I thought you meant from context

[Reid Barton]

but in category theory, "subobject" means (an equivalence class of) monos into something

[Kevin Buzzard]

Oh apologies. I'm just saying "use types not terms for $V_{i,j}$"

[Kevin Buzzard]

Either everything should be a type or everything should be a term. In the Coq odd order paper they made everything a term. Every group was a subgroup of a large ambient group. But this doesn't work for rings, so everything being a type is something we should be getting the hang of. We tried making some things types and some things terms when gluing sheaves and this was the worst of all worlds

[Reid Barton]

also, it hasn't come up yet but in algebraic spaces, $V_{i,j} \to U_i$ might not even be a monomorphism!

[Andrew Yang]

I've changed the definitions and the second draft is about finished over at #9864.