Stream: maths

Topic: Subspaces and opens

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?

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

Reid Barton (Mar 08 2019 at 17:20):

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

Ramon Fernandez Mir (Mar 08 2019 at 17:29):

What does convert do?

Patrick Massot (Mar 08 2019 at 17:30):

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

Ramon Fernandez Mir (Mar 08 2019 at 17:39):

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

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

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.

Johan Commelin (Mar 08 2019 at 18:19):

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

Kevin Buzzard (Mar 08 2019 at 18:20):

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

Kevin Buzzard (Mar 08 2019 at 18:20):

It's pushing forward which is the easy one

Johan Commelin (Mar 08 2019 at 18:20):

Oh, yep.. that's right.

Kevin Buzzard (Mar 08 2019 at 18:56):

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

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