Universe question in Module.equiv_directSum_of_isTorsion

Stream: mathlib4

[Jz Pan]

The docs#Module.equiv_directSum_of_isTorsion is the structure theorem of finitely generated torsion module N over PID R. The R is at universe level u, but the N is at universe level max u v which seems strange to me. Doesn't it work if N is only at universe level v? Any reason behind it?

[Jz Pan]

Seems that docs#lequivProdOfRightSplitExact is faulty as it is of same-universe. Its construction relies on category theory so it can only be same-universe version. It also doesn't have apply simps lemmas. Personally I think we shouldn't depend on category theory on such simple results, the one is that we can have universe polymorphic versions for them, and we can have apply simps lemmas for them.

[Jz Pan]

Now I'm trying to decipher https://github.com/leanprover-community/mathlib4/blob/99dfc6ca1575c39bc68769e61409965d8b9ac3f1/Mathlib/Algebra/Module/PID.lean#L198-L209 ...

[Jz Pan]

OK I think I have a cheap solution: if N : Type v then its lifting to Type max u v satisfies the condition of the original result, but this lifting is isomorphic so we are done. :joy:

[Jz Pan]

PR created as #24403.

[Kevin Buzzard]

Conversely if N is f.g. over R then N is isomorphic to a quotient of R^n so there is something isomorphic to N in R's universe u, namely R^n / (kernel of the surjection)

[Kevin Buzzard]

I will make the bold statement that for FLT all this use of universes is just noise and we could get away with doing all algebra in universe 0, although it will still be helpful to have multi-universe category theory because sometimes you go up to a higher universe and then use tricks like the ones we're using to go back to universe 0

[Jz Pan]

Kevin Buzzard said:

Conversely if N is f.g. over R then N is isomorphic to a quotient of R^n so there is something isomorphic to N in R's universe u, namely R^n / (kernel of the surjection)

Yes we have this result docs#Module.Finite.small

I will make the bold statement that for FLT all this use of universes is just noise and we could get away with doing all algebra in universe 0

I think you need universe 1 if you want to talk about Grothendieck group (K, K_0, K_1 etc) of some abelian category over universe 0. But it is (canonically?) isomorphic to some object in universe 0, so it's still OK.

[Kevin Buzzard]

Right -- I think it's important to allow higher universes in category theory, and have theorems saying things like "you computed the etale cohomology of projective n-space by taking a large limit which means that it has great functoriality properties but it's in Type 1, fortunately here's a theorem which says that there's a group in Type 0 which it's isomorphic to and hopefully the diagrams commute". But away from category theory I wonder whether we need any types other than Type 0 to do, say, 90% of the remainder of mathlib.

[Eric Wieser]

I found a nicer solution that doesn't require modifying equiv_directSum_of_isTorsion at all, #24419

[Eric Wieser]

Though this all seems a bit fishy to me; shouldn't docs#lequivProdOfRightSplitExact come with some lemma that characterizes what the module isomorphism is?

[Eric Wieser]

My suspicious is that by the time we've proved that, the category theory route to the proof is an unecessary detour

[Jz Pan]

Eric Wieser said:

Though this all seems a big fishy to me; shouldn't docs#lequivProdOfRightSplitExact come with some lemma that characterizes what the module isomorphism is?

Yes that was my original plan. Will look at it later.