mathlib3 documentation

mathlib-counterexamples / direct_sum_is_internal

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

This file demonstrates why direct_sum.is_internal_submodule_of_independent_of_supr_eq_top must take ring R and not semiring R.

Submodules of positive and negative integers, keyed by sign.


The two submodules are complements.

But there is no embedding into from the direct sum.

And so they do not represent an internal direct sum.