Documentation

Counterexamples.MonicNonRegular

Monic does not necessarily imply IsRegular in a Semiring with no opposites #

This counterexample shows that the hypothesis Ring R cannot be changed to Semiring R in Polynomial.Monic.isRegular.

The example is very simple.

The coefficient Semiring is the Semiring N₃ of the natural numbers {0, 1, 2, 3} where the standard addition and standard multiplication are truncated at 3.

The products (X + 2) * (X + 2) and (X + 2) * (X + 3) are equal to X ^ 2 + 4 * X + 4 and X ^ 2 + 5 * X + 6 respectively.

By truncation, 4, 5, 6 all mean 3 in N. It follows that multiplication by (X + 2) is not injective.

source
inductive Counterexample.NonRegular.N₃ :
Type

N₃ is going to be a CommSemiring where addition and multiplication are truncated at 3.

Instances For
    source
    instance Counterexample.NonRegular.N₃.instZero :
    Zero Counterexample.NonRegular.N₃
    Equations
    source
    instance Counterexample.NonRegular.N₃.instOne :
    One Counterexample.NonRegular.N₃
    Equations
    source
    instance Counterexample.NonRegular.N₃.instAdd :
    Add Counterexample.NonRegular.N₃

    Truncated addition on N₃.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance Counterexample.NonRegular.N₃.instMul :
    Mul Counterexample.NonRegular.N₃

    Truncated multiplication on N₃.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance Counterexample.NonRegular.N₃.instCommMonoid :
    CommMonoid Counterexample.NonRegular.N₃
    Equations
    source
    instance Counterexample.NonRegular.N₃.instCommSemiring :
    CommSemiring Counterexample.NonRegular.N₃
    Equations
    source
    theorem Counterexample.NonRegular.N₃.X_add_two_mul_X_add_two :
    (Polynomial.X + Polynomial.C 2) * (Polynomial.X + Polynomial.C 2) = (Polynomial.X + Polynomial.C 2) * (Polynomial.X + Polynomial.C 3)

    The main example: multiplication by the polynomial X + 2 is not injective, yet the polynomial is monic.

    source
    theorem Counterexample.NonRegular.N₃.monic_X_add_two :
    (Polynomial.X + Polynomial.C 2).Monic
    source
    theorem Counterexample.NonRegular.N₃.not_isLeftRegular_X_add_two :
    ¬IsLeftRegular (Polynomial.X + Polynomial.C 2)
    source
    theorem Counterexample.NonRegular.N₃.not_monic_implies_isLeftRegular :
    ¬∀ {R : Type} [inst : Semiring R] (p : Polynomial R), p.Monic → IsLeftRegular p

    The statement of the counterexample: not all monic polynomials over semirings are regular.