independent submodules

Stream: mathlib4

[Jiang Xu Wan]

With the definition of isotypic component, I'm trying to show that for an arbitrary module M, the set of all isotypic components of M that come from simple modules is an independent set of submodules of M. How do I express that a set of submodules is independent? In particular, LinearAlgebra.LinearIndependent seems to be useful for later lemmas/theorems I want to prove, but that definition of dependence is on sets of elements of M. I've tried some ways to use this by grabbing representative elements from each isotypic component to perform LinearAlgebra.LinearIndependent on, but I'm getting errors. Any suggestions?

[Lior Silberman]

Isn't there a notion of "the sum of these submodules is direct"?

[Notification Bot]

2 messages were moved here from #mathlib4 > two-sided ideals by Johan Commelin.

[Johan Commelin]

@Jiang Xu Wan I think docs#CompleteLattice.Independent is what you are looking for.

[Eric Wieser]

Or possibly docs#DirectSum.IsInternal

[Junyan Xu]

Here are some suggestions:

• define IsIsotypicModule R M to mean that the R-module M is semisimple with all simple submodules isomorphic;
• for m : Submodule R M, define IsIsotypicComponent m to mean that m is maximal among all submodules satisfying IsIsotypicModule R m (we probably also want to require that m ≠ ⊥ in case M has no simple submodules; assuming M is semisimple, this only happens when M=0);
• show the set of all submodules satisfying IsIsotypicComponent satisfies docs#CompleteLattice.SetIndependent;
• if IsIsotypicComponent m is true, then for all simple submodule s ≤ m, we have isotypic R M s = m (where isotypic is as defined here in the other thread); we may want to define a function that sens m to an arbitrary chosen simple submodule s;
• for each isotypic component m, you can get a direct sum decomposition into simples using a version of docs#exists_setIndependent_of_sSup_atoms_eq_top with sSup s = ⊤ replaced by sSup s = m.

[Jiang Xu Wan]

whilst I didn't use most of your suggestions, I was able to prove that if S is simple, then isotypic R M S is semisimple (which took quite a bit more effort than I was expecting), which let me use docs#exists_setIndependent_of_sSup_atoms_eq_top via #IsSemisimpleModule.sSup_simples_eq_top. Still, thank you for bringing docs#exists_setIndependent_of_sSup_atoms_eq_top to my attention.

[Jiang Xu Wan]

Now something I'm not entirely sure how to do is how to convert the set of independent submodules from docs#exists_setIndependent_of_sSup_atoms_eq_top into an indexed set for use in docs#DirectSum.IsInternal (in particular, I'm thinking to use DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top to establish that an isotypic component can be written as an internal direct sum, namely of the independent set of spanning atoms)

[Eric Wieser]

If you have an independent set, you can use the set itself as the indexing type

[Jiang Xu Wan]

I was trying that out, but the problem is that the indexing set needs to satisfy DecidableEq and SupSet, and I couldn't synthesize those on the indexing set. I need a work-around for this

[Eric Wieser]

I would be surprised if the indexing set has to satisfy SupSet. You can use letI := Classical.decEq s to get the former typeclass

[Jiang Xu Wan]

Okay, that helped, thanks! I just needed to make the index set be Subtype.val (and it took quite a few tries to get that to work), and I now have isotypic R M S is a direct sum