Zulip Chat Archive

Stream: general

Topic: tactic.unfreeze_local_instances


view this post on Zulip Kenny Lau (Oct 28 2018 at 21:43):

import analysis.topology.topological_space
universe u
open set
local attribute [instance] classical.prop_decidable
class t0_space (α : Type u) [topological_space α] : Prop :=
(t0 :  x y, x  y   U:set α, is_open U  (xor (x  U) (y  U)))

theorem exists_open_singleton_of_fintype
  (α : Type u) [topological_space α] [t0_space α]
  [f : fintype α] [decidable_eq α] [ha : nonempty α] :
   x:α, is_open ({x}:set α) :=
have H :  (T : finset α), T     x  T,  u, is_open u  {x} = {y | y  T}  u :=
begin
  intro T,
  apply finset.case_strong_induction_on T,
  { intro h, exact (h rfl).elim },
  { intros x S hxS ih h,
    by_cases hs : S = ,
    { existsi [x, finset.mem_insert_self x S, univ, is_open_univ],
      rw [hs, inter_univ], refl },
    { rcases ih S (finset.subset.refl S) hs with y, hy, V, hv1, hv2,
      by_cases hxV : x  V,
      { cases t0_space.t0 x y (λ hxy, hxS $ by rwa hxy) with U hu,
        rcases hu with hu1, hu2, hu3 | hu2, hu3⟩⟩,
        { existsi [x, finset.mem_insert_self x S, U  V, is_open_inter hu1 hv1],
          apply set.ext,
          intro z,
          split,
          { intro hzx,
            rw set.mem_singleton_iff at hzx,
            rw hzx,
            exact finset.mem_insert_self x S, hu2, hxV⟩⟩ },
          { intro hz,
            rw set.mem_singleton_iff,
            rcases hz with hz1, hz2, hz3,
            cases finset.mem_insert.1 hz1 with hz4 hz4,
            { exact hz4 },
            { have h1 : z  {y : α | y  S}  V,
              { exact hz4, hz3 },
              rw  hv2 at h1,
              rw set.mem_singleton_iff at h1,
              rw h1 at hz2,
              exact (hu3 hz2).elim } } },
        { existsi [y, finset.mem_insert_of_mem hy, U  V, is_open_inter hu1 hv1],
          apply set.ext,
          intro z,
          split,
          { intro hz,
            rw set.mem_singleton_iff at hz,
            rw hz,
            refine finset.mem_insert_of_mem hy, hu2, _⟩,
            have h1 : y  {y} := set.mem_singleton y,
            rw hv2 at h1,
            exact h1.2 },
          { intro hz,
            rw set.mem_singleton_iff,
            cases hz with hz1 hz2,
            cases finset.mem_insert.1 hz1 with hz3 hz3,
            { rw hz3 at hz2,
              exact (hu3 hz2.1).elim },
            { have h1 : z  {y : α | y  S}  V := hz3, hz2.2,
              rw  hv2 at h1,
              rw set.mem_singleton_iff at h1,
              exact h1 } } } },
      { existsi [y, finset.mem_insert_of_mem hy, V, hv1],
        apply set.ext,
        intro z,
        split,
        { intro hz,
          rw set.mem_singleton_iff at hz,
          rw hz,
          split,
          { exact finset.mem_insert_of_mem hy },
          { have h1 : y  {y} := set.mem_singleton y,
            rw hv2 at h1,
            exact h1.2 } },
        { intro hz,
          rw hv2,
          cases hz with hz1 hz2,
          cases finset.mem_insert.1 hz1 with hz3 hz3,
          { rw hz3 at hz2,
            exact (hxV hz2).elim },
          { exact hz3, hz2 } } } } }
end,
begin
  tactic.unfreeze_local_instances,
  cases ha with x,
  specialize H finset.univ (finset.ne_empty_of_mem $ finset.mem_univ x),
  rcases H with y, hyf, U, hu1, hu2,
  existsi y,
  have h1 : {y : α | y  finset.univ} = (univ : set α),
  { exact set.eq_univ_of_forall (λ x : α,
      by rw mem_set_of_eq; exact finset.mem_univ x) },
  rw h1 at hu2,
  rw set.univ_inter at hu2,
  rw hu2,
  exact hu1
end

view this post on Zulip Kenny Lau (Oct 28 2018 at 21:43):

Why do I need tactic.unfreeze_local_instances there?

view this post on Zulip Kenny Lau (Oct 28 2018 at 21:44):

(working example, but clearly not minimal)

view this post on Zulip Mario Carneiro (Oct 28 2018 at 21:50):

because it's a typeclas arg left of the colon

view this post on Zulip Mario Carneiro (Oct 28 2018 at 21:51):

you can use unfreezeI for short

view this post on Zulip Kenny Lau (Oct 28 2018 at 21:57):

I don't understand

view this post on Zulip Kenny Lau (Oct 28 2018 at 21:57):

isn't every typeclass argument left of colon?

view this post on Zulip Chris Hughes (Oct 28 2018 at 22:26):

You don't usually do cases on type class args

view this post on Zulip Kenny Lau (Oct 28 2018 at 22:26):

yeah even if I don't do cases it still messes up

view this post on Zulip Mario Carneiro (Oct 28 2018 at 22:42):

anything that disrupts the context past the position of the colon will require unfreezeI

view this post on Zulip Mario Carneiro (Oct 28 2018 at 22:43):

in this case you can do cases id ha with a if you don't want to clear the hypothesis in the context

view this post on Zulip Kenny Lau (Oct 28 2018 at 22:44):

oh, I get it now

view this post on Zulip Kenny Lau (Oct 28 2018 at 22:45):

oh and how would you golf the proof?

view this post on Zulip Mario Carneiro (Oct 28 2018 at 22:45):

I've been thinking about that... that proof is a little scary long

view this post on Zulip Mario Carneiro (Oct 28 2018 at 22:45):

Maybe you can find a maximal element in the specialization preorder?

view this post on Zulip Kenny Lau (Oct 28 2018 at 22:53):

I don't understand what you mean by the specialization preorder

view this post on Zulip Mario Carneiro (Oct 28 2018 at 22:54):

okay, I refreshed my memory on the specialization preorder and indeed this proof should work (although it is a minimal element by wiki's definition)

view this post on Zulip Mario Carneiro (Oct 28 2018 at 22:54):

it's basically finite zorn's lemma

view this post on Zulip Kevin Buzzard (Oct 28 2018 at 22:55):

A point x specialises to a point y if y is in the closure of x

view this post on Zulip Mario Carneiro (Oct 28 2018 at 22:56):

I think that's the reverse of wiki's terminology?

view this post on Zulip Mario Carneiro (Oct 28 2018 at 22:56):

they say y is a specialization of x in that case

view this post on Zulip Mario Carneiro (Oct 28 2018 at 22:57):

they also say that the orientation is contentious

view this post on Zulip Kevin Buzzard (Oct 28 2018 at 22:57):

Darn Zulip app doesn't show me new posts when they arrive

view this post on Zulip Kevin Buzzard (Oct 28 2018 at 22:58):

Including my own

view this post on Zulip Kevin Buzzard (Oct 28 2018 at 22:59):

Right -- x specialises to y, so y is a specialisation of x.

view this post on Zulip Mario Carneiro (Oct 28 2018 at 22:59):

okay, I wasn't sure about the active verb there

view this post on Zulip Kevin Buzzard (Oct 28 2018 at 23:00):

This is how the words are used in algebraic geometry at least

view this post on Zulip Mario Carneiro (Oct 28 2018 at 23:02):

You should look at the wiki page and decide which order of le makes sense

view this post on Zulip Mario Carneiro (Oct 28 2018 at 23:03):

I'm leaning to the first definition, x <= y means x is a specialization of y, because the evidence from algebraic geometry using Spec R smacks of that order-reversing filter thing

view this post on Zulip Reid Barton (Oct 28 2018 at 23:19):

The ordering I have seen is the one which is equivalent to x \le y if closure({x}) is a subset of closure({y})

view this post on Zulip Reid Barton (Oct 28 2018 at 23:23):

Actually, I'm not sure which way it goes now and my source is at home

view this post on Zulip Mario Carneiro (Oct 28 2018 at 23:36):

I'm not sure why this argument doesn't extend to the infinite case by zorn's lemma though

view this post on Zulip Mario Carneiro (Oct 28 2018 at 23:36):

Obviously it's not true for R so I'm missing a part of the argument

view this post on Zulip Kenny Lau (Oct 29 2018 at 02:46):

https://github.com/leanprover/mathlib/pull/448

view this post on Zulip Kevin Buzzard (Oct 29 2018 at 07:56):

Obviously it's not true for R so I'm missing a part of the argument

For sensible spaces like R the preorder is just "x<=y iff x=y". So there are maximal and minimal elements, but these do not correspond to open singletons.

view this post on Zulip Reid Barton (Oct 29 2018 at 12:38):

Okay, the paper where I've encountered this actually says "... so that X\le_X is the well-known [4] reflexive and transitive relation y{x}y \in \{x\}^-", so I did have this backwards.

view this post on Zulip Reid Barton (Oct 29 2018 at 14:10):

After being confused by this for a while, my conclusion is that the "xx specializes to yy" relation is actually different in algebraic geometry and in domain theory

view this post on Zulip Reid Barton (Oct 29 2018 at 14:11):

one of them has to do with closed sets, the other with open sets

view this post on Zulip Reid Barton (Oct 29 2018 at 14:12):

Because of the duality between open and closed sets, this appears as a reversal of the order

view this post on Zulip Kevin Buzzard (Oct 29 2018 at 15:52):

In algebraic geometry, a "generic point" of an irreducible algebraic variety is a rigorous notion of the intuitive idea of how a general point on the variety behaves. Historically this was done in a vague way -- we had the "actual points" and then "it's true for a generic point" just meant "most points satisfy this" with several, sometimes competing definitions of "most", but with Grothendieck's approach we have the luxury of the generic point actually being a point in the top space, whose topological closure is the entire variety. The idea is that a generic point can specialise to a random "actual point", which is then a specialisation of the generic point. Perhaps the simplest example of this is the two-point topological space with one closed and one open point. A fruitful mental model of this space in geometry is that the whole space is the open unit disc, the closed point is the origin, and the open point is all the other points -- a "general" point in the open disc. If η\eta is the generic point and ss the closed point then the sequence η,η,η,\eta,\eta,\eta,\ldots converges to ss (as well as to η\eta), which is the specialisation in action. One cna think of it as a bunch of points in the punctured disc tending to the origin.


Last updated: May 12 2021 at 04:19 UTC