Prop 2.1

Stream: condensed mathematics

[Adam Topaz]

I added a skeleton for the inductive case of the injectivity part of the proof of Proposition 2.1 here:
https://github.com/leanprover-community/lean-liquid/blob/14a3e29edc37b48c3f7c55dd4d546f2c81365a66/src/free_pfpng/main.lean#L232

This proof contains a bunch of relatively small sorries, some of which should be trivial, while some a bit more complicated.
Any help with these would be much appreciated!

[Johan Commelin]

So that's the first 25% of the entire proof, basically?

[Adam Topaz]

I think surjectivity will actually be a bit easier.

[Adam Topaz]

Well, once the following is sorry-free: https://github.com/leanprover-community/lean-liquid/blob/b0c7649a6aebfa8f4bda55e06e462d240cb248a2/src/condensed/ab.lean#L446

[Adam Topaz]

Essentially that will reduce the proof of surjectivity to show that for all $n$ there exists some profinite $T$ and some map of condensed sets $T \to \mathbb{Z}[S]$ and a surjective map of profinite sets $T \to \mathbb{Z}[S]_{\le n}$ such that the obvious diagram with target $\bigcup_n \mathbb{Z}[S]_{\le n}$ commutes (this $T$ is taken to be $S^n \times \{-1,0,1\}^n$ in Analytic.pdf), and I don't think that will be too difficult.

[Johan Commelin]

Ok, sounds good!

[Johan Commelin]

Does the following sorry need a mathlib refactor? Or merely a library hunt? (cc @Andrew Yang)

instance : limits.has_limits_of_size.{u} Ab.{u+1} := sorry

[Andrew Yang]

We have docs#category_theory.limits.has_limits_of_size_shrink

[Johan Commelin]

Hmm, I'm not sure if that is enough...

[Johan Commelin]

Ooh, it is!

[Adam Topaz]

In other news, Profinite.mono_free'_to_condensed_free_pfpng_induction_aux is done.

[Johan Commelin]

The decl profinite_to_condensed_unit contains a sorry. But I don't think that decl is used in the rest of the file. Do you expect to use it at some point? (There are also some commented variants all the way at the bottom of the file.)

[Adam Topaz]

Let's leave it for now, but we can probably drop it later.

[Johan Commelin]

Another mystery: src/free_pfpng/basic.lean has a broken definition now that I filled in two sorrys there.

[Johan Commelin]

I don't understand how that can happen.

[Johan Commelin]

I pushed after filling in the sorry, so now the build is broken :see_no_evil:

[Johan Commelin]

The fix was easy: add .{u u}. Still, it's surprising that filling in two sorrys of type Prop could cause this issue.

[Yaël Dillies]

Johan breaking Lean every day a little more :upside_down:

[Adam Topaz]

I just pushed a proof of

lemma epi_Profinite_to_Condensed_map_of_epi {X Y : Profinite.{u}}
  (f : X ⟶ Y) [hf : epi f] : epi (Profinite_to_Condensed.map f) :=

with a few small sorries. This will be needed for the surjectivity part of 2.1.

[Johan Commelin]

Fixed some more sorries.

[Johan Commelin]

Only 9 left in that file

[Adam Topaz]

make it 8

[Adam Topaz]

(maybe 7?)

[Johan Commelin]

6 src/free_pfpng/main.lean

[Johan Commelin]

Of which 2 seem to be in quasi-dead code.

[Johan Commelin]

Of course there is also still

4 src/condensed/ab.lean

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/blob/2bbe6f6caef14ade0dceed174b6e9dc54af6a468/src/free_pfpng/main.lean#L563
:up: that one is a pretty serious sorry.

[Adam Topaz]

I think the ones in ab.lean should be manageable.

[Johan Commelin]

I'm working on

instance Profinite.is_iso_free_to_pfpng (S : Profinite.{u}) : is_iso S.free_to_pfpng :=

[Johan Commelin]

Shouldn't be too hard.

[Adam Topaz]

Update: free_pfpng/main.lean now has 13 sorries, but no "sorried" data.

[Adam Topaz]

(Well, except for the sorry in free_pfpng_profinite_iso, but that's somehow unrelated to the crux of Prop 2.1)

[Adam Topaz]

Here's is a sorry that has zero category theory involved, and is needed for the surjectivity part of Prop 2.1

lemma Profinite.pmz_to_free_pfpng_epi_aux {T : Type*} [fintype T]
  (r : nnreal)
  (f : T → ℤ)
  (hf : ∑ i : T, ∥ f i ∥₊ ≤ r) :
  ∃ (e : fin ⌊r⌋₊ → pmz) (t : fin ⌊r⌋₊ → T),
  (∑ (i : fin ⌊r⌋₊), (λ (s : T), if (t i = s) then (e i : ℤ) else 0)) = f :=
sorry

(Here pmz is $\{1,-1,0\}$.)
The lemma is here, in case anyone wants to take a look:
https://github.com/leanprover-community/lean-liquid/blob/ea406127dcb3d2ad72e51f9b59b4bc805b1f8f52/src/free_pfpng/main.lean#L910

[Johan Commelin]

@Adam Topaz Mathlib contains sign_type. Could that be reused in place of pmz?

[Adam Topaz]

Sure, i can switch out pmz.

[Johan Commelin]

Other question: shall we split the file?

[Adam Topaz]

yes, probably.

[Adam Topaz]

I can do it -- give me about 30 mins

[Johan Commelin]

All the sorries are at the bottom, and I need to wait quite a while to get rid of orange bars in the first 750 lines

[Adam Topaz]

The other chunky sorry left in this file is this:
https://github.com/leanprover-community/lean-liquid/blob/ea406127dcb3d2ad72e51f9b59b4bc805b1f8f52/src/free_pfpng/main.lean#L960

[Yaël Dillies]

This looks like a fun sorry.

[Adam Topaz]

Yeah, it's one of those things that's "trivial" mathematically, but is hard nontrivial to formalize.

[Adam Topaz]

Actually, another question: Do we have a name for (λ (s : T), if (t i = s) then (e i : ℤ) else 0)? It's just finsupp.single but as a plain function.

[Johan Commelin]

Is there docs#function.single? (Ans: no)

[Johan Commelin]

@Yaël Dillies Do you want to take it on?

[Yaël Dillies]

I can try while I'm on the train.

[Adam Topaz]

Okay, I split up the files. The lemma in question can now be found in free_pfpng/epi.lean near the bottom (and it now uses sign_type as well)

[Yaël Dillies]

Johan Commelin said:

Is there docs#function.single? (Ans: no)

You can use docs#function.update

[Yakov Pechersky]

docs#pi.single!

[Yaël Dillies]

Hmm... tasty

(finset.univ.to_list.map $ λ t, repeat (sign $ f t) (f t).nat_abs).join.inth

[Yaël Dillies]

I would be glad if someone had a better idea.

[Yakov Pechersky]

What's inth?

[Johan Commelin]

(Btw: I'm looking at the first two sorrys in epi.lean.)

[Johan Commelin]

Yakov Pechersky said:

What's inth?

list.nth but for inhabited types.

[Johan Commelin]

So it returns default when out of bounds.

[Johan Commelin]

Fixed three sorries

[Yaël Dillies]

Okay I think I got an idea which makes it trivial

[Johan Commelin]

Another sorry down

[Johan Commelin]

4 left in this file, 1 is for @Yaël Dillies, 2 are in comments, and then the final one at the bottom.

[Adam Topaz]

I'll try to take care of the last one.

[Johan Commelin]

Cool! I saw you pushed a bunch in the past hours. Looks like Prop 2.1 is almost done!

[Johan Commelin]

@Yaël Dillies Is your "idea which makes it trivial" something that you think you can push soonish?

[Yaël Dillies]

Yes! I'm working on it right now.

[Yaël Dillies]

I can tell you already that I further need [nonempty T].

[Johan Commelin]

I'm 99% sure that this is fine

[Johan Commelin]

In practice, we have T : discrete_quotient S. So if S is nonempty, then T is nonempty as well.
This means that we need to make a case distinction in the proof of

instance Profinite.pmz_to_free_pfpng_epi (S : Profinite.{u}) (j : nnreal) :
  epi (S.pmz_to_free_pfpng j) :=

on whether S is empty or not.

[Johan Commelin]

Hmm, that might actually be an issues for empty S and j \ge 1. We have

def Profinite.pmz_to_free_pfpng (S : Profinite.{u}) (j : nnreal) :
  S.pmz ⌊j⌋₊ ⟶ (ProFiltPseuNormGrp₁.level.obj j).obj S.free_pfpng :=

which is in other words the map

$$(S \times \{-1,0,1\})^{\lfloor j \rfloor} \longrightarrow \{0\}$$

for all j.

[Johan Commelin]

If S is empty, then S.free_pfpng is the trivial group, and level j of that will always be the singleton $\{0\}$.

[Johan Commelin]

But for j \ge 1 the LHS is empty, so there cannot be a surjective map.

[Johan Commelin]

So we probably have to do the case split on whether S is empty in another place of the proof.

[Yaël Dillies]

Yeah, exactly. The sorry you ask for is straight up wrong when T is empty, because there's no map ℕ → T.

[Yaël Dillies]

Sorry killed

[Yaël Dillies]

I didn't have cache so I don't know what I broke nor whether the noncomputable_theory introduced decidability issues that I didn't have in local.

[Johan Commelin]

Great! Thanks a lot.

[Yaël Dillies]

The trick was to generalize fintype T to s : finset T and then induct.

[Johan Commelin]

I just want to remark that this means we are now very very close to the point where all that's left is "just some homological algebra". All the condensed stuff will be done. Once Filippo and Kevin finish the 6.9/7.2 stuff, all the pseudo-normed-group stuff will also be done.
Then only the BD lemma remains, and a bunch of glue.

[Adam Topaz]

Oops! Yeah, I should have distinguished the (non)empty case.

In the empty case, S.free_pfpng and its condensed variants are trivial, and we already know that the comparison map is a mono, so that should be enough to show it's an iso.

[Adam Topaz]

So I think you may as well assume that S is nonempty (hence T is nonempty) in the whole file free_pfpng/epi.lean and do the case split in free_pfpng/main.lean.

[Adam Topaz]

I can do that when I get to my office in a couple of hours, if it's not taken care of before then ;)

[Adam Topaz]

@Yaël Dillies did you change the type of the lemma in question?

[Adam Topaz]

(except for the nonempty assumption, of course)

[Yaël Dillies]

I believe not, except for adding decidable_eq T and nonempty T.

[Adam Topaz]

It's okay, I fixed it.

[Adam Topaz]

You changed the functions from having domain fin _ to N, the sum to use finset.range, and the conclusion to say $\forall t, ...$ instead of an equality of functions. It was just a few lines to fix.

[Yaël Dillies]

Ah yeah, sorry I forgot

[Adam Topaz]

Okay, I took care of the empty case as well.

[Adam Topaz]

So now mono.lean, epi.lean are sorry-free, and main.lean is sorry-free except for some naturality proof and some isomorphism which should be easy to construct. There are a few sorries left in condensed/coproducts and condensed/ab

[Johan Commelin]

Amazing!

[Johan Commelin]

Do you want to throw away the two commented sorrys in epi.lean?

[Johan Commelin]

Or should they stay around for something?

[Adam Topaz]

Ah, those were just some failed experiment. I removed them

[Adam Topaz]

No more sorries in coproducts.

[Adam Topaz]

Now condensed/ab.lean is sorry-free as well

[Adam Topaz]

So Prop 2.1 is (more-or-less) sorry-free

[Johan Commelin]

#print axioms free_pfpng_profinite_iso
-- prints
propext
quot.sound
classical.choice

[Johan Commelin]

Adam, that was a heroic effort! You pulled it off in a couple of days. Fantastic!

[Johan Commelin]

I just updated the blueprint. Should have another green oval in a couple of minutes.

[Johan Commelin]

It's green: https://leanprover-community.github.io/liquid/dep_graph_section_2.html

[Peter Scholze]

I was chatting with Johan a week ago, asking him about what's left to do. My guess was that Proposition 2.1 would be the hardest remaining bit! So I think you're really closing in on the finish line here.

[Peter Scholze]

(Congratulations Adam!!)

[Adam Topaz]

I should add one more point regarding Prop 2.1 -- I think it's a fairly important milestone for our formalization effort, since its the key result which ties together the condensed side with the more concrete CompHausFiltPseuNormGroup side.

[Johan Commelin]

Yes, it is a nontrivial computation about condensed sets. Maybe the only nontrivial one we need.