col_exact

Stream: condensed mathematics

[Johan Commelin]

It's time to start the attack on the final missing piece in the proof of thm 9.5.
@Adam Topaz @Heather Macbeth @Patrick Massot Can we now state 8.19 and 9.2? Do you already have something in this direction?

[Adam Topaz]

Here is where I am with 8.19:

1. The Cech nerve is constructed here:
   https://github.com/leanprover-community/lean-liquid/blob/d075271b5099d8c1b174f87d8b253d979483b205/src/for_mathlib/cech/basic.lean#L112

2. The cochain complex associated to a cosimplicial object is here:
   https://github.com/leanprover-community/lean-liquid/blob/d075271b5099d8c1b174f87d8b253d979483b205/src/for_mathlib/simplicial/complex.lean#L114

3. The proof that a split arrow yields a contracting homotopy on cochain complexes is contained in this file:
   https://github.com/leanprover-community/lean-liquid/blob/cech_stuff/src/for_mathlib/cech/contracting_homotopy.lean

4. Now, the fact that any morphism of profinite sets can be written as a limit of arrows of finite sets is here:
   https://github.com/leanprover-community/lean-liquid/blob/d075271b5099d8c1b174f87d8b253d979483b205/src/for_mathlib/Profinite/functorial_limit.lean#L963
   and the fact that such arrows of finite sets are "covers" (i.e. surjective) given the original morphism of profinite sets is surjective is the theorem surjective_of_surjective in the same file.

What we still need is the fact that the Cech nerve construction commutes with limits, and the fact that the locally_constant construction commutes with colimits. After that, we will be able to prove the first part of 8.19 (i.e. before taking completions) without too much trouble. I don't know the status of 8.1 from the blueprint. If I recall there was some work toward 8.1 from the blueprint (by @Patrick Massot perhaps?).

[Johan Commelin]

Thanks for the detailed update.

[Johan Commelin]

Do you think you can already state and sorry 8.19, with what you've got?

[Adam Topaz]

Yeah, I can try to do that this afternoon

[Johan Commelin]

Once we have sorried statements of 8.19 and 9.2 we can start a divide-and-conquer approach (-;

[Patrick Massot]

Proposition 8.1 from the blueprint has been fully done for a long time, but I forgot to update the blueprint.

[Patrick Massot]

I'll resume working on 9.2 from Analytic tomorrow (having two numbering schemes is pretty annoying...)

[Patrick Massot]

I'm working on updating the blueprint to reflect the Lean proof of Proposition 8.1. I wonder how deep I should go into the tower of lemmas leading to it. The main statement is here (there are no 4-terms complexes there, but they are barely hidden). The density of ker g in ker \hat g is inlined in the blueprint, whereas it is stated separately in Lean. And then there is the whole story of writing elements as sums converging fast enough. In Lean this is sliced pretty thinly with this lemma which uses this one. Should I keep Peter's writeup or state one or more lemmas from our mess?

[Patrick Massot]

Note that the fast converging sum lemma was originally formalized with another application in mind (around the weak vs strong exactness discussion) so it may be useful at some point anyway.

[Johan Commelin]

I wouldn't worry too much about how closely to reflect the lean

[Johan Commelin]

Patrick Massot said:

I'll resume working on 9.2 from Analytic tomorrow (having two numbering schemes is pretty annoying...)

At least the schemes are proper, and we can try to keep them separated (-;

[Patrick Massot]

Ok, I'll try to keep the original proofs as much as possible then. I'll still state the 3 terms version because I suspect the 4-term corollary that is currently stated will be stated directly in a bundled context (with categories).

[Patrick Massot]

Still about Proposition 8.17 in Analytic.pdf, @Peter Scholze the version on https://github.com/PeterScholze/Analytic has a "for all $\widehat{y}$ in $\widehat{M}_1$" in the conclusion where you probably mean "for all $\widehat{y}$ in $\ker \widehat{d}_1$". And the version on http://www.math.uni-bonn.de/people/scholze/Notes.html is still having the old statement that is not quite correct.

[Peter Scholze]

Ha, my version control hasn't worked so well. Fortunately Johan has an updated version on GitHub... will correct!

[Adam Topaz]

Well, it's a mess right now with more basic things missing than I had anticipated, but here's the statement of Prop 8.19:
https://github.com/leanprover-community/lean-liquid/blob/79bec5091a9690d8c67d2215203cbffd30d02797/src/prop_819.lean#L55

I'll have to clean up some of the code before merging this to master. I'll try to do this over the next few days. The main thing I'm not too happy about is all this nonsense with augmentation. I think instead of going through several steps like is done in the link above, I will construct the augmented cochain complex by hand. I think this would also make it easier to relate to the complexes that are being used in the main theorem.

[Johan Commelin]

Do you think you can reuse some of https://github.com/leanprover-community/lean-liquid/blob/master/src/simplicial/alternating_face_map.lean ?

[Adam Topaz]

Probably, but I need as much functoriality as possible to make the argument work.

[Adam Topaz]

I already reused some of your lemmas from that file in cosimplicial_object.to_complex

[Johan Commelin]

Ok, I see.

[Johan Commelin]

Well, making this version more functorial shouldn't hurt wherever I use it. Probably only needs minor adjustments (replacing F with F.obj).

[Adam Topaz]

Another annoying thing is that it seems the right_op stuff from the category theory library seems to be missing some constructions (like taking an opposite of a natural transformation)

[Scott Morrison]

I'll hit merge as soon as you PR it. :-)

[Adam Topaz]

Scott Morrison said:

I'll hit merge as soon as you PR it. :-)

#7505

[Adam Topaz]

This should be helpful to go back-and-forth between simplicial and cosimplicial objects :)

[Adam Topaz]

I've updated the code in for_mathlib/simplicial/complex with a new definition of the alternating face map complex, which is functorial as a functor from augmented cosimplicial objects.

In my opinion, the definition of an augmented (co)simplicial object has settled on the following (in the simplicial case, for example):

@[simps]
def const : C ⥤ simplicial_object C := category_theory.functor.const _

variable (C)

/-- Augmented simplicial objects. -/
@[derive category, nolint has_inhabited_instance]
def augmented := comma (𝟭 (simplicial_object C)) const

I chose this because I think it's the easiest to work with given the definition of the Cech nerve that I now have.
The functorial version of cocomplex works with such a definition of an augmented cosimplicial object, and its values should be (more-or-less :smile: ) defeq to what Johan has in simplicial/alternating_face_map.lean

[Johan Commelin]

I get the impression that part of the col_exact argument is the following step:

import system_of_complexes.basic

open_locale nnreal big_operators
open category_theory opposite

variables (C : system_of_complexes)

def norm_exact_complex (D : cochain_complex SemiNormedGroup ℕ) : Prop :=
∀ (m : ℕ) (ε : ℝ≥0) (hε : 0 < ε) (x : D.X (m+1)) (hx : D.d _ (m+2) x = 0),
  ∃ y : D.X m, D.d _ _ y = x ∧ nnnorm y ≤ (1 + ε) * nnnorm x
-- this probably needs a little bit extra about degree `0`, but I don't know what exactly

lemma weak_exact_of_factor_exact (k K : ℝ≥0) [fact (1 ≤ k)] (m : ℕ) (c₀ : ℝ≥0)
  (D : ℝ≥0 → cochain_complex SemiNormedGroup ℕ)
  (f : Π c, C.obj (op $ k * c) ⟶ D c)
  (g : Π c, D c ⟶ C.obj (op c))
  (hD : ∀ c, norm_exact_complex (D c)) :
  C.is_weak_bounded_exact k K m c₀ :=
begin
  sorry
end

[Johan Commelin]

I am either misunderstanding the proofs, and this lemma is nonsense. Or I'm being dumb, and not seeing why this is true.

[Johan Commelin]

Edit: I was missing the assumption hfg, which says that f and g factor the restriction maps of C

[Peter Scholze]

OK; is there still a math problem?

[Johan Commelin]

Yes, the hfg was not what I was confused about. That was just a silly thing I forgot when I wrote the post.

[Peter Scholze]

Let me translate this into math: If $D_c^\bullet$ is a system of complexes such that $D_{kc}^\bullet\to D_c^\bullet$ factors over an exact complex $C_c^\bullet$, with some bounds, then $D_c^\bullet$ is weak exact. (I'm ignoring the factor $K$ here.)

[Johan Commelin]

The point is that norm_exact_complex asks hx : D.d _ _ x = 0

[Johan Commelin]

But for weak bounded exactness you need to prove something for all x.

[Johan Commelin]

Probably there's a simple trick that I'm missing.

[Peter Scholze]

I think there is: Given any $x$, you can find some other $x'$ with $d(x')=d(x)$ and $||x'||\leq (1+\epsilon)||d(x)||$; then $d(x-x')=0$ and you can find some $y$ with $dy=x-x'$ and $||y||\leq (1+\epsilon)||x-x'||$. But then $||x-dy||=||x'||\leq (1+\epsilon)||dx||$.

[Johan Commelin]

Aha, let me see if I can understand that

[Peter Scholze]

This is an argument that happens on $C$; then afterwards you can translate to $D$

[Johan Commelin]

Peter Scholze said:

I think there is: Given any $x$, you can find some other $x'$ with $d(x')=d(x)$ and $||x'||\leq (1+\epsilon)||d(x)||$;

But here you are making some assumption on the differentials and the normed groups that appear in the complex, right?
This is not true for an arbitrary bounded morphism $d$.

[Peter Scholze]

I'm using the norm exactness one degree higher: $d(x)$ lies in the kernel of the next differential, so you can use that hypothesis

[Peter Scholze]

Is it OK?

[Johan Commelin]

Sorry, we had a minor emergency with one of the kids (nothing serious), so I haven't really done anything yet.

[Peter Scholze]

Oh OK; no worries! I hope it's fine

[Johan Commelin]

She's sleeping again... (-;

[Johan Commelin]

I'm still confused. Maybe it's getting too late. $d(x)$ lies in the kernel of the next differential. But only if I move $d(x)$ to $D$ then I get some preimage $x'$ for $f(d(x))$ with $\|x'\| \le (1 + \varepsilon) \|f(d(x))\|$.
So it feels like I'm still doing something wrong. Because I can't move $x'$ back to $C$.

[Johan Commelin]

But may I should just try to continue working with this $x'$?

[Peter Scholze]

The whole argument should happen in $C$

[Peter Scholze]

Sorry, $D$!

[Peter Scholze]

I mean the complex that is actually exact

[Peter Scholze]

I think when I translated your code into math, I mistranslated this

[Johan Commelin]

Aah! Confusion is gone (-;

[Johan Commelin]

Now I can make sense of what you wrote :smile:

[Johan Commelin]

There are 3 easy sorrys left. (Mostly d commutes with f and g, that kind of stuff.)
And then there is the case i = 0. But for that, I think we need to also modify the statement of 8.19 as it is currently written in Lean.

[Johan Commelin]

Apart from that, the columns $\hat V(Cech nerve)$ are weak bounded exact.

[Johan Commelin]

Of course that still has to be glued to the columns in the double complex. But it feels like 1/3 of the argument is done.

[Johan Commelin]

Thanks for explaining the trick

[Peter Scholze]

Well, sorry for not properly explaining it in the notes :wink:

[Johan Commelin]

The sorrys are in thm95/col_exact_prep.lean in case someone else wants to work on them

[Johan Commelin]

I'm off to bed now.

[Johan Commelin]

This part is now complete, modulo the degree 0 thing.

[Peter Scholze]

What's the matter with degree 0?

[Johan Commelin]

Not so much, but it's just that prop819 is currently phrased only for positive degrees. Adam told me he will rephrase it at some point.

[Adam Topaz]

I think the statement of prop819 will stay as is @Johan Commelin . I wanted to use the X_next, d_to, etc. API to have one statement that also takes care of degree zero, but these definitions involve some isomorphism under the hood which we a priori have no control over. Since the statement involves norms, this would make the proof much more tedious as one would have to unfold everything to see that this isomorphism is really an eq_to_iso hence strictly norm preserving... I think it would be much easier to just take care of degree 0 as a separate case

[Adam Topaz]

The degree 0 case is easy actually since the map from degree zero to degree one is pullback along a surjective map of Profinite sets, so seeing that it's injective is easy

[Johan Commelin]

Totally fine with me. If you push the statement of injectivity at some point, then I will use it for that sorry.

[Adam Topaz]

Sure, that should be quick, I can do that later today

[Adam Topaz]

@Johan Commelin I added a proof of the degree zero case. It's a little messy -- feel free to golf + move + cut + whatever...
https://github.com/leanprover-community/lean-liquid/blob/ab1eabe4fc36f18e1a1a833469f29802b8f01ae3/src/prop819.lean#L183

[Johan Commelin]

Thanks, I'll take a look

[Johan Commelin]

The degree 0 case is now also done. Current sorry count:

1       src/prop819.lean
1       src/thm95/default.lean
22      src/thm95/col_exact.lean
9       src/thm95/constants.lean
2       src/prop819/locally_constant.lean
Total:  35

[Peter Scholze]

So to get the column exactness, it remains to apply 9.2 and the dual snake lemma? (And finish 8.19, of course.)

[Johan Commelin]

And the canonical isomorphisms!

[Johan Commelin]

Rough estimate: I'm halfway done with applying 9.2 and the dual snake lemma.

[Peter Scholze]

pff, canonical isomorphisms :stuck_out_tongue_wink:

[Johan Commelin]

But after that we'll have two complexes that are "obviously the same". But they need to be related by the canonical isomorphisms
$\mathrm{Hom}(\Lambda^{(m)}, M)^{\mathrm{BD}_q} \cong \left(\mathrm{Hom}(\Lambda', M)^{\mathrm{BD}_q}\right)^{m/\mathrm{Hom}(\Lambda, M)^{\mathrm{BD}_q}}$

[Patrick Massot]

Do you still need help which doesn't require being very familiar with the final part of the proof?

[Johan Commelin]

aahrg, where is my LaTeX-typo??

[Patrick Massot]

No dollars at the end I'd say

[Johan Commelin]

Peter Scholze said:

pff, canonical isomorphisms :stuck_out_tongue_wink:

Well, they even got a mention in the PDF, so they must be important and nontrivial :rofl:

[Johan Commelin]

Actually, I guess the $(\_)^q$ should be moved inside the fibre product, on the RHS. Fixed

[Johan Commelin]

Patrick Massot said:

Do you still need help which doesn't require being very familiar with the final part of the proof?

I'll see whether I can stub out some standalone sorrys. But it's all quite heavy on the category_theory side...

[Peter Scholze]

Oh I see, there's actually some content here in merely having an isomorphism. I assumed the issue was having it sufficiently canonical/functorial

[Johan Commelin]

Bwah, it's getting quite a bit messier by the $(\_)^{\mathrm{BD}_q}$

[Johan Commelin]

Once the 9.2/dual snake lemma is done, we'll know the final constants. So then someone can get thm95/constants sorry-free.

[Riccardo Brasca]

Dual snake lemma is done, isn't' it?

[Adam Topaz]

I'm a bit stuck with 8.19. I have the exactness working fine, but, as always, the issue is about the norms.
Here's a summary. Start with a surjective morphism of profintite sets $X \to B$, write $X = \lim_i X_i$ with $X_i$ the discrete (finite) quotients of $X$. To each $X_i$, there is a unique maximal finite quotient $B_i$ of $B$ such that $X \to B$ descends to $X_i \to B_i$ and one has $(X \to B) = \lim_i (X_i \to B_i)$.

Okay, so now we take a seminormed gorup $M$, consider the Cech nerve $C_\bullet$ of $X \to B$, and consider $M(C_\bullet)$.
Write $C_\bullet^i$ for the Cech nerve of $X_i \to B_i$.
The goal is to show that $M(C_\bullet)$ satisfies this controlled exactness condition, meaning that it's exact and that for every $f$ such that $d(f) = 0$ there exists some $g$ such that $d(g) = f$ and such that $|g| \le |f|$.

If $f \in M(C_n)$ then there exists some $i$ as above such that $f$ factors via $f_i \in M(C_n^i)$ for some $i$, and by enlarging $i$ we can also ensure that $d(f_i) = 0$. The $C_n^i$ split, so the contracting homotopy gives some $g_i \in M(C_{n-1}^{i})$ such that $d(g_i) = f_i$, and looking at the image of $g_i$ in $M(C_{n-1})$ we can an element $g$ such that $d(g) = f$.

This is all fine so far. From the construction, we also know that $|g_i| \le |f_i|$, that $|g| \le |g_i|$ and $|f| \le |f_i|$. But I don't see why $|g| \le |f|$. What am I missing here?

[Adam Topaz]

If, for example, we could show that $|f_i| = |f|$, then we would be done, but I don't see why that's the case.

[Peter Scholze]

I think one can arrange $|f_i|=|f|$, possibly after enlarging $i$. Take $f_i: C_n^i \to M$, then $f = f_i|_{C_n}$, so $|f|$ depends only on the image of $C_n$ in $C_n^i$. But this image agrees with the image of $C_n^j$ for $j\geq i$ sufficiently large, and then $f_j=f_i|_{C_n^j}$ satisfies $|f_j|=|f|$.

[Peter Scholze]

Riccardo Brasca said:

Dual snake lemma is done, isn't' it?

I believe Johan meant the application of 9.2+dual snake. There'll still be an isomorphism of complexes left to prove, but this will preserve norms. So one can figure out all the constants in parallel to constructing that final isomorphism.

[Adam Topaz]

Peter Scholze said:

I think one can arrange $|f_i|=|f|$, possibly after enlarging $i$. Take $f_i: C_n^i \to M$, then $f = f_i|_{C_n}$, so $|f|$ depends only on the image of $C_n$ in $C_n^i$. But this image agrees with the image of $C_n^j$ for $j\geq i$ sufficiently large, and then $f_j=f_i|_{C_n^j}$ satisfies $|f_j|=|f|$.

Okay, so I've reworked the proof of 8.19 to rely on this condition, which I state as follows: For every $f \in M(C_n)$, there exists some $i$ and some $f_i \in M(C_n^i)$ such that:

1. the image of $f_i$ in $M(C_n)$ is $f$.
2. one has $d(f_i) = 0$.
3. one has $|f_i| = | f|$.

This assertion is the only thing left for the proof of 8.19, and it's the following sorry:
https://github.com/leanprover-community/lean-liquid/blob/53aa0d055c72778e81a249ba913fa3a49d595db6/src/prop819.lean#L242

[Peter Scholze]

Cool! (I think there's a missing condition $d(f)=0$ in what you wrote here.)

[Adam Topaz]

Oh of course... Fortunately I was careful enough to add it to the code itself :wink: (it's the assumption hf)

[Johan Commelin]

All the sorrys in col_exact.lean are done, except for the elephant in the room.

[Johan Commelin]

(Which is the canonical isomorphism between two systems of complexes that are roughly $\hat V(\_)$ applied to two isomorphic Cech nerves

[Peter Scholze]

So, taking stock, what is left?

a) Finish the proof of 8.19. Adam is working on that, and it's reduced to some basic facts about maps from profinite sets to discrete spaces, I think?

b) Fill in the canonical isomorphism in the column exactness. Johan is probably working on that?

c) Fill in the inductive definition of $k_1$ and $K_1$.

Anything else? Sounds like you're getting very close to the finish line (of 9.4+9.5)!

[Johan Commelin]

Yeah, that seems to sum it up.

[Johan Commelin]

Ooh, we'll have 9.4 with weak exactness. But we have the lemma in place to derive the version with strong exactness. So that would be < 5 minutes (-;

[Peter Scholze]

Actually one should first take a limit in 9.4 to pass to the version with profinite $S$, and then pass to strong exactness. But OK, let's leave that for the second goal of actually getting to 9.1.

[Johan Commelin]

The reason you first take the limit is to improve the constants, right? The other way could also be done I guess?

[Peter Scholze]

Yeah, both ways would be fine, but passing to the limit you will again only get weak exactness a priori

[Peter Scholze]

So it's an unnecessary back-and-forth between weak and strong exactness

[Johan Commelin]

Yeah, so that seems to be properly part of the second adventure (-;

[Johan Commelin]

All the sorrys about strictness of the isomorphism of complexes are done.

[Johan Commelin]

So the remaining sorrys are firmly in the land of "canonical isomorphisms between profinitely filtered pseudo normed groups"

[Johan Commelin]

The sort of thing that needs to be done: $(\mathrm{rescale}_{N} (M^N))^n \cong \mathrm{rescale}_N ((M^n)^N)$

[Peter Scholze]

Ah, so you already know $\mathrm{Hom}(\Lambda'^{(m)},M)\cong \mathrm{Hom}(\Lambda',M)^{m/\mathrm{Hom}(\Lambda,M)}$?

[Johan Commelin]

No no, sorry for suggesting that. That is the other big beast.

[Johan Commelin]

This is the kind of ugly that it looks like in Lean:

(Profinite.limit_cone
  (limits.wide_pullback_shape.wide_cospan
    (FLC_complex_arrow (aug_map r' Λ M N n) _ c).right
    (λ (i : ulift (fin (i + 1))), (FLC_complex_arrow (aug_map r' Λ M N n) _ c).left)
    (λ (i : ulift (fin (i + 1))), (FLC_complex_arrow (aug_map r' Λ M N n) _ c).hom))).X
 ≅
Profinite.of ↥(pseudo_normed_group.filtration
  (↥(polyhedral_lattice.Hom ↥(Cech_conerve.obj (Λ.diagonal_embedding N) i) ↥M) ^ n) c)

[Johan Commelin]

Which isn't really helpful if you don't know the definition of half of the nouns... :shrug:

[Johan Commelin]

It just shows that there is still some room for improvement, notationwise.

[Peter Scholze]

Ah too bad. But at least you got rid of $V$, I assume? That's clearly progress.

[Johan Commelin]

Note that the isomorphism as you wrote it, ignores the exponent coming from Breen--Deligne.

[Peter Scholze]

Yes, sure. I know that you also have to get rid of this one. I just wondered whether that's all that's left to do.

[Peter Scholze]

By the way, can you use the adjointness property of the Cech nerve to get a comparison map, and hence reduce to proving isomorphisms of profinitely filtered pseudonormed groups (as opposed to simplicial such)?

[Johan Commelin]

Hmm, interesting. I'm not sure if that adjunction has been done. @Adam Topaz ??

[Johan Commelin]

We would have to restructure the proof a bit. Because one of the two sides is not definitionally of the form $\hat V(\_)$.

[Johan Commelin]

So to get rid of the $\hat V(\_)$, I have to look componentwise.

[Peter Scholze]

Hmm OK. But I meant for the remaining step.

[Peter Scholze]

Isn't it left to prove an isomorphism of simplicial profinitely filtered pseudonormed groups?

[Peter Scholze]

One of which is a Cech nerve

[Peter Scholze]

(Maybe I'm talking nonsense -- I don't actually know what you are doing!)

[Adam Topaz]

Johan Commelin said:

Hmm, interesting. I'm not sure if that adjunction has been done. Adam Topaz ??

We don't have this adjunction unfortunately. I could add it if it's important

[Johan Commelin]

It's not clear to me that we can apply it easily...

[Adam Topaz]

When I previously defined the Cech nerve as a Kan extension, the adjunction was automatic, but working with the Kan extension was much more tedious in practice, so I switched to using pullbacks.

[Johan Commelin]

Hmmm, I actually think that using the adjunction might be helpful.

[Johan Commelin]

Checking that a map of simplicial complicated-gadgets is an iso is a lot easier then constructing such a map.

[Adam Topaz]

I'll add it

[Johan Commelin]

Merci!

[Johan Commelin]

Of course we don't get a free lunch. Checking that a pretty inexplicit map is an isomorphism isn't Lean-trivial either.

[Johan Commelin]

But I guess we can have a theorem that says that on each simplicial level, the map comes from the universal property of pullbacks?

[Johan Commelin]

And using that, we can hopefully show that level-wise it's bijective.

[Adam Topaz]

Yes the maps are defeq to lifting some cone to a morphism to a limit

[Adam Topaz]

I have to do other stuff for a little while, but I'll make a PR with the adjunction this afternoon

[Johan Commelin]

Would you mind also adding it to the LTE repo?

[Adam Topaz]

Sure, no problem

[Adam Topaz]

#7716

[Adam Topaz]

And I added it to LTE as well here:
https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/Cech/adjunction.lean

[Johan Commelin]

Thanks!

[Johan Commelin]

Injectivity of the canonical iso is done.

[Peter Scholze]

Tell me when I should start to put the champagne in the fridge :champagne: :wink:

[Riccardo Brasca]

We should also find a way to let Johan fill the last sorry :grinning:

[David Michael Roberts]

It would be awesome if it could be livestreamed (though I'll probably be asleep at the time, anyway) :sunglasses:

[Adam Topaz]

Okay, the first of the three main sorry's for 8.19 is done: If $X = \varprojlim_i X_i$ with $X_i$ profinite and $i$ cofiletered, and $f : X \to S$ is any locally constant function, there exists some $i$ such that $f$ factors through $X_i$.
https://github.com/leanprover-community/lean-liquid/blob/ae0bfa81bd980dd1df85299dbe0380c4b4c11ef6/src/for_mathlib/Profinite/clopen_limit.lean#L745

[Adam Topaz]

I put this separately from the prop819 file because it has a [nonempty X] assumption

[Adam Topaz]

And I'll worry about that assumption later...

[Adam Topaz]

I guess we know that when $X$ is empty that there is some sufficiently large $i$ such that $X_i$ is empty, but do I really want to do a by_cases (nonempty X) proof? :expressionless:

[Peter Scholze]

Where do you need the assumption $X$ is nonempty to start with?

[Adam Topaz]

Oh it's stupid really... the construction says: If $S$ is a discrete quotient of $X$ then there is an $i$ and a discrete quotient $T$ of $X_i$ such that $S$ is the pullback of $T$ along $X \to X_i$. This shows that $X \to X_i$ descends to an injective map $S \to T$. To get the statement about locally constant functions $f : X \to M$, we first descend to a discrete quotient, obtain such a $T$, but then we need to choose a section $T \to S$ to compose with to obtain $X_i \to M$.

[Adam Topaz]

And to obtain such a section, we need $S$ to be nonempty

[Peter Scholze]

Wait, why a section? Is $S\to T$ surjective? In any case, can't you just define the image to be $0$ for all elements of $T$ not in the image?

[Adam Topaz]

No it's injective

[Adam Topaz]

Yes, that's fine too.

[Adam Topaz]

Anyway, something has to be nonempty :smile:

[Peter Scholze]

But $M$ is a group (or is it more general here?), so it's nonempty...

[Peter Scholze]

Well, never mind in any case :-)

[Adam Topaz]

Yeah, I had it stated with M being any type. But now I've changed it to assuming that the type M is nonempty, so it should all be good now and X can be empty :smile:

[Patrick Massot]

I had the same kind of issues when proving Lemma 9.2. The fact that a normed group is always nonempty was very convenient.

[Johan Commelin]

Anyone else get deterministic timeouts in col_exact.lean around line 859 in VScode? (Compiling on the command-line works, luckily.)

[Johan Commelin]

These are really frustrating. Probably we need to very carefully mark certain things as irreducible. But I'm not very good at that dance.

[Johan Commelin]

Also... it seems that is not the way things can/should be solved in Lean 4. So if someone knows a future-proof way of making this work, that would be great!