abelian group decomposition

Stream: Is there code for X?

[Winston Yin]

Is there a "fundamental theorem of finitely generated abelian groups" in mathlib?

[Johan Commelin]

@Winston Yin Not the full theorem. But several parts are there. For example: submodule of free module over a PID is free.

[Johan Commelin]

The classification of torsion modules is missing.

[Johan Commelin]

What exactly is the statement that you need?

[Winston Yin]

I see. I don't need the theorem itself. I'm just trying to find something to model the definition of a representation decomposition after...

[Winston Yin]

I'm stuck at a problem where my definition of "isomorphic to a direct sum of modules" is not properly finding the type class instance for the direct sum module

[Winston Yin]

I'm trying to write a mwe to debug the problem

[Eric Wieser]

This problem happens a lot, there are various threads about typeclass issues for direct_sum and dfinsupp

[Eric Wieser]

You might want docs#direct_sum.submodule_is_internal for "isomorphic to a direct sum of (sub)modules"

[Winston Yin]

I'll take a look. I have some isomorphism that extends linear_equiv as well as a function symm that returns the opposite isomorphism, but when I actually try to use symm on an isomorphism between some V and some direct_sum ι V', it fails to synthesise the module instance for the direct_sum.

[Eric Wieser]

Adding an explicit type on your isomorphism with (the_iso : X ≃ₗ [R] Y).symm is sometimes enough to sort lean out.