## Stream: maths

### Topic: induced neighborhoods

#### Patrick Massot (Jun 26 2019 at 15:45):

And where is the corresponding lemma for the coinduced topology?

#### Patrick Massot (Jun 26 2019 at 15:49):

maybe it's wrong actually

@Reid Barton?

#### Reid Barton (Jun 26 2019 at 15:53):

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

#### Reid Barton (Jun 26 2019 at 15:53):

I don't think we need to preserve the name

#### Kevin Buzzard (Jun 26 2019 at 16:21):

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

explicit

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

#### Mario Carneiro (Jun 26 2019 at 16:22):

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

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

Thanks.

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

#### Kevin Buzzard (Jun 26 2019 at 16:28):

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

#### Patrick Massot (Jun 26 2019 at 16:28):

The tempting statement uses map, but it looks wrong

#### Mario Carneiro (Jun 26 2019 at 16:29):

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

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

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

#### Patrick Massot (Jun 26 2019 at 16:30):

Where is this nuchaku thing again?

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

#### Patrick Massot (Jun 26 2019 at 16:33):

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

#### Patrick Massot (Jun 26 2019 at 16:33):

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

#### Mario Carneiro (Jun 26 2019 at 16:34):

or how far it is from lean

#### Mario Carneiro (Jun 26 2019 at 16:35):

@Jasmin Blanchette Help us! Where is leanchaku?

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

#### Mario Carneiro (Jun 26 2019 at 16:37):

That requires your goal be computable though

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

#### Mario Carneiro (Jun 26 2019 at 16:37):

most top space stuff isn't computable

#### Kevin Buzzard (Jun 26 2019 at 16:37):

Even if they only have 3 elements?

#### Mario Carneiro (Jun 26 2019 at 16:38):

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

#### Mario Carneiro (Jun 26 2019 at 16:38):

it's just some thing about sets

#### Kevin Buzzard (Jun 26 2019 at 16:38):

can we enumerate all subsets of a decidable finset?

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

#### Kevin Buzzard (Jun 26 2019 at 16:39):

"just check everything"?

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

#### Kevin Buzzard (Jun 26 2019 at 16:40):

I want to stick to finite decidable types.

even then

#### Mario Carneiro (Jun 26 2019 at 16:41):

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

#### Mario Carneiro (Jun 26 2019 at 16:41):

because you can't have a decidable_eq for set

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

#### Kevin Buzzard (Jun 26 2019 at 16:42):

which he found by using a tool which searched for counterexamples

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

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

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

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

#### Kevin Buzzard (Jun 26 2019 at 16:44):

Is there decidable_pred_set A?

#### Mario Carneiro (Jun 26 2019 at 16:44):

that's called A -> bool

Fair comment.

#### Mario Carneiro (Jun 26 2019 at 16:45):

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

#### Kevin Buzzard (Jun 26 2019 at 16:46):

Patrick, do you fancy refactoring topology again?

#### Mario Carneiro (Jun 26 2019 at 16:47):

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

#### Mario Carneiro (Jun 26 2019 at 16:48):

basically a computable top basis

#### Mario Carneiro (Jun 26 2019 at 16:48):

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

#### 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 $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 (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 $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 (Jun 27 2019 at 08:14):

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

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


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

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

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

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

#### Mario Carneiro (Jun 27 2019 at 08:57):

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

#### Mario Carneiro (Jun 27 2019 at 08:57):

Those two theorems are not equivalent

#### Mario Carneiro (Jun 27 2019 at 08:58):

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

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

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

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

#### Kevin Buzzard (Jun 27 2019 at 08:59):

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

aah

#### Mario Carneiro (Jun 27 2019 at 09:00):

not in general, with these sort of galois connections things

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

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

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

#### Kevin Buzzard (Jun 27 2019 at 09:03):

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

#### Mario Carneiro (Jun 27 2019 at 09:04):

Turns out there isn't one yet

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


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


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


#### Mario Carneiro (Jun 27 2019 at 09:16):

reduced in what direction?

#### Mario Carneiro (Jun 27 2019 at 09:17):

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

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

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

#### Kevin Buzzard (Jun 27 2019 at 09:17):

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

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

#### Kevin Buzzard (Jun 27 2019 at 09:20):

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

#### Mario Carneiro (Jun 27 2019 at 09:20):

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

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

#### Kevin Buzzard (Jun 27 2019 at 09:21):

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

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

#### Kevin Buzzard (Jun 27 2019 at 09:21):

Oh yeah, I proved inclusions for both false theorems

#### 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,
intro hX,
rw mem_comap_sets,
sorry --goal is false
end


#### Kevin Buzzard (Jun 27 2019 at 09:22):

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

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

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

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


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


#### Kevin Buzzard (Jun 27 2019 at 09:32):

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

#### Kevin Buzzard (Jun 27 2019 at 09:32):

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

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


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

#### Mario Carneiro (Jun 27 2019 at 09:35):

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

#### Mario Carneiro (Jun 27 2019 at 09:35):

because topological_space.coinduced is basically the quotient topology

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

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

#### Chris Hughes (Jun 27 2019 at 16:24):

It's enough to make it more difficult.

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

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

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

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

#### Kevin Buzzard (Jun 27 2019 at 16:42):

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

#### Kevin Buzzard (Jun 27 2019 at 16:43):

That's the definition of filter.map

#### Reid Barton (Jun 27 2019 at 16:54):

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

#### Kevin Buzzard (Jun 27 2019 at 20:47):

I couldn't get that to work

Last updated: May 14 2021 at 20:13 UTC