induced neighborhoods

Stream: maths

[Patrick Massot]

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?

[Patrick Massot]

And where is the corresponding lemma for the coinduced topology?

[Patrick Massot]

maybe it's wrong actually

[Patrick Massot]

@Reid Barton?

[Reid Barton]

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

[Reid Barton]

I don't think we need to preserve the name

[Patrick Massot]

What about the coinduced topology?

[Kevin Buzzard]

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

[Mario Carneiro]

explicit

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Thanks.

[Mario Carneiro]

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

[Kevin Buzzard]

What about the coinduced topology?

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

[Patrick Massot]

The tempting statement uses map, but it looks wrong

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Patrick Massot]

Where is this nuchaku thing again?

[Kevin Buzzard]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

or how far it is from lean

[Mario Carneiro]

@Jasmin Blanchette Help us! Where is leanchaku?

[Kevin Buzzard]

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

[Mario Carneiro]

That requires your goal be computable though

[Kevin Buzzard]

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.

[Mario Carneiro]

most top space stuff isn't computable

[Kevin Buzzard]

Even if they only have 3 elements?

[Mario Carneiro]

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

[Mario Carneiro]

it's just some thing about sets

[Kevin Buzzard]

can we enumerate all subsets of a decidable finset?

[Mario Carneiro]

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

[Kevin Buzzard]

"just check everything"?

[Mario Carneiro]

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

[Kevin Buzzard]

I want to stick to finite decidable types.

[Mario Carneiro]

even then

[Mario Carneiro]

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

[Mario Carneiro]

because you can't have a decidable_eq for set

[Kevin Buzzard]

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"

[Kevin Buzzard]

which he found by using a tool which searched for counterexamples

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Kevin Buzzard]

Is there decidable_pred_set A?

[Mario Carneiro]

that's called A -> bool

[Kevin Buzzard]

Fair comment.

[Mario Carneiro]

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

[Kevin Buzzard]

Patrick, do you fancy refactoring topology again?

[Mario Carneiro]

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

[Mario Carneiro]

basically a computable top basis

[Mario Carneiro]

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

[Kevin Buzzard]

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 $Y$ of beta is in the LHS iff $f(a)$ is in the interior of $Y$, and is in the RHS iff $a$ is in the interior of $f^{-1}(Y)$. The first of these implies the second, but if I only know that $a$ is in the interior of $f^{-1}(Y)$ I can't deduce that $f(a)$ is in the interior of $Y$ (consider a closed embedding with $Y$ equal to the image and $a$ not in the interior of $Y$ computed in beta).

[Kevin Buzzard]

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 $B$, and similarly $A$ for \alpha.

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

So $Y$ is in the LHS iff there exists some $U\subseteq A$ open and a pre-image under $f$, such that $a\in U\subseteq f^{-1}(Y)$. And $Y$ is in the RHS iff there exists some $U\subseteq A$ open (but not necessarily a preimage under $f$) such that $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 $f$ and $B$ and just put an equivalence relation on $A$ (and let $B$ be the quotient and f=mk). And now the question is: come up with an example of a topological space $A$ and a random equivalence relation on it which has nothing to do with the topology, with the property that there's a union $X$ of equivalence classes $(f^{-1}(Y))$ and an element $a\in A$ and an open subset $U$ of $A$ with $a\in U\subseteq X$, but where there is no $U'$ 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,\eta\}$ be the top space with two elements, a closed (non-open) point $s$ and an open point $\eta$ (is this called Sierpinski space or something?). Let alpha be the disjoint union of $S$ and a discrete one point space $\{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\}$ being in the right hand side but not the left hand side.

How best to get Lean to check my working?

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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?

[Kevin Buzzard]

@[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?

[Mario Carneiro]

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

[Mario Carneiro]

Those two theorems are not equivalent

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

aah

[Mario Carneiro]

not in general, with these sort of galois connections things

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Mario Carneiro]

Turns out there isn't one yet

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

reduced in what direction?

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Oh yeah, I proved inclusions for both false theorems

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Mario Carneiro]

because topological_space.coinduced is basically the quotient topology

[Patrick Massot]

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

[Kevin Buzzard]

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?

[Chris Hughes]

It's enough to make it more difficult.

[Johan Commelin]

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

[Johan Commelin]

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?

[Kevin Buzzard]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

That's the definition of filter.map

[Reid Barton]

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

[Kevin Buzzard]

I couldn't get that to work