## Stream: condensed mathematics

### Topic: lemma 9.2

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

#### Johan Commelin (Mar 15 2021 at 15:40):

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

#### Peter Scholze (Mar 15 2021 at 15:41):

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

#### Peter Scholze (Mar 15 2021 at 15:41):

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

#### Peter Scholze (Mar 15 2021 at 15:42):

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

#### Johan Commelin (Mar 15 2021 at 15:43):

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

#### Johan Commelin (Mar 15 2021 at 15:43):

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

Hmm, OK.

#### Johan Commelin (Mar 15 2021 at 15:44):

Peter Scholze said:

I don't think you need to quantify over $a$ anymore, for example, and there's still lots of $S$'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:

#### Peter Scholze (Mar 15 2021 at 15:45):

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

#### Peter Scholze (Mar 15 2021 at 15:45):

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

#### Johan Commelin (Mar 15 2021 at 15:47):

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

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

#### Peter Scholze (Mar 15 2021 at 15:48):

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

#### Peter Scholze (Mar 15 2021 at 15:48):

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

#### Peter Scholze (Mar 15 2021 at 15:49):

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

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

#### 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=A_1\sqcup\ldots\sqcup A_n$, you can find a partition $B=B_1\sqcup\ldots\sqcup B_n$ extending it. For this, you can first spread any $A_i$ individually into a clopen subset $B_i'$ of $B$, and then set $B_1=B_1'$, $B_2=(B_1'\cup B_2')\setminus B_1'$, ..., $B_{n-1}=(B_1'\cup\ldots\cup B_{n-1}')\setminus (B_1'\cup\ldots\cup B_{n-2}')$ and $B_n=B\setminus (B_1'\cup\ldots\cup B_{n-1}')$.

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

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

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

#### Patrick Massot (Apr 26 2021 at 08:01):

Actually I don't follow that. What do you mean by "spread any $A_i$ into a clopen subset $B_i'$ of $B$"?

#### Peter Scholze (Apr 26 2021 at 08:04):

Find some clopen subset $B_i'$ of $B$ with $A_i=A\cap B_i'$.

#### 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]$ with a discrete set $\{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.)

#### Peter Scholze (Apr 26 2021 at 08:06):

Is the Tietze extension lemma in Lean?

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

#### 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 $A$ as the cofiltered intersection of the clopen subsets $\tilde{A}\subset B$ containing $A$, and then thinking in terms of pro-(finite sets), it is clear that any map from $A$ to a finite set extends to some $\tilde{A}$. Thus, we can assume that $A$ is clopen in $B$, but then it's very easy.

#### Peter Scholze (Apr 26 2021 at 08:13):

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

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

#### 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 $\overline{\mathcal{M}}_{r'}(S)_{\le r'c}^a$ to $\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?

#### Peter Scholze (Apr 26 2021 at 09:19):

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

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

#### Peter Scholze (Apr 26 2021 at 09:20):

But that's just one way to think about it

Ok, thanks.

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

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

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


#### Patrick Massot (Apr 26 2021 at 15:46):

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

#### Patrick Massot (Apr 26 2021 at 15:47):

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

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

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

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

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

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

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

#### 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.) #### 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. #### 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. #### 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. #### 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/ #### Peter Scholze (Apr 26 2021 at 19:16): (I'm sorry you'll need to speak some french for this...) #### 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" #### 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) #### 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. #### 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. #### 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. #### 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. #### 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. #### Johan Commelin (Apr 26 2021 at 19:26): And you have to make the transition somewhere. #### Johan Commelin (Apr 26 2021 at 19:27): Re Serre: he's also the person that doesn't understand what $\mathbb{DOUBLESTROKE}$ letters are good for on paper, right? :wink: #### Adam Topaz (Apr 26 2021 at 19:35): oooof shots fired! #### Johan Commelin (Apr 26 2021 at 19:35): Ooh, they are actually discussing typography just after the topos discussion :rofl: #### 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? #### 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) #### Kevin Buzzard (Apr 26 2021 at 19:36): The youtube subtitles are absolutely atrocious #### 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!) #### 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: #### 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) #### 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 #### 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. #### 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" #### Johan Commelin (Apr 26 2021 at 19:45): But actually, without those Amazon recommendations, you'll have holes slipping into your APIs #### 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 #### 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.

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

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

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


#### Adam Topaz (Apr 26 2021 at 20:25):

a bit is a bit of an understatement :)

#### Peter Scholze (Apr 26 2021 at 20:27):

I guess this will not convince Mario then ;-)

#### Adam Topaz (Apr 26 2021 at 20:30):

@Patrick Massot what is toto'?

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


#### Patrick Massot (Apr 26 2021 at 20:31):

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

#### Patrick Massot (Apr 26 2021 at 20:32):

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

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


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

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

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


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


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

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

#### Patrick Massot (Apr 27 2021 at 06:45):

This is now fixed

#### Johan Commelin (Apr 27 2021 at 06:46):

@Patrick Massot Thanks! :octopus:

Last updated: May 09 2021 at 23:10 UTC