indecomposable module

Stream: Is there code for X?

[Kevin Buzzard]

A module is indecomposable if it's not 0 and cannot be written as a product of two nonzero submodules. More precisely for this latter condition, you can either say that there doesn't exist A B : Submodule R M with A ⊔ B = ⊤ and A ⊓ B = ⊥ (other than bot and top), or you could say that there doesn't exist A B : Module R with A × B ≃ₗ[R] M and both A,B nontrivial. Do we not have this concept yet in mathlib? Someone suggested SupIrred but I don't think this is quite right -- it might be too strong. I am envisioning a module with four submodules A,B,A \cap B and then 0 strictly under A \cap B and that's it. This might be indecomposable but not SupIrred, if it can happen at all.

[Eric Wieser]

Is this IsSimpleOrder (Submodule R M)? (docs#IsSimpleOrder)

[Eric Wieser]

Answer: no, but maybe the statement should also be lattice-theoretic via docs#IsCompl

[Kevin Buzzard]

Right -- $\Z/p^n\Z$ is indecomposable even though it has submodules $(p)\supseteq(p^2)\supseteq\cdots$.

[Kevin Buzzard]

Yeah so it seems to say that IsCompl x y is true exactly twice (bot,top and top,bot, and bot isn't top).

[Antoine Chambert-Loir]

Yes. But you could say that x or y is bot, but the module itself is not bot. As for irreducibility.

[Kevin Buzzard]

Aha -- top isn't bot, but if top = x \sup y with x \inf y = bot then x = bot or y = bot. Makes it look like the definition of prime.

[Eric Wieser]

I guess ∀ x y, ⊥ < x → x < ⊤ → ⊥ < y → y < ⊤ → IsCompl x y → False would work?

[Eric Wieser]

(I'd be inclined to drop " if it's not 0" and let Nontrivial M handle that)

[Kevin Buzzard]

This would be true for the trivial module

[Kevin Buzzard]

x <= y looks very fishy to me, those would never be compl.

[Eric Wieser]

Oh whoops, I had linear orders on my mind - edited

[Kevin Buzzard]

yeah I think the revision is fine.