Zulip Chat Archive

Stream: maths

Topic: induced neighborhoods


view this post on Zulip Patrick Massot (Jun 26 2019 at 15:29):

What should we do with the duplication https://github.com/leanprover-community/mathlib/blob/master/src/topology/order.lean#L557-L558 vs https://github.com/leanprover-community/mathlib/blob/master/src/topology/order.lean#L862?

view this post on Zulip Patrick Massot (Jun 26 2019 at 15:45):

And where is the corresponding lemma for the coinduced topology?

view this post on Zulip Patrick Massot (Jun 26 2019 at 15:49):

maybe it's wrong actually

view this post on Zulip Patrick Massot (Jun 26 2019 at 15:49):

@Reid Barton?

view this post on Zulip Reid Barton (Jun 26 2019 at 15:53):

I guess just delete the second one and update its uses to use the first one

view this post on Zulip Reid Barton (Jun 26 2019 at 15:53):

I don't think we need to preserve the name

view this post on Zulip Patrick Massot (Jun 26 2019 at 15:55):

What about the coinduced topology?

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:21):

The function and the element are explicit in one, implicit in the other. Which is "right"?

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:21):

explicit

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:22):

And what's the algorithm for working this out? Both f and a are determined by the type of the conclusion.

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:22):

you don't use the type of the conclusion in the accounting, just other hypotheses

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:23):

One way to put it: if you write have := my_thm a b c h1 h2 with all explicit variables filled in, then there should be no metavariables remaining

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:24):

Thanks.

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:24):

The rule for iff's is a bit different though; it is sufficient that (my_iff a).1 h and (my_iff a).2 h' have no metavariables

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:28):

What about the coinduced topology?

Is the corresponding lemma still about comaps, or about maps? Or are they the same?

view this post on Zulip Patrick Massot (Jun 26 2019 at 16:28):

The tempting statement uses map, but it looks wrong

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:29):

It may be missing because there isn't a nice statement

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:29):

Can we guess statements and then somehow try them out on all topological spaces with at most three elements?

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:30):

I ran into that issue yesterday. It would be really cool to be able to formalise a guess and then just try it

view this post on Zulip Patrick Massot (Jun 26 2019 at 16:30):

Where is this nuchaku thing again?

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:30):

In fact Lean should have an option where it occasionally tests your goal with random values for the variables and then prints a little message saying "by the way your goal is false right now" if it finds a counterexample

view this post on Zulip Patrick Massot (Jun 26 2019 at 16:33):

https://github.com/nunchaku-inria/nunchaku

view this post on Zulip Patrick Massot (Jun 26 2019 at 16:33):

I don't know how far it is from being usable

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:34):

or how far it is from lean

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:35):

@Jasmin Blanchette Help us! Where is leanchaku?

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:36):

Even something like this https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/noob.20question%28s%29/near/168891798 would be cool.

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:37):

That requires your goal be computable though

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:37):

You just guess

theorem nhds_coinduced {α β : Type} [T : topological_space α] (f : α  β) (a : α) :
  @nhds β (topological_space.coinduced f T) (f a) = map f (nhds a) :=

randomly and fire a bunch of topological spaces at it and see.

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:37):

most top space stuff isn't computable

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:37):

Even if they only have 3 elements?

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:38):

it's not a computable statement - it's not written in terms of computable functions

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:38):

it's just some thing about sets

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:38):

can we enumerate all subsets of a decidable finset?

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:39):

Sure it's possible to algorithmically determine the answer on small finite sets but we would need a decision procedure

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:39):

"just check everything"?

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:40):

And many of the facts aren't even over computable types, e.g. you might have to check whether {1} = {2, 3} as elements of set nat

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:40):

I want to stick to finite decidable types.

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:41):

even then

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:41):

even if it said set (fin 4) there it wouldn't work

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:41):

because you can't have a decidable_eq for set

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:41):

I saw Kenny do this once. Someone said "is it true that every commutative binary relation is associative" and a couple of minutes later Kenny said "no, here is a random two element set and a random commutative binary relation which is not associative"

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:42):

which he found by using a tool which searched for counterexamples

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:42):

It's possible to make computable versions of all the functions in the statement, but I don't think you can get that to happen automatically by inferring a decidable instance

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:43):

because you can't have a decidable_eq for set

What if they're decidable sets or something? There must be a way around this.

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:43):

I just want to let A and B be sets of size 3 and put a random topology on A and choose a random element and test the proposition.

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:44):

I think you can prove decidable (s = t) if decidable_pred s and decidable_pred t and s t : set A where fintype A

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:44):

Is there decidable_pred_set A?

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:44):

that's called A -> bool

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:45):

Fair comment.

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:45):

If you encoded topologies as (A -> bool) -> bool you could get most things to compute

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 16:46):

Patrick, do you fancy refactoring topology again?

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:47):

There is also data.analysis.topology which has "computational realizers" for topologies and filters

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:48):

basically a computable top basis

view this post on Zulip Mario Carneiro (Jun 26 2019 at 16:48):

which works even on "real world" topologies like the reals

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 20:56):

I've just come back to this. So I think

theorem nhds_coinduced {α β : Type} [T : topological_space α] (f : α  β) (a : α) :
  @nhds β (topological_space.coinduced f T) (f a) = map f (nhds a)

is false, because a subset YY of beta is in the LHS iff f(a)f(a) is in the interior of YY, and is in the RHS iff aa is in the interior of f1(Y)f^{-1}(Y). The first of these implies the second, but if I only know that aa is in the interior of f1(Y)f^{-1}(Y) I can't deduce that f(a)f(a) is in the interior of YY (consider a closed embedding with YY equal to the image and aa not in the interior of YY computed in beta).

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 08:06):

Oh darn it I can't just consider a closed embedding because f is not just continuous, I need to find an example where beta has the coinduced topology. So I still think it's false. Here are my thoughts. It's really annoying not being able to write beta in Zulip without copy-paste so I'm going to call it BB, and similarly AA for \alpha.

So an arbitrary subset YBY\subseteq B is in the LHS if there's some VBV\subseteq B open such that f(a)Vf(a)\in V and VYV\subseteq Y. The definition of VV being open in BB is simply that U:=f1(V)U := f^{-1}(V) is open in AA.

So YY is in the LHS iff there exists some UAU\subseteq A open and a pre-image under ff, such that aUf1(Y)a\in U\subseteq f^{-1}(Y). And YY is in the RHS iff there exists some UAU\subseteq A open (but not necessarily a preimage under ff) such that aUf1(Y)a\in U\subseteq f^{-1}(Y).

So now this is all about whether subsets are pre-images or not, so we can throw away ff and BB and just put an equivalence relation on AA (and let BB be the quotient and f=mk). And now the question is: come up with an example of a topological space AA and a random equivalence relation on it which has nothing to do with the topology, with the property that there's a union XX of equivalence classes (f1(Y))(f^{-1}(Y)) and an element aAa\in A and an open subset UU of AA with aUXa\in U\subseteq X, but where there is no UU' satisfying the same properties and also being a union of equivalence classes.

The simplest way to do this would be to just have two equivalence classes, one of them being not open, and set-theoretically the disjoint union of an open set and a point, and the other one being the rest.

So it seems to me that the simplest counterexample is this. Let S:={s,η}S:=\{s,\eta\} be the top space with two elements, a closed (non-open) point ss and an open point η\eta (is this called Sierpinski space or something?). Let alpha be the disjoint union of SS and a discrete one point space {a}\{a\}, as a topological space. Let beta be bool and define a map alpha -> beta by sending s and a to tt and eta to ff.

If I've got this calculation right, and I may not have, then this should be a counterexample, with the subset {s,a}\{s,a\} being in the right hand side but not the left hand side.

How best to get Lean to check my working?

view this post on Zulip Mario Carneiro (Jun 27 2019 at 08:14):

I think that alpha := option Prop and f := is_some will work to get that

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 08:28):

In writing down a proof I just had to write existsi subset.trans _ hY because use (subset.trans _ hY) gave me the cool error

failed to instantiate goal with subset.trans 6._.104 hY

view this post on Zulip Mario Carneiro (Jun 27 2019 at 08:29):

I have had issues with use in the past as well... it's not a total replacement of existsi

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 08:50):

theorem nhds_coinduced {α β : Type} [T : topological_space α] (f : α  β) (a : α) :
  comap f (@nhds β (topological_space.coinduced f T) (f a)) = (nhds a) :=

I think this theorem is also false, for exactly the same reasons. Are the theorems equivalent? Just shows how little I know about filters. I'm working through examples like this because I've realised that actually I have had very little experience working with filters and lattices in Lean; my abysmal efforts at 3am last Sat trying to make instances of lattice classes where I found that I didn't even know how to create the structures let alone use them, has somehow woken me up a bit.

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 08:51):

I think that alpha := option Prop and f := is_some will work to get that

I wanted option Sierpinski_space. This feels different. Is it? If Prop = bool then...I'm assuming the top on bool is the discrete top. Am I wrong?

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 08:54):

@[instance]
protected def bool.topological_space : topological_space bool :=
⊤

You don't want "truth to be an open condition, falsehood to be a closed one" or something? Oh, is the point that the map Prop -> bool is noncomputable and hence not continuous?

view this post on Zulip Mario Carneiro (Jun 27 2019 at 08:57):

The topology on Prop is sierpinski, the topology on bool is discrete

view this post on Zulip Mario Carneiro (Jun 27 2019 at 08:57):

Those two theorems are not equivalent

view this post on Zulip Mario Carneiro (Jun 27 2019 at 08:58):

(well I guess they are equivalent if they are both false)

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 08:58):

And the map from bool to Prop is continuous, and the noncomputable map from Prop to bool is not.

view this post on Zulip Mario Carneiro (Jun 27 2019 at 08:58):

I'm not totally convinced that the sierpinski topology on Prop is the "right" one, but it is convenient in this case

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 08:59):

Those two theorems are not equivalent

Right. I asked because it seemed to me that at the end of the day they were both asking the same question, which surprised me a little.

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 08:59):

Are either of map o comap or comap o map the identity?

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:00):

aah

view this post on Zulip Mario Carneiro (Jun 27 2019 at 09:00):

not in general, with these sort of galois connections things

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:00):

I can just look in the library for theorems whose names contain map_comap etc, and see examples of conditions which force it. So I can see that neither is true in general (as I suspected).

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:01):

I think that for at least one of those theorems, it's true in general iff it's true for surjections, and perhaps for surjections you can do something.

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:02):

But this isn't my point. I just want to say to Lean "hey Lean, just go through your database of small topological spaces and find counterexamples for me please". The fact that there is a counterexample with alpha having three elements makes me think that this is possible. Your suggestion with option Prop is somehow not going in the way I want this to go.

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:03):

It also makes me have to learn what the topology on option X is

view this post on Zulip Mario Carneiro (Jun 27 2019 at 09:04):

Turns out there isn't one yet

view this post on Zulip Mario Carneiro (Jun 27 2019 at 09:05):

I'm trying to prove this too; here's my prelude so far

import topology.order

open filter

namespace topological_space

instance {α} [t : topological_space α] : topological_space (option α) :=
coinduced option.some t

theorem nhds_coinduced {α β : Type} [T : topological_space α] (f : α  β) (a : α) :
  @nhds β (topological_space.coinduced f T) (f a) = map f (nhds a) := sorry

end topological_space

def sierp := bool
instance : topological_space sierp := topological_space.generate_from {{tt}}

theorem is_open_sierp {s : set sierp} (h : is_open s) {a} (ha : a  s) : tt  s :=
begin
  induction h,
  { rcases h_H with rfl|⟨⟨⟩⟩, exact or.inl rfl },
  { trivial },
  { exact h_ih_a ha.1, h_ih_a_1 ha.2 },
  { rcases ha with s, h₁, h₂,
    exact s, h₁, h_ih _ h₁ h₂ }
end

view this post on Zulip Mario Carneiro (Jun 27 2019 at 09:10):

def f : option sierp  bool
| (some tt) := tt
| _ := ff

example : false :=
begin
  have := le_of_eq (topological_space.nhds_coinduced f none),
  replace := @this {x | x = ff} (mem_map.2 _),
  { rw mem_nhds_sets_iff at this,
    rcases this with s, h₁, h₂, h₃,
    rw [is_open_coinduced, is_open_coinduced] at h₂,
    cases h₁ (@is_open_sierp _ h₂ ff h₃) },
  refine mem_nhds_sets_iff.2 {none}, _, _, or.inl rfl,
  { rintro _ (rfl|⟨⟨⟩⟩), exact rfl },
  rw [is_open_coinduced,
    (@set.eq_empty_iff_forall_not_mem _ (some ⁻¹' {none})).2], simp,
  rintro _ (⟨⟨⟩⟩|⟨⟨⟩⟩)
end

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:14):

I reduced the (false) theorem

theorem nhds_coinduced {α β : Type} [T : topological_space α] (f : α  β) (a : α) :
  comap f (@nhds β (topological_space.coinduced f T) (f a)) = (nhds a) :=

to

1 goal
α β : Type,
T : topological_space α,
f : α → β,
a : α,
X : set α,
hX : X ∈ (nhds a).sets
⊢ ∃ (t : set β) (H : t ∈ nhds (f a)), f ⁻¹' t ⊆ X

view this post on Zulip Mario Carneiro (Jun 27 2019 at 09:16):

reduced in what direction?

view this post on Zulip Mario Carneiro (Jun 27 2019 at 09:17):

Are you saying that goal implies the theorem or vice versa?

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:17):

This seems to say that an arbitrary neighbourhood of a should be contained within a neighbourhood which is a preimage. Exactly the same false statement. In fact this should be perhaps thought of as the criterion under which one can deduce both of these theorems @Patrick Massot ; it looks to me like it's equivalent. Does it have some more natural interpretation? I think the goal I just posted above, when considered as a hypothesis, is basically equivalent to both the theorems.

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:17):

I am saying that I started with the false theorem, tried to prove it, and that's where I'm stuck.

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:17):

However I am not sure I actually did anything non-reversible.

view this post on Zulip Mario Carneiro (Jun 27 2019 at 09:19):

Here's a different question. What is an expression for @nhds β (topological_space.coinduced f T) (f a)?

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:20):

I've been thinking about it as some sort of sub-filter of nhds a

view this post on Zulip Mario Carneiro (Jun 27 2019 at 09:20):

So there is at least one inequality that can be proved then

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:20):

It's not really a sub-filter, because it also contains a bunch of junk coming from points in beta which aren't in the image of f

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:21):

I don't really know how to think about filters.

view this post on Zulip Mario Carneiro (Jun 27 2019 at 09:21):

You will notice that in the proof of false above the first thing I do is use le_of_eq on the false theorem, so maybe the other inequality holds

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:21):

Oh yeah, I proved inclusions for both false theorems

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:21):

theorem nhds_coinduced {α β : Type} [T : topological_space α] (f : α  β) (a : α) :
  comap f (@nhds β (topological_space.coinduced f T) (f a)) = (nhds a) :=
begin
  apply filter.ext,
  dsimp,
  intro X,
  split,
    rintro Y, H, hY,
    rw mem_nhds_sets_iff at H,
    rcases H with V, HVY, HV, HaV,
    rw mem_nhds_sets_iff,
    use f ⁻¹' V,
    existsi (subset.trans _ hY),
      split,
        exact HV,
      exact HaV,
    intros x hx, exact HVY hx,
  -- bad way
  intro hX,
  rw mem_comap_sets,
  sorry --goal is false
end

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:22):

I didn't formalise the other proof but it's equally easy.

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:23):

I have no feeling for what should go in the library (or whether something is already there).

view this post on Zulip Mario Carneiro (Jun 27 2019 at 09:23):

usually it is comap f L' <= L and L' <= map f L that are the strong/ false properties; the other inequalities L <= comap f L' and map f L <= L' are equivalent to each other (they are the adjunction) and are equivalent to a tendsto

view this post on Zulip Mario Carneiro (Jun 27 2019 at 09:31):

theorem nhds_coinduced_comap {α β : Type} [T : topological_space α] (f : α  β) (a : α) :
  nhds a  comap f (@nhds β (topological_space.coinduced f T) (f a)) :=
tendsto_iff_comap.1 $
by apply continuous.tendsto; exact continuous_coinduced_rng

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:32):

theorem nhds_coinduced {α β : Type} [T : topological_space α] (f : α  β) (a : α) :
  map f (nhds a)  @nhds β (topological_space.coinduced f T) (f a) :=
begin
  intro Y,
  intro HY,
  rw mem_nhds_sets_iff at HY,
  rcases HY with V, HV, HOV, HaV,
  rw mem_map,
  rw mem_nhds_sets_iff,
  use f ⁻¹' V,
  existsi _, swap,
    intros x hx, apply HV, exact hx,
  split, exact HOV,
  exact HaV,
end

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:32):

Aah but you can just do that one with the Galois connection thing I guess.

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:32):

I'm assuming it works that way around :-)

view this post on Zulip Mario Carneiro (Jun 27 2019 at 09:33):

yes, it's even easier because this is the definition of tendsto:

theorem nhds_coinduced_map {α β : Type} [T : topological_space α] (f : α  β) (a : α) :
  map f (nhds a)  @nhds β (topological_space.coinduced f T) (f a) :=
by apply continuous.tendsto; exact continuous_coinduced_rng

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:35):

So now the only question left is whether that goal I posted above is a sufficiently interesting precondition to get the other inequalities. I'm having trouble visualising it in some conceptual way. Once one has visualised it in a conceptual way, it might simply turn into literally the statement of the inequality in the other direction.

view this post on Zulip Mario Carneiro (Jun 27 2019 at 09:35):

I suspect this has something to do with being a quotient map

view this post on Zulip Mario Carneiro (Jun 27 2019 at 09:35):

because topological_space.coinduced is basically the quotient topology

view this post on Zulip Patrick Massot (Jun 27 2019 at 13:05):

Thank you very much Kevin and Mario. I didn't think that question would trigger so many messages in my absence. I should have written more assertively I thought the obvious nice formula was wrong (even if I don't have a counter-example).

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 16:18):

What I found frustrating is that I still don't really understand why we can't just say "test this on all surjections from topological spaces with at most three elements". Is the fact that an open set is a map to Prop and not bool enough to actually stop this happening?

view this post on Zulip Chris Hughes (Jun 27 2019 at 16:24):

It's enough to make it more difficult.

view this post on Zulip Johan Commelin (Jun 27 2019 at 16:27):

If only we had some tactic that would transform maps to Prop into maps to the equivalent bool...

view this post on Zulip Johan Commelin (Jun 27 2019 at 16:29):

Should we define toboological_space? Define some transfer relations? Would it be easy to test Kevin's question on toboological_spaces with at most 3 elements? Or would this still require a significant amount of work?

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 16:39):

I just like doing little exercises like this, I need to learn more about how to use filters and lattices and the like.

view this post on Zulip Reid Barton (Jun 27 2019 at 16:42):

The fact that we have to deal with set (set X) and not just set X also makes it a bit more difficult

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 16:42):

I couldn't get f ⁻¹' ⁻¹' to work :-)

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 16:43):

That's the definition of filter.map

view this post on Zulip Reid Barton (Jun 27 2019 at 16:54):

maybe ((f ⁻¹') ⁻¹')?

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 20:47):

I couldn't get that to work


Last updated: May 14 2021 at 20:13 UTC