Zulip Chat Archive

Stream: condensed mathematics

Topic: The system of Mbar r' S is not (yet) admissible

Johan Commelin (Mar 15 2021 at 16:21):

@Peter Scholze Here is another thing I'm confused about. At the top of page 60 you explain how to to make the system associated to Mbar r' S admissible. But I think at some point you said that for theorem 9.5 it doesn't actually matter.

Peter Scholze (Mar 15 2021 at 16:22):

Yes

Johan Commelin (Mar 15 2021 at 16:22):

By taking some suitable restrictions, we can still prove the current statement.

Johan Commelin (Mar 15 2021 at 16:22):

But this affects the constants, doesn't it?

Peter Scholze (Mar 15 2021 at 16:23):

Of course it does, but in a controllable way

Johan Commelin (Mar 15 2021 at 16:23):

So it's a tradeoff between the c_i and the k and K

Johan Commelin (Mar 15 2021 at 16:24):

Which version do you prefer?

Peter Scholze (Mar 15 2021 at 16:25):

Hmm, I'm not exactly sure what the question is...

Peter Scholze (Mar 15 2021 at 16:25):

I think 9.6 needs admissibility, so you want to rescale all maps to make them admissible

Peter Scholze (Mar 15 2021 at 16:25):

or rescale the $c_i$ 's, sorry

Peter Scholze (Mar 15 2021 at 16:26):

Ah, so is the question that of rescaling $c_i$ vs rescaling the maps?

Johan Commelin (Mar 15 2021 at 16:26):

Right, and compose the maps with restriction maps

Peter Scholze (Mar 15 2021 at 16:26):

OK, so in the manuscript I rescaled $c_i$ (and implicitly composed with restriction maps)

Johan Commelin (Mar 15 2021 at 16:27):

Well, I think the question is, for which system would you want us to compute the constants? For the one with rescaled c_i or for the "original" system. Or maybe both?

Peter Scholze (Mar 15 2021 at 16:27):

OK, that's hard to say, I think both solutions should be essentially equivalent

Peter Scholze (Mar 15 2021 at 16:27):

I'd say it's easier to rescale the $c_i$ because then one can use variables that are already around

Johan Commelin (Mar 15 2021 at 16:29):

I wonder whether we should axiomatize 9.8, and prove 9.5 for all M that satisfy 9.8.

Johan Commelin (Mar 15 2021 at 16:30):

Hmm, but that's orthogonal to how we construct the system, so ignore that remark

Johan Commelin (Mar 15 2021 at 16:32):

So, we have these 3 definitions: https://leanprover-community.github.io/liquid/index.html#basic_suitable

Johan Commelin (Mar 15 2021 at 16:32):

And I think we can add one on top, saying that a sequence of c_is is very_suitable, which depends on Breen--Deligne data + r and r'

Johan Commelin (Mar 15 2021 at 16:33):

and then, for very_suitable c_i, we can show that the current definition BD.system spits out an admissible system.

Johan Commelin (Mar 15 2021 at 16:34):

The alternative would be to refactor BD.system and rescale the maps...

Johan Commelin (Mar 15 2021 at 16:34):

But I'm not sure that it's easy to abstract over those two approaches, and prove 9.5 for both of them at once

Johan Commelin (Mar 15 2021 at 16:37):

For this rescaling of the c_i we use the assumption r < r', right? Is this used in any other place? It seems to me that the "rescale the maps approach" wouldn't need that assumption.

Peter Scholze (Mar 15 2021 at 16:37):

I don't think we need this inequality here

Peter Scholze (Mar 15 2021 at 16:38):

Only $r<1$ or something like that

Peter Scholze (Mar 15 2021 at 16:38):

The place where it's really used is at the end of the proof of 9.5, there's even a footnote for it! :-)

Johan Commelin (Mar 15 2021 at 16:38):

Ooh, yes, I forgot the footnote for a moment

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

But for the rescaling the c_i approach, you need to know that $[T] \circ(T^{-1})^{*}$ is norm-nonincreasing, right?

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

(Dinner time.... see you later.)

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

I don't think so, I only need that restriction from $M_{\leq c}$ to $M_{\leq r'c}$ decreases the norm by a factor of $r$ .

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

(Also time to go home here.)

Last updated: Dec 20 2023 at 11:08 UTC