universe strikes back

Stream: condensed mathematics

[Johan Commelin]

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

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

So we really need maximal universe polymorphism :octopus:

[Adam Topaz]

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

[Johan Commelin]

See challenge.lean. My VScode is frozen.

[Adam Topaz]

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

[Adam Topaz]

looks like laurent_measures/ext has a build error..

[Johan Commelin]

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

[Johan Commelin]

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

[Adam Topaz]

Okay. I'm playing with the universes now.

[Adam Topaz]

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

[Adam Topaz]

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

[Johan Commelin]

Does the whole project build?

[Adam Topaz]

I'll try.

[Adam Topaz]

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

[Johan Commelin]

Can you fix those by changing some u to 0?

[Adam Topaz]

1 moment

[Adam Topaz]

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

[Adam Topaz]

okay it all builds

[Johan Commelin]

cool!

[Johan Commelin]

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

[Adam Topaz]

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]

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

[Johan Commelin]

We only prove first_target in universe 0.

[Adam Topaz]

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

[Johan Commelin]

Because $\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]

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

[Johan Commelin]

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

[Johan Commelin]

@Adam Topaz did you push your fixes?

[Adam Topaz]

pushed now