9.5 => 9.4 pain

Stream: condensed mathematics

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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]

---

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

[Johan Commelin]

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

[Peter Scholze]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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