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.

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 (let_fun this := { carrier := {z : ℤ | 0 ≤ i • z}, add_mem' := ⋯, zero_mem' := ⋯ }; this)

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

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

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

The two submodules are complements.

def Counterexample.withSign.independent : CompleteLattice.Independent Counterexample.withSign

Equations

• Counterexample.withSign.independent = ⋯

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

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

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

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

And so they do not represent an internal direct sum.