lemma 9.2

Stream: condensed mathematics

[Johan Commelin]

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]

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

[Peter Scholze]

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

[Peter Scholze]

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]

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

[Johan Commelin]

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]

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

[Peter Scholze]

Hmm, OK.

[Johan Commelin]

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]

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

[Peter Scholze]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Peter Scholze]

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

[Peter Scholze]

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

[Johan Commelin]

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

[Peter Scholze]

OK, Great! Then it should work in this generality

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

So, now we can write $x \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.

[Johan Commelin]

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

[Peter Scholze]

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

[Heather Macbeth]

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 $A\subset B$ of profinite sets and a map $f_A: A\to \widehat{V}$, there is an extension $f_B: B\to \widehat{V}$ of $f_A$ with $||f_B||\leq (1+\epsilon)||f_A||$. To see this, write $f_A$ as a (fast) convergent sum of maps that factor over a finite quotient of $A$; for maps factoring over a finite quotient of $A$, the extension is clear (and can be done in a norm-preserving way), as any map from $A$ to a finite set can be extended to a map from $B$ 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 $\widehat{V}$ be a complete normed group (no knowledge about the $V$ it came from), and that $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?

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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.

[Peter Scholze]

@Heather Macbeth That's right.

[Bhavik Mehta]

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?

[Peter Scholze]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Peter Scholze]

I think 8.17 could be helpful here, applied to $M'$ the locally constant functions from $B$ to $V$, and $M$ the locally constant functions from $A$ to $V$ (and $M''=0$)

[Peter Scholze]

Then one needs to see that any locally constant map from $A$ to $V$ extends to a locally constant map from $B$ to $V$ 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?

[Patrick Massot]

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 $A$ to a finite set $C$ continuously extends to $B$. 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?

[Peter Scholze]

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]

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]

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]

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]

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

[Peter Scholze]

(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]

Is the Tietze extension lemma in Lean?

[Patrick Massot]

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

[Peter Scholze]

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]

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]

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]

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]

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

[Peter Scholze]

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

[Peter Scholze]

But that's just one way to think about it

[Patrick Massot]

Ok, thanks.

[Adam Topaz]

@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]

@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]

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]

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

[Patrick Massot]

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

[Adam Topaz]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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]

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

[Adam Topaz]

@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]

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]

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]

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]

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]

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

[Peter Scholze]

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]

(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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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]

And you have to make the transition somewhere.

[Johan Commelin]

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

[Adam Topaz]

oooof shots fired!

[Johan Commelin]

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

[Peter Scholze]

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]

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]

The youtube subtitles are absolutely atrocious

[Kevin Buzzard]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

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

[Peter Scholze]

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

[Patrick Massot]

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]

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]

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]

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]

a bit is a bit of an understatement :)

[Peter Scholze]

I guess this will not convince Mario then ;-)

[Adam Topaz]

@Patrick Massot what is toto'?

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Adam Topaz]

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]

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]

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

[Adam Topaz]

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]

@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]

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

[Patrick Massot]

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]

This is now fixed

[Johan Commelin]

@Patrick Massot Thanks! :octopus:

[Johan Commelin]

I've finished the statement of 9.2, @Patrick Massot (just compiling locally before I push)

[Johan Commelin]

It might make sense to move all the extend stuff to a different file, because it doesn't need the "heavyweight" imports that the statement of 9.2 needs.

[Patrick Massot]

I just did that move (and also removed silly unneeded assumptions), see the module docstring of https://github.com/leanprover-community/lean-liquid/blob/master/src/prop_92/extension_profinite.lean

[Patrick Massot]

But I need to sleep before the next steps.

[Johan Commelin]

Is it just me, or do you also need a lot less case-bashing than before?

[Patrick Massot]

It is just you, the core proof didn't change at all.

[Johan Commelin]

I guess I glossed over embedding.ex_discrete_quotient this morning :see_no_evil:

[Patrick Massot]

Latest status update: Lemma 9.2 from the analytic lectures notes is now completely checked in Lean. The proof I formalized is a variation on Peter's proof. It does not involve any continuous function with values in $\widehat{V}$. In my proof $\widehat{V}(M)$ is used purely as an abstract completion of $V(M)$. Also, I don't extend any function to infinitely many levels of the filtration, all the action happens in $V(M_{\le c})$ and $V(M_{\le r'c})$. There is an infinite inductive extension process but I "conjugate by $T$" at each step to stay in the same level.

Some details can be found in the current blueprint (that will soon be deployed online). I have added yet another technical definition in Def 4.1 (hoping people won't notice too much in the given context). It allows to nicely phrase Lemma 4.2 which abstracts the part of this argument which is common with the controlled exactness stuff (Prop 4.3 in the blueprint). Then the new one is Lemma 5.8 in the blueprint. Many more details can be found in the Lean code.