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: Dec 20 2023 at 11:08 UTC