Zulip Chat Archive

Stream: maths

Topic: Subspaces and opens


view this post on Zulip Ramon Fernandez Mir (Mar 08 2019 at 17:16):

I'm having a very hard time with something which I thought would take an hour. I have a topological space X and an open subset U : opens X. I define a presheaf on X as map from opens X to some type plus some properties as follows:

structure presheaf (X : Type u) [T : topological_space X] :=
(F     : opens X  Type v)
(res   :  (U V) (HVU : V  U), F U  F V)
(Hid   :  (U), res U U (set.subset.refl U) = id)
(Hcomp :  (U V W) (HWV : W  V) (HVU : V  U), res U W (set.subset.trans HWV HVU) = res V W HWV  res U V HVU)

Now suppose that I have OX : sheaf X (presheaf as above + sheaf axiom). I want to define the restriction sheaf, of type sheaf U (or sheaf {x // x ∈ U}). I have a map f : opens X → opens U which is just subtype.val with the proof that it preserves is_open. I have defined the restricted presheaf in the obvious way using f. Is this the right way to work with subspaces? Am I missing something already in mathlib?

The reason why I think that I might be doing something very wrong is because when I try to prove the sheaf condition, at some point I have a goal that looks like:

⊢ OX.res (f Uj) ((f Uj) ∩ (f Uk)) _ (s j) = OX.res (f Uk) ((f Uj) ∩ (f Uk)) _ (s k)

And in my hypotheses I have:

H : OX.res (f Uj) (f (Uj ∩ Uk)) _ (s j) = OX.res (f Uk) (f (Uj ∩ Uk)) _ (s k)

I also have a lemma that says:

 lemma f.inter :  {V W}, (f U (V  W)) = (f U V)  (f U W)

So I thought that rewriting at H would do the trick but I get:

[check] application type mismatch at
  OX.res (f Uj) _a _
argument type
  f (Uj ∩ Uk) ⊆ f Uj
expected type
  _a ⊆ f Uj

Any suggestions?

view this post on Zulip Reid Barton (Mar 08 2019 at 17:20):

You can't rewrite H with that lemma because there are proof terms (the _s) whose types depend on the things you want to rewrite.
Try convert H instead

view this post on Zulip Reid Barton (Mar 08 2019 at 17:20):

At least, I think that's the problem. I don't recognize your error message though.

view this post on Zulip Ramon Fernandez Mir (Mar 08 2019 at 17:29):

What does convert do?

view this post on Zulip Patrick Massot (Mar 08 2019 at 17:30):

https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md#convert

view this post on Zulip Ramon Fernandez Mir (Mar 08 2019 at 17:39):

Thanks! I should get more familiar with many of these..

view this post on Zulip Mario Carneiro (Mar 08 2019 at 18:08):

that error message is what you get if you get the rewrite motive is not type correct error and then follow the error's advice and set_option trace.check true

view this post on Zulip Kevin Buzzard (Mar 08 2019 at 18:18):

Hi. Sorry, I was chairing a meeting and watching these interesting messages go by. I think you should make a more general construction than this. I think you should define the pullback sheaf, or comap sheaf as it will be called in this world, for an open immersion. Because at some point when defining a scheme you're going to need to pull a sheaf back along an isomorphism so you're going to have to write that code anyway.

view this post on Zulip Johan Commelin (Mar 08 2019 at 18:19):

Might as well do pullback of sheaves in general in that case.

view this post on Zulip Kevin Buzzard (Mar 08 2019 at 18:20):

But that's harder because then you have to take some limit

view this post on Zulip Kevin Buzzard (Mar 08 2019 at 18:20):

It's pushing forward which is the easy one

view this post on Zulip Johan Commelin (Mar 08 2019 at 18:20):

Oh, yep.. that's right.

view this post on Zulip Kevin Buzzard (Mar 08 2019 at 18:56):

I had to deal with all this with schemes the first time around :-)

view this post on Zulip Kevin Buzzard (Mar 08 2019 at 19:02):

I was idly wondering whether pullbacks are easy for an open map (image of open is open) but the naive definition isn't a sheaf, it seems to me (f(U intersect V) might not be f(U) intersect f(V)). So maybe open immersions are the correct generality.


Last updated: May 11 2021 at 00:31 UTC