Zulip Chat Archive

Stream: condensed mathematics

Topic: universe strikes back


Johan Commelin (May 19 2022 at 13:01):

It turns out that we want to apply thm95.profinite to

  • Λ=Z\Lambda = \mathbb{Z} (which lives in Type 0
  • Lˉr(S)\bar{\mathcal{L}}_{r'}(S), where SS is a profinite set in Type 1 (or Type u)
  • VV a pp-Banach in Type 2 (or Type u+1).

So we really need maximal universe polymorphism :octopus:

Adam Topaz (May 19 2022 at 13:02):

Where does S : Profinite.{1} come from? That seems suspicious

Johan Commelin (May 19 2022 at 13:03):

See challenge.lean. My VScode is frozen.

Adam Topaz (May 19 2022 at 13:20):

I'm trying to look... but I'm waiting on lean to build... as usual...

Adam Topaz (May 19 2022 at 13:21):

looks like laurent_measures/ext has a build error..

Johan Commelin (May 19 2022 at 13:22):

Yes, it's related. I'm working on a fix.

Johan Commelin (May 19 2022 at 13:23):

Might be easier to git checkout @^5 and fetch oleans there.

Adam Topaz (May 19 2022 at 13:23):

Okay. I'm playing with the universes now.

Adam Topaz (May 19 2022 at 13:24):

theorem liquid_tensor_experiment (S : Profinite.{0}) (V : pBanach.{0} p) :
   i > 0, Ext i (ℳ_{p'} S) V  0 :=

Adam Topaz (May 19 2022 at 13:24):

Lean seems to be happy with that. Shall I push?

Johan Commelin (May 19 2022 at 13:25):

Does the whole project build?

Adam Topaz (May 19 2022 at 13:25):

I'll try.

Adam Topaz (May 19 2022 at 13:26):

yes, it builds, except forr the error I mentioned above.

Johan Commelin (May 19 2022 at 13:26):

Can you fix those by changing some u to 0?

Adam Topaz (May 19 2022 at 13:30):

1 moment

Adam Topaz (May 19 2022 at 13:30):

the file is fixed, but I'll try to build the whole project again

Adam Topaz (May 19 2022 at 13:30):

okay it all builds

Johan Commelin (May 19 2022 at 13:30):

cool!

Johan Commelin (May 19 2022 at 13:30):

I don't know where that 1 came from...

Adam Topaz (May 19 2022 at 13:31):

Is 0 required here?

/-- Thm 9.4bis of [Analytic]. More precisely: the first observation in the proof 9.4 => 9.1. -/
theorem is_iso_Tinv2 [normed_with_aut r V]
  (hV :  (v : V), (normed_with_aut.T.inv v) = 2  v) :
   i, is_iso (((Ext' i).map ((condensify_Tinv2 (Fintype_Lbar.{0 0} r')).app S).op).app
    (Condensed.of_top_ab V)) :=

Johan Commelin (May 19 2022 at 13:31):

Maybe from a long time ago, when we still got some universes wrong in Condensed?

Johan Commelin (May 19 2022 at 13:31):

We only prove first_target in universe 0.

Adam Topaz (May 19 2022 at 13:31):

laurent_measures/ext could have been univeerse polymorphic if it wasn't for those 0s

Johan Commelin (May 19 2022 at 13:32):

Because Λ=Z\Lambda = \mathbb{Z} lives in universe 0 and it must be the same as the universe of S. Unless we do a huge refactor.

Johan Commelin (May 19 2022 at 13:32):

Or we take ulift \Z and show it is a polyhedral lattice with Hom(Lambda, M) = M.

Johan Commelin (May 19 2022 at 13:33):

But I'm happy with the 0s. Certainly for now.

Johan Commelin (May 19 2022 at 13:33):

@Adam Topaz did you push your fixes?

Adam Topaz (May 19 2022 at 13:34):

pushed now


Last updated: Dec 20 2023 at 11:08 UTC