r<1

Stream: condensed mathematics

[Kevin Buzzard]

This is hopefully an easy one. Right now in invpoly.basic we have instance : fintype { F : ℤ[T⁻¹] S | ∥F∥₊ ≤ c} := sorry and this sorry is I think false in general if r>=1. If I insert an r<1 hypothesis then various later theorems in the file break because they don't have it but rely on finiteness for a compactness assertion. I've pushed a fix to the is_r_lt_one_assumption branch but didn't want to push to master immediately in case we need some of these results more generally. Can someone take a look over it and/or merge the branch to master? Here's the diff.

[Johan Commelin]

@Kevin Buzzard Assuming < 1 is fine. This will always be satisfied in the final application.

[Johan Commelin]

I pushed a commit fixing up another file

[Kevin Buzzard]

Hmm. Now src/Lbar/ses.lean is broken, and this was code which worked before.

def to_laurent_measures_nat_trans [fact (r' < 1)] :
  invpoly.fintype_functor r' ⟶ laurent_measures.fintype_functor r' :=
{ app := λ S, to_laurent_measures_hom r' S,
...

->

type mismatch at field 'app'
  λ (S : Fintype), to_laurent_measures_hom r' S
has type
  Π (S : Fintype), comphaus_filtered_pseudo_normed_group_with_Tinv_hom r' (invpoly r' S) (laurent_measures r' S)
but is expected to have type
  Π (X : Fintype), (fintype_functor r').obj X ⟶ (laurent_measures.fintype_functor r').obj X

Can you work out what's going on from this?

[Johan Commelin]

That's werid... those look like they should be defeq

[Adam Topaz]

Isn't this supposed to be a strict morphism?

[Adam Topaz]

Oh, nevermind, the homs with Tinv are already strict

[Kevin Buzzard]

They were defeq, things still compile fine on master. I've just pushed some simple boundedness results, enough to make the fintype instance easy now, but I'm reluctant to start on it if it's going to cause breakages I can't fix :-)

[Kevin Buzzard]

I'm going to take a short break and then come back to it. I have (extremely mild) Covid BTW so I have to stay at home today :D

[Kevin Buzzard]

Ok so it was my own error; I hadn't pulled Johan's changes. I think I'm back on track.

[Kevin Buzzard]

OK so both master and this is_r_lt_one_assumption_OK branch are compiling; the diff is here; I have added several r<1 assumptions which weren't there before and I am not confident enough to say whether this is OK. If someone wants to give me the goahead then I can merge this to master; in the mean time I'll prove the finiteness result under the r<1 assumption.

[Johan Commelin]

@Kevin Buzzard feel free to merge it into master now that it compiles

[Kevin Buzzard]

OK -- finiteness is now done for r<1 and invpoly.basic is sorry-free! I'll look for another project now.