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


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