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 iSupIndep and that they span all of ℤ, they do not form a decomposition into a direct sum.

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

theorem Counterexample.UnitsInt.one_ne_neg_one : 1 ≠ -1

def Counterexample.withSign (i : ℤˣ) : Submodule ℕ ℤ

Submodules of positive and negative integers, keyed by sign.

Equations

• Counterexample.withSign i = AddSubmonoid.toNatSubmodule (have this := { carrier := {z : ℤ | 0 ≤ i • z}, add_mem' := ⋯, zero_mem' := ⋯ }; this)

theorem Counterexample.mem_withSign_one {x : ℤ} : x ∈ withSign 1 ↔ 0 ≤ x

theorem Counterexample.mem_withSign_neg_one {x : ℤ} : x ∈ withSign (-1) ↔ x ≤ 0

theorem Counterexample.withSign.isCompl : IsCompl (withSign 1) (withSign (-1))

The two submodules are complements.

theorem Counterexample.withSign.independent : iSupIndep withSign

theorem Counterexample.withSign.iSup : _root_.iSup withSign = ⊤

theorem Counterexample.withSign.not_injective : ¬Function.Injective ⇑(DirectSum.toModule ℕ ℤˣ ℤ fun (i : ℤˣ) => (withSign i).subtype)

But there is no embedding into ℤ from the direct sum.

theorem Counterexample.withSign.not_internal : ¬DirectSum.IsInternal withSign

And so they do not represent an internal direct sum.