README

Stream: condensed mathematics

[Johan Commelin]

It was high time to update the README. I might still have missed stuff that is out of date. Please review the README and https://github.com/leanprover-community/lean-liquid/pull/119

[Johan Commelin]

This is now ready for review.

[Adam Topaz]

Looking at it now!

[Adam Topaz]

I left a few minor comments.

[Johan Commelin]

Thanks

[Adam Topaz]

Hmmm.... one question: Should we really claim that

variables (p' p : ℝ≥0) [fact (0 < p')] [fact (p' < p)] [fact (p ≤ 1)]
theorem liquid_tensor_experiment (S : Profinite.{0}) (V : pBanach.{0} p) :
  ∀ i > 0, Ext i (ℳ_{p'} S) V ≅ 0 :=

is Theorem 9.1 from Analytic.pdf?

[Adam Topaz]

The precise statement of Theorem 9.1 is that $RHom(M(S,\mathbb{Z}((t))_{r'}),\hat V) = \hat V (S)$.

[Adam Topaz]

Of course, the precise statement we formalized is Theorem 1.1 of Peter's challenge.

[Johan Commelin]

Good point. So let's claim that instead.

[Adam Topaz]

Fortunately, this is already correct:
https://github.com/leanprover-community/lean-liquid/blob/25dc13f472934009786afaaaa2392fa2c8d73e3c/src/challenge.lean#L13

[Johan Commelin]

I pushed another commit fixing that bit in the readme.

[Adam Topaz]

Thanks! I approved + enabled auto-merge