Not all complementary decompositions of a module over a semiring make up a direct sum #

This shows that while ℤ≤0 and ℤ≥0 are complementary -submodules of , which in turn implies as a collection they are CompleteLattice.Independent and that they span all of , they do not form a decomposition into a direct sum.

This file demonstrates why DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top must take Ring R and not Semiring R.

Submodules of positive and negative integers, keyed by sign.

Instances For

    But there is no embedding into from the direct sum.

    And so they do not represent an internal direct sum.