## Stream: condensed mathematics

### Topic: 9.5 => 9.4 pain

#### 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 \colon V \to W$ into $V$ 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 $\mathrm{Hom}(\Z, M)$ is isomorpic to $M$, 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.

#### 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.

#### 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

#### 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.

#### 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.

#### 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.

#### Johan Commelin (Mar 10 2021 at 12:23):

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

#### Johan Commelin (Mar 10 2021 at 12:23):

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

#### Johan Commelin (Mar 10 2021 at 13:17):

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

#### 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.

#### 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.

#### 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.

#### 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

#### Johan Commelin (Mar 10 2021 at 15:20):

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

#### 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.

#### Johan Commelin (Mar 10 2021 at 20:23):

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

#### Johan Commelin (Mar 10 2021 at 20:24):

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

#### 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.

#### 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