Zulip Chat Archive

Stream: condensed mathematics

Topic: 9.5 => 9.4 pain


view this post on Zulip Johan Commelin (Mar 10 2021 at 11:13):

The sorry in liquid.lean is currently not provable, I think :sad:
In the definition of the system of complexes associated with Mbar r' S (or any M), we take equalizers in a final step. These equalizers are taken in the category NormedGroup with bounded homomorphisms.

Key point: I don't think that we can prove that the inclusion from the equalizer of f ⁣:VWf \colon V \to W into VV is an isometry. The only tool we have is the universal property of equalizers.

For the proof 9.5 => 9.4 we want to use that Hom(Z,M)\mathrm{Hom}(\Z, M) is isomorpic to MM, and hence they have isomorphic complexes. But the isomorphism between those complexes does not have to be by isometries. I thought we could easily prove that it would be isometries, but you can now see why we are stuck.

view this post on Zulip Johan Commelin (Mar 10 2021 at 11:14):

So, either we refactor everything, or we get weird constants in 9.4 that are not the same as the constants in 9.5.

view this post on Zulip Kevin Buzzard (Mar 10 2021 at 11:17):

If you want to keep track of precise norms then you could use morphisms which are norm-nonincreasing rather than bounded

view this post on Zulip Johan Commelin (Mar 10 2021 at 12:01):

Yes, but we need some morphisms that increase the norm. So we need to do something slightly smarter.

view this post on Zulip Johan Commelin (Mar 10 2021 at 12:01):

I think that the easiest way out is to just use an explicit construction of the equalizer, instead of the category_theory machine.

view this post on Zulip Johan Commelin (Mar 10 2021 at 12:21):

Hmm, I need to think carefully about my claim that we need morphisms that increase the norm. That might be based on an old idea of using NormedGroup for stuff that is now all dealt with by profinitely_filtered_pseudo_normed_group.

view this post on Zulip Johan Commelin (Mar 10 2021 at 12:23):

Otoh, with norm-nonincreasing maps, we no longer have a preadditive category

view this post on Zulip Johan Commelin (Mar 10 2021 at 12:23):

Which might be annoying for some of the homological algebra that we want to do later

view this post on Zulip Johan Commelin (Mar 10 2021 at 13:17):

I confirmed that there are quite a number of morphisms that are potentially norm-increasing.

view this post on Zulip Johan Commelin (Mar 10 2021 at 13:18):

In particular, we haven't yet implemented the step just above 9.6, which explains how to make BD.system (Mbar r' S) into an admissible system. Our current definition is not admissible.

view this post on Zulip Johan Commelin (Mar 10 2021 at 13:19):

And I think we want to maintain the flexibility to talk about norm-increasing homs during the construction.

view this post on Zulip Johan Commelin (Mar 10 2021 at 13:25):

Johan Commelin said:

In particular, we haven't yet implemented the step just above 9.6, which explains how to make BD.system (Mbar r' S) into an admissible system. Our current definition is not admissible.

Note that this is not a mathematical issue, we can reduce to the admissible case. I claim that thm95 is provable as stated.
There is a reduction to the admissible case. But we need to implement that reduction step.

view this post on Zulip Johan Commelin (Mar 10 2021 at 15:19):


The pain has been fixed. I've made the equalizers explicit, and show that a whole bunch of maps are norm-noninc

view this post on Zulip Johan Commelin (Mar 10 2021 at 15:20):

So the file liquid.lean no longer contains a sorry.

view this post on Zulip Peter Scholze (Mar 10 2021 at 20:20):

Congratulations on the progress! Were there norm-increasing maps in the end? I would have expected that the two complexes should really be the same, with the same norms.

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:23):

@Peter Scholze I needed to make an actual change, but there was no math content

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:24):

If you take an equalizer EVWE \subset V \stackrel{\to}{\to} W in NormedGroup then there is no reason why the inclusion EVE \subset V is norm-preserving.

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:25):

Ok, I should qualify that: if you take an equalizer in the sense of abstract category theory.

view this post on Zulip Johan Commelin (Mar 10 2021 at 20:25):

So I ended up defining NormedGroup.equalizer which does the obvious thing, and fixes this problem.


Last updated: May 09 2021 at 16:20 UTC