Documentation

Counterexamples.DirectSumIsInternal

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.

source
theorem Counterexample.UnitsInt.one_ne_neg_one :
1 ≠ -1
source
def Counterexample.withSign (i : ℤˣ) :
Submodule ℕ ℤ

Submodules of positive and negative integers, keyed by sign.

Equations
Instances For
    source
    theorem Counterexample.mem_withSign_one {x : ℤ} :
    x ∈ Counterexample.withSign 1 ↔ 0 ≤ x
    source
    theorem Counterexample.mem_withSign_neg_one {x : ℤ} :
    x ∈ Counterexample.withSign (-1) ↔ x ≤ 0
    source
    theorem Counterexample.withSign.isCompl :
    IsCompl (Counterexample.withSign 1) (Counterexample.withSign (-1))

    The two submodules are complements.

    source
    def Counterexample.withSign.independent :
    iSupIndep Counterexample.withSign
    Equations
    Instances For
      source
      theorem Counterexample.withSign.iSup :
      iSup Counterexample.withSign = ⊤
      source
      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.

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

      And so they do not represent an internal direct sum.