# Zulip Chat Archive

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