Zulip Chat Archive

Stream: condensed mathematics

Topic: lemma 9.2


view this post on Zulip Johan Commelin (Mar 15 2021 at 15:38):

Lemma 9.2 might look a bit intimidating, but actually you don't need to understand all the details of Mr(S)\overline{\mathcal M}_{r'}(S). You can abstract over it. So this might be a nice target for someone trying to jump into the project.

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:40):

https://leanprover-community.github.io/liquid/index.html#lem:Tinv

view this post on Zulip Peter Scholze (Mar 15 2021 at 15:41):

I think you didn't yet fully go through with the abstraction, did you?

view this post on Zulip Peter Scholze (Mar 15 2021 at 15:41):

I don't think you need to quantify over aa anymore, for example, and there's still lots of SS's in the document

view this post on Zulip Peter Scholze (Mar 15 2021 at 15:42):

Basically all Mr(S)a\overline{\mathcal M}_{r'}(S)^a's should become MM's

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:43):

Hmm, I think we might still want the aa. Because we didn't define sums of profinitely filtered pseudo normed group with Tinv's yet

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:43):

I'm not sure if we want to do that, or just keep the a here

view this post on Zulip Peter Scholze (Mar 15 2021 at 15:44):

Hmm, OK.

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:44):

Peter Scholze said:

I don't think you need to quantify over aa anymore, for example, and there's still lots of SS's in the document

Hmm, my search-replace didn't do what I wanted it to do. It just removed the \overline but nothing else :sad:

view this post on Zulip Peter Scholze (Mar 15 2021 at 15:45):

(In this case, it should be not sums but products, by the way)

view this post on Zulip Peter Scholze (Mar 15 2021 at 15:45):

I'd have guessed those shouldn't be hard to come up with?

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:47):

Yeah, but then we'll need to know that (Ma)c=(Mc)a(M^a)_c = (M_c)^a, and this will not be defeq.

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:47):

So when we apply it in 9.5 we will need to use that iso, which just seems annoying. But maybe we'll need that iso anyway.

view this post on Zulip Peter Scholze (Mar 15 2021 at 15:48):

Hmm, OK, they seem def-eq to me ;-). But yeah, it's fine with the aa there.

view this post on Zulip Peter Scholze (Mar 15 2021 at 15:48):

Slightly more seriously, I think there's however something about the rr' that's relevant here

view this post on Zulip Peter Scholze (Mar 15 2021 at 15:49):

Does a profinitely filtered pseudo-normed group with action of T1T^{-1} have the property that the norm scales by rr'?

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:50):

/-- A *profinitely filtered pseudo normed topological group with action by `T⁻¹`* is
a profinitely filtered pseudo normed topological group `M` together with a
nonnegative real `r'` and homomorphism `Tinv : M → M` such that
`Tinv x ∈ filtration M (r'⁻¹ * c)` for all `x ∈ filtration M c`.

Morphisms are continuous and strict homomorphisms. -/
class profinitely_filtered_pseudo_normed_group_with_Tinv (r' : out_param $ 0) (M : Type*)
  extends profinitely_filtered_pseudo_normed_group M :=
(Tinv : profinitely_filtered_pseudo_normed_group_hom M M)
(Tinv_mem_filtration :  c x, x  filtration c  Tinv x  filtration (r'⁻¹ * c))

view this post on Zulip Peter Scholze (Mar 15 2021 at 15:51):

OK, Great! Then it should work in this generality

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:53):

Maybe we should somehow force lean to accept the notation T⁻¹ without starting to look for a T of which it should take the inverse. That would make things more pleasant to read.

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:10):

@Peter Scholze By the way, there is a way in which we can make these defeq, but it involves making the M_c into separate types. Whereas now they are terms of type set M.

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:11):

So, now we can write xMc1yMc2    (x+y)Mc1+c2x \in M_{c_1} \land y \in M_{c_2} \implies (x+y) \in M_{c_1 + c_2}, which is quite comfortable to work with.

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:12):

But if we make the M_c into separate types, that means that we need to carry around functions add:Mc1×Mc2Mc1+c2\mathrm{add} : M_{c_1} \times M_{c_2} \to M_{c_1+c_2} and lots of compatibility maps.

view this post on Zulip Peter Scholze (Mar 15 2021 at 16:12):

OK, I see. Anyway, the blueprint now looks good!

view this post on Zulip Heather Macbeth (Mar 16 2021 at 23:02):

I looked a little at this lemma, and specifically I tried to formulate the core topological part of the argument, see branch here. Here is what the blueprint says:

... it suffices to see that for any closed immersion ABA\subset B of profinite sets and a map fA:AV^f_A: A\to \widehat{V}, there is an extension fB:BV^f_B: B\to \widehat{V} of fAf_A with fB(1+ϵ)fA||f_B||\leq (1+\epsilon)||f_A||. To see this, write fAf_A as a (fast) convergent sum of maps that factor over a finite quotient of AA; for maps factoring over a finite quotient of AA, the extension is clear (and can be done in a norm-preserving way), as any map from AA to a finite set can be extended to a map from BB to the same finite set.

Before I or anyone else tries to prove this, I wanted to check that I haven't thrown away too much information. For this part of the argument, do we really just need that V^\widehat{V} be a complete normed group (no knowledge about the VV it came from), and that fA:AV^f_A:A\to\widehat{V} be bounded continuous (not locally constant or something fancier)? So this an extension theorem for profinite sets, in the same spirit as the Tietze extension theorem, etc?

view this post on Zulip Johan Commelin (Mar 17 2021 at 06:33):

Ooh, this makes me realise that I don't know whether the equivalence Profinite = Pro(Fintype) is now completely in mathlib.

view this post on Zulip Johan Commelin (Mar 17 2021 at 06:33):

@Calle Sönne @Bhavik Mehta you were working on this, right?

view this post on Zulip Patrick Massot (Mar 17 2021 at 08:20):

Heather, you should have a look at https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/sequences.lean before starting on this.

view this post on Zulip Peter Scholze (Mar 17 2021 at 10:19):

@Heather Macbeth That's right.

view this post on Zulip Bhavik Mehta (Mar 17 2021 at 12:39):

The equivalence of categories isn't in mathlib - we don't have Pro yet. Calle was working on showing that any profinite set is a cofiltered limit of finite sets, which I think is done but not in mathlib yet?

view this post on Zulip Peter Scholze (Mar 17 2021 at 12:45):

@Johan Commelin Will it be necessary to use this here? Maybe the definition of V^(S)\hat{V}(S) in terms of the completion of locally constant maps is good enough?

view this post on Zulip Johan Commelin (Mar 17 2021 at 12:53):

Hmm, but the proof in the PDF talks about factoring via finite quotients.

view this post on Zulip Adam Topaz (Mar 17 2021 at 13:38):

To factor over a finite quotient you need much less -- just a decomposition of the profinite set into a disjoint union of opens.

view this post on Zulip Peter Scholze (Mar 17 2021 at 13:45):

I think 8.17 could be helpful here, applied to MM' the locally constant functions from BB to VV, and MM the locally constant functions from AA to VV (and M=0M''=0)

view this post on Zulip Peter Scholze (Mar 17 2021 at 14:06):

Then one needs to see that any locally constant map from AA to VV extends to a locally constant map from BB to VV with the same norm. So I think the only thing one needs to see about profinite sets is that any locally constant map factors over a finite quotient. But that should be an easy consequence of compactness?

view this post on Zulip Patrick Massot (Apr 26 2021 at 07:24):

I tried to see whether I could help with this Lemma 9.2 and I immediately hit something I don't understand. I have no intuition about profinite sets, neither as topological spaces nor as category theory gadgets. So I don't see why obvious things are obvious. If I'm reading the blueprint and this conversation correctly, the first obvious thing is that if $$i : A \to B$ is a closed embedding of profinite sets then any continuous map from AA to a finite set CC continuously extends to BB. I don't mind spending time thinking about this but, if I understand correctly, this is meant to be fully obvious, even without knowing that profinite sets are pro-(finite sets). What is the trick?

view this post on Zulip Peter Scholze (Apr 26 2021 at 07:40):

You can think of a map to a finite set in terms of the partition (into clopen subsets) it induces. So you have to show that given a partition A=A1AnA=A_1\sqcup\ldots\sqcup A_n, you can find a partition B=B1BnB=B_1\sqcup\ldots\sqcup B_n extending it. For this, you can first spread any AiA_i individually into a clopen subset BiB_i' of BB, and then set B1=B1B_1=B_1', B2=(B1B2)B1B_2=(B_1'\cup B_2')\setminus B_1', ..., Bn1=(B1Bn1)(B1Bn2)B_{n-1}=(B_1'\cup\ldots\cup B_{n-1}')\setminus (B_1'\cup\ldots\cup B_{n-2}') and Bn=B(B1Bn1)B_n=B\setminus (B_1'\cup\ldots\cup B_{n-1}').

Why does any clopen subset of AA extend to BB? I think this should follow from a rather naive argument (making use of the fact that the topology has a basis of clopen subsets).

view this post on Zulip Patrick Massot (Apr 26 2021 at 07:56):

Thanks, I'll think about this. This is the kind of things I would have tried if the statement hadn't been pictured as completely obvious. I guess I over interpreted that obviousness.

view this post on Zulip Patrick Massot (Apr 26 2021 at 07:57):

My wrong guess was that the category theoretic interpretation of profinite sets would make it obvious, but then I was confused because this was part of a discussion claiming this category thing wasn't needed.

view this post on Zulip Patrick Massot (Apr 26 2021 at 08:01):

Actually I don't follow that. What do you mean by "spread any AiA_i into a clopen subset BiB_i' of BB"?

view this post on Zulip Peter Scholze (Apr 26 2021 at 08:04):

Find some clopen subset BiB_i' of BB with Ai=ABiA_i=A\cap B_i'.

view this post on Zulip Peter Scholze (Apr 26 2021 at 08:06):

(Saying it all differently, the claim is that in the Tietze extension lemma for compact Hausdorff spaces, one can replace the interval [0,1][0,1] with a discrete set {0,1/n,,1}\{0,1/n,\ldots,1\} when assuming that the spaces are totally disconnected. I'd assume this follows directly from an inspection of the proof of Tietze's extension lemma.)

view this post on Zulip Peter Scholze (Apr 26 2021 at 08:06):

Is the Tietze extension lemma in Lean?

view this post on Zulip Patrick Massot (Apr 26 2021 at 08:08):

I don't think so, but this shouldn't be a problem. Sorry I'm very slow this morning.

view this post on Zulip Peter Scholze (Apr 26 2021 at 08:12):

Maybe I can also give a different argument, which is the one I'm secretly using. One can write AA as the cofiltered intersection of the clopen subsets A~B\tilde{A}\subset B containing AA, and then thinking in terms of pro-(finite sets), it is clear that any map from AA to a finite set extends to some A~\tilde{A}. Thus, we can assume that AA is clopen in BB, but then it's very easy.

view this post on Zulip Peter Scholze (Apr 26 2021 at 08:13):

By the way, you will probably realize that the lemma fails when AA is empty and the target is empty (but BB is nonempty).

view this post on Zulip Patrick Massot (Apr 26 2021 at 08:14):

I'm now perfectly happy with the hands-on proof, but I'm also glad to see you indeed had a secret proof like I suspected.

view this post on Zulip Patrick Massot (Apr 26 2021 at 09:16):

Peter, since you are is still around, maybe I should ask another question. In this Lemma 9.2, the first thing you do is to extend a continuous function from Mr(S)rca\overline{\mathcal{M}}_{r'}(S)_{\le r'c}^a to Mr(S)a\overline{\mathcal{M}}_{r'}(S)^a. But I thought the later wasn't really meant to have a topology. What do you mean exactly there?

view this post on Zulip Peter Scholze (Apr 26 2021 at 09:19):

I mean a compatible family of maps defined on all its profinite subsets

view this post on Zulip Peter Scholze (Apr 26 2021 at 09:20):

That, I guess, is the same thing as a map on the union, equipped with its colimit topology

view this post on Zulip Peter Scholze (Apr 26 2021 at 09:20):

But that's just one way to think about it

view this post on Zulip Patrick Massot (Apr 26 2021 at 09:21):

Ok, thanks.

view this post on Zulip Adam Topaz (Apr 26 2021 at 12:35):

@Patrick Massot before you spend too much time on this, perhaps I should merge the Profinite stuff I did in the cech_stuff branch. It has some code about decomposition of Profinite sets into disjoint unions of clopen sets, and a description of morphisms in terms of limits of morphisms of finite sets.

view this post on Zulip Adam Topaz (Apr 26 2021 at 12:59):

@Patrick Massot I isolated these files related to profinite sets in the profinite_clopen branch, in case you find them useful!
https://github.com/leanprover-community/lean-liquid/compare/profinite_clopen

view this post on Zulip Patrick Massot (Apr 26 2021 at 15:46):

I'm seeing this a bit late. Does your abstract work include:

lemma nhds_basis_clopen [compact_space X] [t2_space X] [totally_disconnected_space X] (x : X) :
  (𝓝 x).has_basis (λ s : set X, x  s  is_clopen s) id

view this post on Zulip Patrick Massot (Apr 26 2021 at 15:46):

This says that clopen sets containing xx form a basis of neighborhoods of xx in a profinite set.

view this post on Zulip Patrick Massot (Apr 26 2021 at 15:47):

But this is stated purely in the world of topological spaces, not category theory.

view this post on Zulip Adam Topaz (Apr 26 2021 at 15:48):

Not in this form, but mathematically speaking this is equivalent to the fact that a profinite set is the limit of its continuous finite quotients, which is obtained in
https://github.com/leanprover-community/lean-liquid/blob/60497481a6d980fb7742ab528ff33420e30f99e1/src/for_mathlib/Profinite/functorial_limit.lean#L586

view this post on Zulip Adam Topaz (Apr 26 2021 at 15:49):

Of course it would be useful to have the version in terms of the neighborhood basis as well

view this post on Zulip Patrick Massot (Apr 26 2021 at 15:50):

I proved it in the neighborhood basis form, but this is not connected at all to Pro objects.

view this post on Zulip Patrick Massot (Apr 26 2021 at 15:51):

I'd be very curious to see if we could have a proof going through your work but stated in concrete form like I did. This is a waste of time in principle, but it would be nice to see if math can go in this direction in Lean (instead of from concrete to category theory)

view this post on Zulip Adam Topaz (Apr 26 2021 at 15:59):

I can explain a bit more what's going on in this abstract code.

Start with X : Profinite. From this, we have X.clopen_cover which is the type of all decomposititons of X into a disjoint union of clopen sets. Terms of X.clopen_cover are given a coercion to type, where, for I : X.clopen_cover, the terms U : I are the clopen sets in the cover.
The idea is to think of I : X.clopen_cover as a finite quotient of X, and the quotient map (as a locally constant map) is given by I.proj : X \to I.

There is also a partial order on the X.clopen_cover given by refinement -- I \le J if and only if I refines J. Given any such refinement I \le J, the map I \to J is denoted clopen_cover.map h where h is the proof that I \le J.

One remark: The function clopen_cover.map is actually done in more generality for any morphism of profinite sets f : X \to Y. See clopen_cover.le_rel. This condition le_rel f I J, where I : X.clopen_cover and J : Y.clopen_cover, says that I refines the pullback of J with respect to f. It was useful to state it in this way to obtain the functoriality of the limit description, but that's irrelevant for this discussion, I think.

Anyway, the link above then proves that X is isomorphic to the limit of the diagram obtained by the X.clopen_cover, where the transition maps are clopen_cover.map, and the comparison map from X to each I : X.clopen_cover is given by I.proj.

view this post on Zulip Adam Topaz (Apr 26 2021 at 16:03):

(I should probably add some docs to these files anyway... I'll try to do that later today)

view this post on Zulip Adam Topaz (Apr 26 2021 at 18:43):

@Patrick Massot I added a proof of the following lemma:

lemma nhds_eq_infi (a : X) : nhds a =  (I : X.clopen_cover), filter.comap I.proj (nhds $ I.proj a) :=

in https://github.com/leanprover-community/lean-liquid/blob/47b84603819efba93634df61c32630411ddec667/src/for_mathlib/Profinite/nhds.lean#L37
I think the assertion you need should follow easily from this. (The same file also has a start for the theorem about the nhds basis, but I'll have to finish it off later.)

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 18:58):

I absolutely agree with Patrick's comment above -- if category theory magic could somehow prove more lemmas about down-to-earth structures this would be really nice to see, and perhaps this is a chance to see it.

view this post on Zulip Adam Topaz (Apr 26 2021 at 19:03):

There's no magic. It's just that the small things one needs to prove in order to get what we need in this case have already been proven, albeit in a category-theoretic language.

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 19:13):

What I'm saying is that there are very few, if any, examples of stuff proved in a category-theoretic language actually being used to deduce API for explicit structures. This is Patrick's point. Mario has been adamant for a long time that he can't see the point of category theory, and I think this is just because he doesn't know enough mathematics to see its usefulness (it doesn't help at all with UG maths really, which is why we don't teach categories to undergraduates). But maybe we are now at the stage where we can show Mario the usefulness of this stuff.

view this post on Zulip Peter Scholze (Apr 26 2021 at 19:16):

Re usefulness of categories: Did you Serre's comments on categories (and topoi) as linked on Lieven le Bruyns blog http://www.neverendingbooks.org/

view this post on Zulip Peter Scholze (Apr 26 2021 at 19:16):

(I'm sorry you'll need to speak some french for this...)

view this post on Zulip Peter Scholze (Apr 26 2021 at 19:17):

Basically Serre is saying "categories are abstract nonsense that's better avoided, and I've never understood what topoi are supposed to be good for"

view this post on Zulip Peter Scholze (Apr 26 2021 at 19:18):

(I hope I'm not completely misrepresenting what he says... my french is a little rusty and I didn't watch it closely)

view this post on Zulip Johan Commelin (Apr 26 2021 at 19:23):

Well, in a very mundane way, LTE is mixing lots of category language with lots of non-category stuff.

view this post on Zulip Johan Commelin (Apr 26 2021 at 19:23):

We have a whole bunch of stuff that is just hands on inequality bashing with seminormed groups.

view this post on Zulip Johan Commelin (Apr 26 2021 at 19:24):

But the whole normed-spectral business is happy to use the category language. And I think that there it's a very useful book-keeping device.

view this post on Zulip Johan Commelin (Apr 26 2021 at 19:25):

Once we've packed everything up, there's a lot less that you have to drag along explicitly.

view this post on Zulip Johan Commelin (Apr 26 2021 at 19:26):

Of course this is a rather cheap application. But when we start doing 9.4 => 9.1, I think category theory will really become indispensable.

view this post on Zulip Johan Commelin (Apr 26 2021 at 19:26):

And you have to make the transition somewhere.

view this post on Zulip Johan Commelin (Apr 26 2021 at 19:27):

Re Serre: he's also the person that doesn't understand what DOUBLESTROKE\mathbb{DOUBLESTROKE} letters are good for on paper, right? :wink:

view this post on Zulip Adam Topaz (Apr 26 2021 at 19:35):

oooof shots fired!

view this post on Zulip Johan Commelin (Apr 26 2021 at 19:35):

Ooh, they are actually discussing typography just after the topos discussion :rofl:

view this post on Zulip Peter Scholze (Apr 26 2021 at 19:35):

I agree: To me, LTE is also an experiment in seeing precisely how well Lean is able to simultaneously do nontrivial category theory and nontrivial "actual arguments"; it's an argument that's simultaneously using a nontrivial amount of formal background, and subtle estimates.

But in the end, LTE is hardly an application of category theory to something concrete: The statement we're after is itself of a very category-theoretic nature. If we'd go further and prove say finiteness of coherent cohomology (as a consequence of some categorical statement, in particular the liquid stuff, as Clausen and I do), then that might count.

There are of course many easier applications of category theory to concrete things; isn't there something simple to convince Mario?

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 19:36):

That is the first time I've ever heard Serre call anyone "Tu" I think! He always called me "vous", and other people told me the same. He says at the beginning that you can't "just do a bit of category theory" (if you're Bourbaki) and looking at what e.g. Voevodsky did in UniMath and what Scott did from 2016 to 2020 in Lean (pretty much single-handedly, before Bhavik and Adam arrived) I'm very much inclined to agree with him. Serre also expresses concern about large categories and in some sense he's right -- one has to be careful with foundations (especially if one is pushing everything into ZFC, a system not at all designed for this kind of mathematics)

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 19:36):

The youtube subtitles are absolutely atrocious

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 19:37):

The problem with the easier applications of category theory to concrete things is that they already got done in a concrete way without categories (often by Mario!)

view this post on Zulip Johan Commelin (Apr 26 2021 at 19:37):

Peter Scholze said:

But in the end, LTE is hardly an application of category theory to something concrete: The statement we're after is itself of a very category-theoretic nature. If we'd go further and prove say finiteness of coherent cohomology (as a consequence of some categorical statement, in particular the liquid stuff, as Clausen and I do), then that might count.

I think it would be absolutely amazing to do the "finiteness of coherent cohomology" part in Lean. But I will not start dreaming about that for now :thinking: :smiley:

view this post on Zulip Mario Carneiro (Apr 26 2021 at 19:41):

I should remark that in my last few pair programming sessions with Johan, we added functoriality (in the literal category sense) to a bunch of things that were not explicitly functors. This made sense at first because all the lemmas were already there, they were functors already in all but name, although maybe toward the end I introduced some functors that weren't strictly necessary and/or followed "by analogy", producing a bunch of naturality subgoals that a direct proof would have avoided (until later, perhaps)

view this post on Zulip Mario Carneiro (Apr 26 2021 at 19:43):

When the goal statement is itself stated in category theoretic terms, it is definitely harder to tell which category things are required or are helping vs which are just re-packaging

view this post on Zulip Johan Commelin (Apr 26 2021 at 19:45):

But I think stating things like "all higher Ext-groups vanish" without using categorical language is uselessly painful.

view this post on Zulip Mario Carneiro (Apr 26 2021 at 19:45):

a lot of uses of functors and natural transformations seem mostly like amazon recommendations: "if you proved this, you might also like to prove that"

view this post on Zulip Johan Commelin (Apr 26 2021 at 19:45):

But actually, without those Amazon recommendations, you'll have holes slipping into your APIs

view this post on Zulip Peter Scholze (Apr 26 2021 at 19:46):

You see, and then you do these things, and finally you realize a few things have become trivial

view this post on Zulip Patrick Massot (Apr 26 2021 at 19:46):

Adam Topaz said:

Patrick Massot I added a proof of the following lemma:

lemma nhds_eq_infi (a : X) : nhds a =  (I : X.clopen_cover), filter.comap I.proj (nhds $ I.proj a) :=

in https://github.com/leanprover-community/lean-liquid/blob/47b84603819efba93634df61c32630411ddec667/src/for_mathlib/Profinite/nhds.lean#L37
I think the assertion you need should follow easily from this. (The same file also has a start for the theorem about the nhds basis, but I'll have to finish it off later.)

Maybe I wasn't clear before: I already have a proof of that. But I'm still interested in seeing the proof through category theory.

view this post on Zulip Adam Topaz (Apr 26 2021 at 19:49):

The proof is linked above. It's not as clean as it could be because of lacking API and/or automation (not because of the category theory!). Essentially one has to transport things, by hand, across a homeomorphism.

view this post on Zulip Adam Topaz (Apr 26 2021 at 20:24):

Okay then, I added a very ugly, ungolfed proof of the Lemma that @Patrick Massot was asking for above.
https://github.com/leanprover-community/lean-liquid/blob/d6d7aee9a58398df9ed2322643182eef3e5ef780/src/for_mathlib/Profinite/nhds.lean#L56

view this post on Zulip Patrick Massot (Apr 26 2021 at 20:25):

My proof is a bit shorter:

λ U, begin
  split,
  { have : connected_component x = {x},
      from totally_disconnected_space_iff_connected_component_singleton.mp _ x,
    rw connected_component_eq_Inter_clopen at this,
    intros hU,
    let N := {Z // is_clopen Z  x  Z},
    suffices :  Z : N, Z.val  U,
    { rcases this with ⟨⟨s, hs, hs'⟩, hs''⟩,
      exact s, hs', hs⟩, hs'' },
    haveI : nonempty N := ⟨⟨univ, is_clopen_univ, mem_univ x⟩⟩,
    have hNcl :  Z : N, is_closed Z.val := (λ Z, Z.property.1.2),
    have hdir : directed superset (λ Z : N, Z.val),
    { rintros s, hs, hxs t, ht, hxt⟩,
    exact ⟨⟨s  t, is_clopen_inter hs ht, hxs, hxt⟩⟩, inter_subset_left s t, inter_subset_right s t },
    have h_nhd:  y  ( Z : N, Z.val), U  𝓝 y,
    { intros y y_in,
      erw [this, mem_singleton_iff] at y_in,
      rwa y_in },
    exact toto' hdir hNcl h_nhd },
  { rintro V, hxV, V_op, -⟩, hUV : V  U⟩,
    rw mem_nhds_sets_iff,
    exact V, hUV, V_op, hxV }
end

view this post on Zulip Adam Topaz (Apr 26 2021 at 20:25):

a bit is a bit of an understatement :)

view this post on Zulip Peter Scholze (Apr 26 2021 at 20:27):

I guess this will not convince Mario then ;-)

view this post on Zulip Adam Topaz (Apr 26 2021 at 20:30):

@Patrick Massot what is toto'?

view this post on Zulip Patrick Massot (Apr 26 2021 at 20:30):

lemma toto' [compact_space X] {ι : Type*} [nonempty ι] {V : ι  set X} (hV : directed () V)
  (hV_closed :  i, is_closed (V i))
  {U : set X} (hU :  x   i, V i, U  𝓝 x) :
   i, V i  U

view this post on Zulip Patrick Massot (Apr 26 2021 at 20:31):

I should polish names but I'm listening to Serre, Dixmier and Cartier on Youtube

view this post on Zulip Patrick Massot (Apr 26 2021 at 20:32):

(Peter ruined my evening work with this link :grinning: )

view this post on Zulip Adam Topaz (Apr 26 2021 at 21:02):

Okay, golfed a bit (using the last two lines of Patrick's proof):

lemma nhds_basis (a : X) : (nhds a).has_basis (λ S, a  S  is_clopen S) id :=
begin
  constructor,
  intros S,
  split,
  { rw nhds_eq_infi,
    intro h,
    rw filter.mem_infi_iff at h,
    rcases h with T,hT,Ts,hT1,hT2⟩,
    replace hT1 :  i : T,  (A : set i.1) (hA : A  nhds (i.1.proj a)), i.1.proj ⁻¹' A  Ts i,
    { intros i,
      exact filter.mem_comap_sets.mp (hT1 i) },
    let Vs : Π (i : T), set i.val := λ i, classical.some (hT1 i),
    have hVs := λ i : T, classical.some_spec (hT1 i),
    let AA :=  (i : T), i.1.proj ⁻¹' (Vs i),
    refine AA, _,_⟩, λ x hx, _⟩,
    { rintros _ i,rfl⟩,
      rcases hVs i with h1,h2⟩,
      rw mem_nhds_sets_iff at h1,
      rcases h1 with Q,hQ,h1,h3⟩,
      apply hQ h3 },
    { refine @is_clopen_Inter X _ T hT.fintype (λ i, i.val.proj ⁻¹' (Vs i)) (λ i, _),
      refine i.val.proj.continuous.is_open_preimage _ trivial,
        is_closed.preimage i.val.proj.continuous _⟩,
      exact {is_open_compl := trivial} },
    { apply hT2,
      rintros i i,rfl⟩,
      rcases hVs i with h1,h2⟩,
      apply h2 (hx _ i,rfl⟩) } },
  { rintro V, hxV, V_op, -⟩, hUV : V  S⟩,
    rw mem_nhds_sets_iff,
    exact V, hUV, V_op, hxV }
end

view this post on Zulip Patrick Massot (Apr 26 2021 at 21:11):

That looks more reasonable. I have to sleep now, but I pushed stuff in https://github.com/leanprover-community/lean-liquid/commit/d82780a11f759afcf9febb767268c76ea98a843a

view this post on Zulip Patrick Massot (Apr 26 2021 at 21:12):

I'm pretty sure all this will end in mathlib, but maybe in LTE we will use the fancy version.

view this post on Zulip Adam Topaz (Apr 26 2021 at 21:13):

The nhds_eq_infi is much shorter now too:

lemma nhds_eq_infi (a : X) : nhds a =  (I : X.clopen_cover), filter.comap I.proj (nhds $ I.proj a) :=
begin
  let f := homeo_of_iso (as_iso ((limit_cone (X.diagram  of_Fintype)).is_limit.lift X.Fincone)),
  have := nhds_of_limit (X.diagram  of_Fintype) (f a),
  rw [nhds_of_homeo f, this, filter.comap_infi],
  congr,
  funext i,
  let P := Π (I : X.clopen_cover), I,
  have : (λ x : P, x i)  subtype.val  f = i.proj, refl,
  simpa [ this, filter.comap_comap],
end

view this post on Zulip Johan Commelin (Apr 27 2021 at 06:06):

@Patrick Massot I get an error on master:

lean-liquid/src/prop_92.lean:152:4: error: unknown identifier 'Union_basis_of_is_open'
state:
X : Type u_1,
_inst_1 : topological_space X,
_inst_2 : compact_space X,
Y : Type u_2,
_inst_3 : topological_space Y,
_inst_4 : t2_space Y,
_inst_5 : compact_space Y,
_inst_6 : totally_disconnected_space Y,
f : X  Y,
hf : embedding f,
U : set X,
hU : is_open U,
hU' : is_closed U,
hfU : is_compact (f '' U),
W : set Y,
W_op : is_open W,
hfW : f ⁻¹' W = U
  (V : set Y), is_clopen V  U = f ⁻¹' V

view this post on Zulip Johan Commelin (Apr 27 2021 at 06:07):

I didn't follow the discussions above, but it looks like this is some new lemma. It's not in mathlib, right?

view this post on Zulip Patrick Massot (Apr 27 2021 at 06:45):

Sorry about that. It's not a new lemma, it was renamed recently by Yury. By accident I was working on an older mathlib yesterday.

view this post on Zulip Patrick Massot (Apr 27 2021 at 06:45):

This is now fixed

view this post on Zulip Johan Commelin (Apr 27 2021 at 06:46):

@Patrick Massot Thanks! :octopus:


Last updated: May 09 2021 at 23:10 UTC