# Zulip Chat Archive

## Stream: general

### Topic: unfolding issue

#### Kevin Buzzard (May 22 2018 at 21:40):

`(presheaf_of_types_pullback_under_open_immersion {F := F, res := res, Hid := Hid, Hcomp := Hcomp} id _).res`

#### Kevin Buzzard (May 22 2018 at 21:40):

Why can't I unfold that?

#### Kevin Buzzard (May 22 2018 at 21:41):

`lam X, presheaf_of_types_pullback_under_open_immersion X f H`

is a function from a structure to itself

#### Kevin Buzzard (May 22 2018 at 21:42):

I explicitly write down the definition, I say what F and res and Hid and Hcomp are

#### Kevin Buzzard (May 22 2018 at 21:42):

I don't see any reason why Lean can't evaluate that res

#### Kevin Buzzard (May 22 2018 at 21:42):

My goal is `[mess above] == res`

#### Kevin Buzzard (May 22 2018 at 21:43):

and this should just unravel to be, hopefully, something trivial.

#### Kevin Buzzard (May 22 2018 at 21:43):

This is another one of those insane "trivial in maths, hard in Lean" things

#### Kevin Buzzard (May 22 2018 at 21:45):

I am trying to prove that if you pull back a sheaf by the identity function, you get the same sheaf

#### Kevin Buzzard (May 22 2018 at 21:45):

this statement is fraught with difficulties though

#### Kevin Buzzard (May 22 2018 at 21:45):

and this is definitely not refl

#### Kevin Buzzard (May 22 2018 at 21:45):

because I am claiming for example that F U = F (id '' U)

#### Chris Hughes (May 22 2018 at 22:21):

What's the definition of `presheaf_of_types_pullback_under_open_immersion`

? I think the functions like `.res`

only unfold when applied to something of the form `{F := _, ...}.res`

and not `x.res`

for example. Have you tried `show`

?

#### Chris Hughes (May 22 2018 at 22:22):

Is it because it doesn't know what the underscore is?

#### Kevin Buzzard (May 22 2018 at 22:25):

The underscore is a horrible proof term.

#### Kevin Buzzard (May 22 2018 at 22:25):

I have realised there's another approach

#### Kevin Buzzard (May 22 2018 at 22:25):

so this question is no longer relevant

#### Kevin Buzzard (May 22 2018 at 22:25):

Again I have to use something very counterintuitive to a mathematician

#### Kevin Buzzard (May 22 2018 at 22:26):

Instead of trying to claim that the identity map is a map `F U -> F (id '' U)`

#### Kevin Buzzard (May 22 2018 at 22:26):

I use the actual map `F U -> F (id '' U)`

which a mathematician would call "the identity map" but which in dependent type theory is known as "restriction from U to the open subset id '' U"

#### Kevin Buzzard (May 22 2018 at 22:28):

it's unbelievable

#### Kevin Buzzard (May 22 2018 at 22:28):

all my hitherto impossible goals magically become refl

#### Kevin Buzzard (May 22 2018 at 22:28):

⊢ {morphism := λ (U : set (X R)) (HU : is_open zariski.open U), ((zariski.structure_presheaf_of_rings R).to_presheaf_of_types).res U (id '' U) HU (eq.mpr (id (eq.rec (eq.refl (is_open zariski.open (id '' U))) (set.image_id U))) HU) (eq.mpr (id (eq.rec (eq.refl (id '' U ⊆ U)) (set.image_id U))) (set.subset.refl U)), commutes := λ (U V : set (X R)) (HU : is_open zariski.open U) (HV : is_open zariski.open V) (Hsub : V ⊆ U), eq.refl (((presheaf_of_rings_pullback_under_open_immersion (zariski.structure_presheaf_of_rings R) id H).to_presheaf_of_types).res U V HU HV Hsub ∘ (λ (HU : is_open zariski.open U), ((zariski.structure_presheaf_of_rings R).to_presheaf_of_types).res U (id '' U) HU (eq.mpr (id (eq.rec (eq.refl (is_open zariski.open (id '' U))) (set.image_id U))) HU) (eq.mpr (id (eq.rec (eq.refl (id '' U ⊆ U)) (set.image_id U))) (set.subset.refl U))) HU)}.morphism U HU (x * y) = {morphism := λ (U : set (X R)) (HU : is_open zariski.open U), ((zariski.structure_presheaf_of_rings R).to_presheaf_of_types).res U (id '' U) HU (eq.mpr (id (eq.rec (eq.refl (is_open zariski.open (id '' U))) (set.image_id U))) HU) (eq.mpr (id (eq.rec (eq.refl (id '' U ⊆ U)) (set.image_id U))) (set.subset.refl U)), commutes := λ (U V : set (X R)) (HU : is_open zariski.open U) (HV : is_open zariski.open V) (Hsub : V ⊆ U), eq.refl (((presheaf_of_rings_pullback_under_open_immersion (zariski.structure_presheaf_of_rings R) id H).to_presheaf_of_types).res U V HU HV Hsub ∘ (λ (HU : is_open zariski.open U), ((zariski.structure_presheaf_of_rings R).to_presheaf_of_types).res U (id '' U) HU (eq.mpr (id (eq.rec (eq.refl (is_open zariski.open (id '' U))) (set.image_id U))) HU) (eq.mpr (id (eq.rec (eq.refl (id '' U ⊆ U)) (set.image_id U))) (set.subset.refl U))) HU)}.morphism U HU x * {morphism := λ (U : set (X R)) (HU : is_open zariski.open U), ((zariski.structure_presheaf_of_rings R).to_presheaf_of_types).res U (id '' U) HU (eq.mpr (id (eq.rec (eq.refl (is_open zariski.open (id '' U))) (set.image_id U))) HU) (eq.mpr (id (eq.rec (eq.refl (id '' U ⊆ U)) (set.image_id U))) (set.subset.refl U)), commutes := λ (U V : set (X R)) (HU : is_open zariski.open U) (HV : is_open zariski.open V) (Hsub : V ⊆ U), eq.refl (((presheaf_of_rings_pullback_under_open_immersion (zariski.structure_presheaf_of_rings R) id H).to_presheaf_of_types).res U V HU HV Hsub ∘ (λ (HU : is_open zariski.open U), ((zariski.structure_presheaf_of_rings R).to_presheaf_of_types).res U (id '' U) HU (eq.mpr (id (eq.rec (eq.refl (is_open zariski.open (id '' U))) (set.image_id U))) HU) (eq.mpr (id (eq.rec (eq.refl (id '' U ⊆ U)) (set.image_id U))) (set.subset.refl U))) HU)}.morphism U HU y

#### Kevin Buzzard (May 22 2018 at 22:28):

proof is refl

#### Andrew Ashworth (May 23 2018 at 01:59):

it seems you discover cool new things daily! perhaps you can include a mathematician's tips and tricks section in the textbook you want to write this summer

Last updated: May 13 2021 at 19:20 UTC