# Zulip Chat Archive

## Stream: maths

### Topic: induced neighborhoods

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

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

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

@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

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

What about the coinduced topology?

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

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

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

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

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

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

What about the coinduced topology?

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.

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

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`

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

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?

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

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, -- bad way 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_space`

s 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