Subspaces and opens

Stream: maths

[Ramon Fernandez Mir]

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]

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]

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

[Ramon Fernandez Mir]

What does convert do?

[Patrick Massot]

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

[Ramon Fernandez Mir]

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

[Mario Carneiro]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

It's pushing forward which is the easy one

[Johan Commelin]

Oh, yep.. that's right.

[Kevin Buzzard]

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

[Kevin Buzzard]

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.