## Stream: general

### Topic: tactic.unfreeze_local_instances

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


#### Kenny Lau (Oct 28 2018 at 21:43):

Why do I need tactic.unfreeze_local_instances there?

#### Kenny Lau (Oct 28 2018 at 21:44):

(working example, but clearly not minimal)

#### Mario Carneiro (Oct 28 2018 at 21:50):

because it's a typeclas arg left of the colon

#### Mario Carneiro (Oct 28 2018 at 21:51):

you can use unfreezeI for short

#### Kenny Lau (Oct 28 2018 at 21:57):

I don't understand

#### Kenny Lau (Oct 28 2018 at 21:57):

isn't every typeclass argument left of colon?

#### Chris Hughes (Oct 28 2018 at 22:26):

You don't usually do cases  on type class args

#### Kenny Lau (Oct 28 2018 at 22:26):

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

#### Mario Carneiro (Oct 28 2018 at 22:42):

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

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

oh, I get it now

#### Kenny Lau (Oct 28 2018 at 22:45):

oh and how would you golf the proof?

#### Mario Carneiro (Oct 28 2018 at 22:45):

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

#### Mario Carneiro (Oct 28 2018 at 22:45):

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

#### Kenny Lau (Oct 28 2018 at 22:53):

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

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

#### Mario Carneiro (Oct 28 2018 at 22:54):

it's basically finite zorn's lemma

#### Kevin Buzzard (Oct 28 2018 at 22:55):

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

#### Mario Carneiro (Oct 28 2018 at 22:56):

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

#### Mario Carneiro (Oct 28 2018 at 22:56):

they say y is a specialization of x in that case

#### Mario Carneiro (Oct 28 2018 at 22:57):

they also say that the orientation is contentious

#### Kevin Buzzard (Oct 28 2018 at 22:57):

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

Including my own

#### Kevin Buzzard (Oct 28 2018 at 22:59):

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

#### Mario Carneiro (Oct 28 2018 at 22:59):

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

#### Kevin Buzzard (Oct 28 2018 at 23:00):

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

#### Mario Carneiro (Oct 28 2018 at 23:02):

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

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

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

#### Reid Barton (Oct 28 2018 at 23:23):

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

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

#### Mario Carneiro (Oct 28 2018 at 23:36):

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

#### Kenny Lau (Oct 29 2018 at 02:46):

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

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

#### Reid Barton (Oct 29 2018 at 12:38):

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

#### Reid Barton (Oct 29 2018 at 14:10):

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

#### Reid Barton (Oct 29 2018 at 14:11):

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

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

#### 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 $s$ the closed point then the sequence $\eta,\eta,\eta,\ldots$ converges to $s$ (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