pow rescale pow

Stream: condensed mathematics

[Johan Commelin]

Here's a pretty self-contained sorry that is needed for col_exact:

-- the contents of `src/thm95/pfpng_iso.lean`
namespace ProFiltPseuNormGrpWithTinv

variables (r' : ℝ≥0) [fact (0 < r')]
variables (c : ℝ≥0) (m n : ℕ)
variables (M : ProFiltPseuNormGrpWithTinv r')

local notation `ρ` := _root_.rescale

/-
Useful facts that we already have:

* `Pow_mul (N n : ℕ) : Pow r' (N * n) ≅ Pow r' N ⋙ Pow r' n`
* `iso_of_equiv_of_strict'` for constructing isos in `ProFiltPseuNormGrpWithTinv r'`
-/

/-- A very specific isomorphism -/
def Pow_rescale_Pow_iso :
  Pow r' m ⋙ rescale r' c ⋙ Pow r' n ≅ Pow r' n ⋙ Pow r' m ⋙ rescale r' c :=
sorry

end ProFiltPseuNormGrpWithTinv

I guess this would naturally break into two subparts: show that Pow commutes with itself, and show that Pow commutes with rescale`.

[Johan Commelin]

Note that for Pow r' (m * n) \iso Pow r' (n * m) we should not cheat and use m * n = n * m directly because that gives the wrong automorphism of fin (m * n). We should use whatever rolls out of fin (m * n) = fin m \times fin n = fin n \times fin m = fin (n * m) using the equivs in mathlib equiv.prod_comm and equiv.fin_prod_fin

[Johan Commelin]

We're getting really close:

3       src/prop819.lean
1       src/thm95/pfpng_iso.lean
3       src/thm95/col_exact.lean
Total:  7

[Johan Commelin]

Is there anyone interested in attacking the natural isomorphism posted in this thread?

[Scott Morrison]

Sure?

[Scott Morrison]

I don't know any of the definitions, but I can make some time this afternoon.

[Scott Morrison]

Started on it: turned 1 sorry into 10, now have to run for an hour.

[Scott Morrison]

Hopefully finish up then.

[Johan Commelin]

Great!

[Scott Morrison]

I got it back down to 3 sorries, two of which are the continuity arguments of iso_of_equiv_of_strict', and I don't really know what to do with these. The other one perhaps works by refl, but is very slow. Perhaps some simp lemmas are missing...

[Scott Morrison]

I've pushed, and will pause on this for a while if anyone wants to have a look.

[Scott Morrison]

(It's all in src/thm95/pfpng_iso.lean.)

[Riccardo Brasca]

I am having a look at the third one

[Riccardo Brasca]

refl indeed works... after a long time. Let me see if I can speed it up

[Peter Scholze]

lol

[Peter Scholze]

I find it amusing that you can tell a computer "these things are literally the same" and then it sits there for an hour until it says "ah yes, they are"

[David Michael Roberts]

I guess the same thing happens with students just starting out...

[Peter Scholze]

It also happens to professors!

[Riccardo Brasca]

I was also surprised the first time I saw it, but sometimes it is a problem. We don't want the computer to unfold everything to the axioms... so we tell him to not unfold certain definitions

[Kevin Buzzard]

Scott had some category theory proofs which were refl and which took a long time, and he greatly sped them up by changing them to "rewrite" proofs, where you explicitly feed proofs of A=B, B=C, C=D, ... in the right order to the computer. Some of the underlying terms which only the computer sees can be very very large, it is quite ridiculous. Working on the perfectoid project taught me this -- at times stuff would get slow, and when the CS people looked at what we were doing they were kind of horrified at how complex our objects were, and gave us tips on how to tame them.

[Riccardo Brasca]

BTW, here is what set_option trace.type_context.is_def_eq_detail true says

https://webusers.imj-prg.fr/~riccardo.brasca/files/refl

[Kevin Buzzard]

The unicode characters are mangled for me. You have an account on github so you could post a gist.

[Riccardo Brasca]

Surprisingly removing dsimp and using directly refl works and it's very fast :thinking:

[Riccardo Brasca]

Note that the project doesn't compile anymore (since 4f9fb104d97b89793492dfc2f85a11467a2ce4c7)...

[Johan Commelin]

Yeah, something in col_exact broke due to changes in pfpng_iso

[Johan Commelin]

I'm ignoring it for now (-;

[Johan Commelin]

"It came on it's own, it'll go on it's own"

[Johan Commelin]

It didn't go away... so I fixed it. Had to specify the universe params. Not so bad :sweat_smile: