# Zulip Chat Archive

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