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.

theorem counterexample.units_int.one_ne_neg_one :

1 ≠ -1

def counterexample.with_sign (i : ℤ ˣ) :

submodule ℕ ℤ

Submodules of positive and negative integers, keyed by sign.

Equations

counterexample.with_sign i = ⇑add_submonoid.to_nat_submodule (show add_submonoid ℤ, from {carrier := {z : ℤ | 0 ≤ i • z}, add_mem' := _, zero_mem' := _})

theorem counterexample.mem_with_sign_one {x : ℤ} :

x ∈ counterexample.with_sign 1 ↔ 0 ≤ x

theorem counterexample.mem_with_sign_neg_one {x : ℤ} :

x ∈ counterexample.with_sign (-1) ↔ x ≤ 0

theorem counterexample.with_sign.is_compl :

is_compl (counterexample.with_sign 1) (counterexample.with_sign (-1))

The two submodules are complements.

def counterexample.with_sign.independent :

complete_lattice.independent counterexample.with_sign

theorem counterexample.with_sign.supr :

supr counterexample.with_sign = ⊤

theorem counterexample.with_sign.not_injective :

¬function.injective ⇑(direct_sum.to_module ℕ ℤ ˣ ℤ (λ (i : ℤ ˣ), (counterexample.with_sign i).subtype))

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

theorem counterexample.with_sign.not_internal :

¬direct_sum.is_internal counterexample.with_sign

And so they do not represent an internal direct sum.