universal map refactor

Stream: condensed mathematics

[Johan Commelin]

In the Breen-Deligne section of LTE we are using free_abelian_group. But we might want to switch to finsupp, because will allow us to reuse constructions that Scott has been adding to mathlib. However, when I tried that this afternoon, I got really weird behaviour with the equation compiler. It probably has something to do with free_abelian_group being computable, whereas finsupp is not.

I pushed to the BD-refactor branch. If you want to take a look, the error shows up around
src/breen_deligne/category.lean:182
where I need to dsimp in a definition.

[Adam Topaz]

I'll try to look at this later today, if it's still an issue

[Adam Topaz]

@Johan Commelin do I understand correctly that the main change from free_abelian_group to finsupp happened in the definition of $\mathbb{Z}[A]$?

[Johan Commelin]

Right, and now the rest of the project needs to adept to that change

[Johan Commelin]

But if it is too much work... I wouldn't worry too much.

[Johan Commelin]

Scott's code isn't all in mathlib yet. So it isn't urgent.

[Adam Topaz]

Gotcha. I have a bit of time now so I wanted to get my bearings straight. I'll play more with this branch later

[Adam Topaz]

Ooof... this proof in hom_pow'_sum is really annoying... I can't make progress at all! Even replacing the first dsimp [...] with

change ((BD.mul_mul_iso 2 (2 ^ N)).inv ≫ (mul 2).map (BD.pow'_iso_mul N).inv) ≫
    (mul 2).map (hom_pow' (BD.sum 2) N) ≫ BD.sum 2 = BD.sum (2 ^ (N + 1)),

(which is what it should be) gives me a timeout.

[Adam Topaz]

Okay, I made some progress. The trick seems to be to avoid using the equation compiler and use nat.rec_on manually.
I pushed my code to the branch BD-refactor-2.

[Adam Topaz]

So far I got breen_deligne/category.lean to compile, but I haven't worked on any of the other files

[Johan Commelin]

@Adam Topaz ooh, thanks for the progress!

[Johan Commelin]

Still, I'm quite surprised that switching from free_abelian_group to finsupp causes this sort of problems.
@Mario Carneiro Are you interested/do you have time to take a look at what's going on? I don't understand this weird behaviour.