main statement

Stream: condensed mathematics

[Johan Commelin]

I just pushed a file challenge.lean. Here's a little snapshot:

variables (p' p : ℝ≥0) [fact (0 < p')] [fact (p' ≤ 1)] [fact (p' < p)] [fact (p ≤ 1)]
variables (S : Profinite.{1})
variables (V : Type 1) [normed_group V] [module ℝ V] [normed_space' ℝ p V] -- `V` is a `p`-Banach

def real_measures.condensed : Profinite ⥤ Condensed Ab :=
Profinite.extend (real_measures.functor p') ⋙ CompHausFiltPseuNormGrp₁.to_Condensed

local notation `ℳ` p' := real_measures.condensed p'

local notation `Ext` i `,` A `,` B := ((Ext ℤ (Condensed Ab) i).obj (op A)).obj B

theorem main_challenge (i : ℕ) (hi : 0 < i) :
  Ext i , (ℳ p').obj S , Condensed.of_top_ab V :=
sorry

[Johan Commelin]

Feel free to beautify!

[Johan Commelin]

Also, this statement still depends on a lot of sorrys. For example, that Condensed Ab is an abelian category with enough projectives.

[Riccardo Brasca]

Do you think proving it has enough projectives is a reasonable "not too difficult" project? I have some time in the next weeks, and I would be very happy to start working with the category theory part of the library!

[Johan Commelin]

The main statement is nonsense! I completely forgot to formalize = 0 in the main statement. Fixed

[Johan Commelin]

@Riccardo Brasca There is a lot of code that Bhavik wrote for the "basic condensed API", but I don't know where that code is.

[Johan Commelin]

It would be helpful if @Bhavik Mehta could push his code somewhere where others can build on top of it.

[Adam Topaz]

The key thing we need to prove that Cond Ab has enough projectives is the sheafification in Cond Ab. This lets you construct the left adjoint to the forgetful functor, and applying that to the condensed set of a projective object of CompHaus (which mathlib knows there are enough of) gives you projectives in Cond Ab. I think constructing the sheafification will be a nontrivial task here.

[Johan Commelin]

@Adam Topaz I guess we can assert the existence of sheafification and the fact that it is adjoin to the inclusion into presheaves. That way we can continue building other stuff on top of that.

[Adam Topaz]

I added

instance : is_right_adjoint (Sheaf_to_presheaf _ _ : Condensed Ab.{u+1} ⥤ _) := sorry

def forget_to_CondensedType : Condensed Ab.{u+1} ⥤ CondensedSet :=
{ obj := λ F, ⟨F.val ⋙ forget _, begin
    cases F with F hF,
    rw (presheaf.is_sheaf_iff_is_sheaf_forget _ _ (forget Ab)) at hF,
    rw ← is_sheaf_iff_is_sheaf_of_type,
    assumption,
    apply_instance
  end ⟩,
  map := λ A B f, whisker_right f _ }

instance : is_right_adjoint forget_to_CondensedType := sorry

[Adam Topaz]

The second sorry should follow from the first

[Johan Commelin]

Thanks, I pulled.

[Adam Topaz]

Somewhat related to this, we currently define CondensedSet using SheafOfTypes as opposed to Condensed Type* (the two are equivalent but not defeq). Do we want to change this?

[Johan Commelin]

I don't have a strong feeling about that.

[Johan Commelin]

So far we haven't used condensed sets yet. Only condensed abelian groups.

[Adam Topaz]

It would save one of the rw lines in the proof above if we do, but it's not a huge deal.

[Johan Commelin]

I guess the sticking point is sheafification. And that will be hard no matter which definition (-;

[Adam Topaz]

Checking the sheaf condition is easier in SheaOfTypes which could be useful later on.

[Johan Commelin]

@Adam Topaz Don't you think we should provide the sheafification functors explicitly?

[Peter Scholze]

Regarding projectives, let me point out that besides their existence, we also need to (later) know quite explicitly their structure, as in Proposition 2.1 of Analytic.pdf. That proposition might be another good intermediate target.

[Johan Commelin]

So this file https://github.com/leanprover-community/lean-liquid/blob/master/src/challenge.lean has the statement of the main challenge. Are there ways to make those Ext groups look better? I want to show this off in a talk two weeks from now.

local notation `ℳ` p' := real_measures.condensed p'

local notation `Ext` i `,` A `,` B := ((Ext ℤ (Condensed Ab) i).obj (op A)).obj B

theorem main_challenge (i : ℕ) (hi : 0 < i) :
  is_zero (Ext i , (ℳ p').obj S , Condensed.of_top_ab V) :=
sorry

[Johan Commelin]

Those ,s are a very ugly hack.

[Johan Commelin]

And without notation, you have all those .obj and op floating around.

[Scott Morrison]

Why not just leave out the ,s? You could just define 𝓔𝓧𝓣 or something?

[Johan Commelin]

@Scott Morrison you mean as an abbreviation?

[Johan Commelin]

Also, that looks very much like an internal Ext object, with all those curly letters.

[Scott Morrison]

True. It would be better to just write Ext.

[Johan Commelin]

Ordinary notation cannot deal with multiple variables in a row, right? So notation would need some form of delimiters.

[Scott Morrison]

Why not just a def? You might even work out how to keep the usual Ext out of scope.

[Scott Morrison]

I was going to have a look, but haven't compiled liquid oleans in some time. :-)

[Johan Commelin]

Like this?

abbreviation Ext (i : ℕ) (AB : Condensed Ab × Condensed Ab) :=
((Ext ℤ (Condensed Ab) i).obj (op AB.1)).obj AB.2

theorem main_challenge (i : ℕ) (hi : 0 < i) :
  is_zero (Ext i ((ℳ p').obj S, Condensed.of_top_ab V)) :=
sorry

[Johan Commelin]

I think that is certainly an improvement (notationwise).

[Johan Commelin]

I pushed this to master

[Johan Commelin]

Scott Morrison said:

I was going to have a look, but haven't compiled liquid oleans in some time. :-)

./scripts/get-cache.sh

[Scott Morrison]

Ah, I was running leanproject get-cache, with no success.

[Scott Morrison]

Why did you make your abbreviation take a pair? Just to make it look slightly more like normal notation? That seems to be overdoing it. :-)

[Scott Morrison]

Next you're going to be introducing notation = 0 for is_zero. :-)

[Scott Morrison]

I guess it's not insane. Use some strange canadian syllabics unicode equality.

[Johan Commelin]

Yeah, maybe it is overdoing it

[Johan Commelin]

Probably, getting rid of the Condensed.of_top_ab is more important.

[Scott Morrison]

Actually, why do you use is_zero? What's wrong with ≅ 0?

[Johan Commelin]

@Scott Morrison That contains data, right? So you need to write a nonempty.

[Scott Morrison]

What would be wrong with data here?

[Johan Commelin]

Also, with all those exact sequences, you want a smooth API for showing that objects are trivial. I'm not sure if ≅ 0 is "agile" enough for that.

[Johan Commelin]

Scott Morrison said:

What would be wrong with data here?

It's a theorem. But maybe we can ignore that, and define data anyway. The linter will complain (-;

[Scott Morrison]

Sure -- in the proofs. But for now you're just trying to write a readable statement.

[Scott Morrison]

I think the for_twitter/ files are allowed to make the linter unhappy.

[Johan Commelin]

So, def or @[nolint] theorem?

[Johan Commelin]

abbreviation Ext (i : ℕ) (A B : Condensed Ab) :=
((Ext ℤ (Condensed Ab) i).obj (op A)).obj B

variables (S : Profinite.{1})
variables (V : Type 1) [normed_group V] [module ℝ V] [normed_space' ℝ p V] -- `V` is a `p`-Banach

theorem main_challenge (i : ℕ) (hi : 0 < i) :
  Ext i ((ℳ p').obj S) (Condensed.of_top_ab V) ≅ 0 :=
sorry

[Johan Commelin]

I guess we could try to get (V : Condensed_Banach' p)?

[Scott Morrison]

structure pBanach :=
(V : Type 1)
(normed_group : normed_group V)
(module : module ℝ V)
(normed_space' : normed_space' ℝ p V)

instance : has_coe_to_sort (pBanach p) :=
{ S := Type 1,
  coe := λ X, X.V }

instance (X : pBanach p) : normed_group X := X.normed_group
instance (X : pBanach p) : module ℝ X := X.module
instance (X : pBanach p) : normed_space' ℝ p X := X.normed_space'

instance : has_coe (pBanach p) (Condensed Ab) :=
{ coe := λ V, Condensed.of_top_ab V }

variables (S : Profinite.{1})
variables (V : pBanach p)

theorem main_challenge (i : ℕ) (hi : 0 < i) :
  Ext i ((ℳ p').obj S) V ≅ 0 :=
sorry

[Johan Commelin]

Please push that (-;

[Johan Commelin]

I guess we can get rid of the final .obj as well, by making ℳ an abbreviation?

[Scott Morrison]

Okay, I pushed. pBanach should go in a different file, however.

[Scott Morrison]

ℳ isn't a valid identifier.

[Scott Morrison]

You could however write Ext i (ℳ_{p'} S) V ≅ 0 using notations

[Johan Commelin]

That looks good!

[Johan Commelin]

I suggest that we go for that!

[Scott Morrison]

Pushed.

[Johan Commelin]

Pulled.

[Scott Morrison]

I did another commit that tidies things up by adding a challenge_notations.lean file.

[Scott Morrison]

Only really useful for making challenge.lean audience friendly. Feel free to revert.

[Johan Commelin]

Scott Morrison said:

I did another commit that tidies things up by adding a challenge_notations.lean file.

Forgot to git add

[Scott Morrison]

Got it.

[Scott Morrison]

I am congenitally incapable of using git add.

[Johan Commelin]

For those of you who aren't pulling every 5 minutes. The non-commenty part of the file now looks like

open_locale nnreal liquid_tensor_experiment

namespace liquid_tensor_experiment

variables (p' p : ℝ≥0) [fact (0 < p')] [fact (p' ≤ 1)] [fact (p' < p)] [fact (p ≤ 1)]

variables (S : Profinite.{1})
variables (V : pBanach p)

theorem main_challenge (i : ℕ) (hi : 0 < i) :
  Ext i (ℳ_{p'} S) V ≅ 0 :=
sorry

end liquid_tensor_experiment

[Johan Commelin]

I propose 1 more tweak:

open_locale nnreal liquid_tensor_experiment
open liquid_tensor_experiment

variables (p' p : ℝ≥0) [fact (0 < p')] [fact (p' ≤ 1)] [fact (p' < p)] [fact (p ≤ 1)]
variables (S : Profinite.{1}) (V : pBanach p)

theorem liquid_tensor_experiment (i : ℕ) (hi : 0 < i) :
  Ext i (ℳ_{p'} S) V ≅ 0 :=
sorry

[Scott Morrison]

Actually, you can make the open_locale do the open, as well.

[Scott Morrison]

Saves another line!

[Scott Morrison]

And I guess if you want to break the fact rule you could make an instance for [fact (p' ≤ 1)], deriving it from the others.

[Sebastien Gouezel]

Is there a reason why your statement is not universe polymorphic?

[Johan Commelin]

The universes are a mess.

[Johan Commelin]

And this might actually Lean-bite us :scream:

[Johan Commelin]

After all, we want to reduce the main challenge to

theorem first_target :
  ∀ m : ℕ, ∃ (k K : ℝ≥0) (hk : fact (1 ≤ k)) (c₀ : ℝ≥0),
  ∀ (S : Type) [fintype S] (V : SemiNormedGroup.{0}) [normed_with_aut r V],
    ​((BD.data.system κ r V r').obj (op $ of r' (Mbar r' S))).is_weak_bounded_exact k K m c₀ :=

[Johan Commelin]

which lives in Type = Type 0.

[Johan Commelin]

And the main challenge is stated in terms of stuff in Type 1

[Johan Commelin]

Both "for technical reasons".

[Johan Commelin]

I'm going to have lunch first.

[Johan Commelin]

The problem is that first_target specializes to the polyhedral lattice ℤ : Type. And all the universe variables in the statement of thm95 have to be the same.

[Johan Commelin]

So I guess we want to make ulift ℤ into a polyhedral lattice.

[Johan Commelin]

But S and V will still need to live in the same universe.

[Johan Commelin]

Decoupling those can be done, but will be an interesting journey.

[Sebastien Gouezel]

Starting with Type 0 first looks reasonable.

[Johan Commelin]

So the main statement lives in universe u+1 because of technical complications with making Profinite a small category. Getting rid of this, probably means that we have to inject all the κ-bounds from the first part of Condensed.pdf into lean.

[Johan Commelin]

(Where κ is some uncountable strong limit cardinal.)

[Adam Topaz]

I might be confused (as usual) about universes... why is S : Profinite.{1} and not S : Profinite.{0}?

[Johan Commelin]

Je ne sais pas :shrug: universes never fail to give me headaches.

[Adam Topaz]

I mean, we should be worrking in Condensed Ab.{1}, which are sheaves on as_small.{1} Profinite.{0}, right?

[Johan Commelin]

I guess so...

[Adam Topaz]

Is

theorem liquid_tensor_experiment (S : Profinite) (V : pBanach p) (i : ℕ) (hi : 0 < i) :
  Ext i (ℳ_{p'} S) V ≅ 0 :=
sorry

supposed to work? I'm getting an error at Ext.

[Johan Commelin]

I think you need to provide the universe variable for S, right?

[Johan Commelin]

Hmm, you are right, it's not working properly

[Adam Topaz]

I think there is a universe issue with real_measures.functorr

[Johan Commelin]

Hmmz, is it easily fixable?

[Johan Commelin]

I have something that typechecks...

[Johan Commelin]

no clue whether it makes universe-sense though.

[Johan Commelin]

I pushed it. It's (S : Profinite.{1}) (V : pBanach.{1} p)

[Adam Topaz]

I'm a little concerned....

[Peter Scholze]

Me too, actually. You definitely want the profinite set $S$ to live in the site defining condensed sets. A priori you might defined condensed sets using some universe of profinite sets, and then define the functor $\mathcal M_{p'}$ on some larger class of profinite sets, but then the theorem wouldn't be true for those larger profinite sets.

[Peter Scholze]

(Otherwise, the theorem statement looks very nice now :-)!)

[Peter Scholze]

Even worse, I think you will have to arrange that the profinite sets $\mathcal{M}(S,\mathbb Z((T))_r)_{\leq c}$ live in the site defining condensed sets. So be careful with your universes!

[Peter Scholze]

(Well, I can't really believe that when you try to glue stuff together you will get unresolvable universe issues. But it may not be a completely trivial task. And it is likely that the current version of the theorem is not true.)

[Adam Topaz]

I think the key thing that needs to be changed is
to_Condensed : CompHausFiltPseuNormGrp₁.{u+1} ⥤ Condensed.{u} Ab.{u+1} should instead be to_Condensed : CompHausFiltPseuNormGrp₁.{u} ⥤ Condensed.{u} Ab.{u+1}

[Adam Topaz]

Well, and we will need to have a functor pBanach.{0} p to Condensed Ab.{1}.

[Adam Topaz]

Do we have a ulift-like functor from Ab.{u} to Ab.{max u v}?

[Johan Commelin]

Nope, I don't think such a ulift-like functor exists.