Zulip Chat Archive

Stream: condensed mathematics

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


view this post on Zulip 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.

view this post on Zulip Peter Scholze (Mar 15 2021 at 16:22):

Yes

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:22):

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

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:22):

But this affects the constants, doesn't it?

view this post on Zulip Peter Scholze (Mar 15 2021 at 16:23):

Of course it does, but in a controllable way

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:23):

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

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:24):

Which version do you prefer?

view this post on Zulip Peter Scholze (Mar 15 2021 at 16:25):

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

view this post on Zulip 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

view this post on Zulip Peter Scholze (Mar 15 2021 at 16:25):

or rescale the cic_i's, sorry

view this post on Zulip Peter Scholze (Mar 15 2021 at 16:26):

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

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:26):

Right, and compose the maps with restriction maps

view this post on Zulip Peter Scholze (Mar 15 2021 at 16:26):

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

view this post on Zulip 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?

view this post on Zulip Peter Scholze (Mar 15 2021 at 16:27):

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

view this post on Zulip Peter Scholze (Mar 15 2021 at 16:27):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:30):

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

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:32):

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

view this post on Zulip 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'

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:34):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Peter Scholze (Mar 15 2021 at 16:37):

I don't think we need this inequality here

view this post on Zulip Peter Scholze (Mar 15 2021 at 16:38):

Only r<1r<1 or something like that

view this post on Zulip 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! :-)

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:38):

Ooh, yes, I forgot the footnote for a moment

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:40):

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

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:40):

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

view this post on Zulip Peter Scholze (Mar 15 2021 at 16:41):

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

view this post on Zulip Peter Scholze (Mar 15 2021 at 16:41):

(Also time to go home here.)


Last updated: May 09 2021 at 21:10 UTC