The counterexample: a nil ideal with a non-nilpotent 2 × 2 matrix

This file assembles the whole development. The scalar-linearization theorem KoetheCounterexample.nil_of_all_pencils_nil discharges the explicit hypothesis of KoetheCounterexample.ShiftWitness.exists_nilideal_nonnil_matrix, and the ground field GroundField = AlgebraicClosure (ULift (ZMod 2)) is countable and algebraically closed, so exists_universalMortalSequence and maskMortality apply to it. The result is a ring R in an arbitrary universe, a nil two-sided ideal I ⊆ R, and a matrix in M_2(I) that is not nilpotent.

theorem KoetheCounterexample.exists_nilideal_nonnil_matrix_of_universal_mortal {k : Type u} [Field k] (v : ℕ → Triple k) (hv : UniversalMortalSequence k v) : ∃ (R : Type u) (x : Ring R) (I : TwoSidedIdeal R), (∀ x_1 ∈ I, IsNilpotent x_1) ∧ ∃ W ∈ TwoSidedIdeal.matrix (Fin 2) I, ¬IsNilpotent W

A universal mortal sequence over any field produces a nil two-sided ideal in a unital ring, with a nonnilpotent two-by-two matrix over that ideal.

@[reducible, inline]

abbrev KoetheCounterexample.GroundField : Type u

The countable algebraically closed ground field \overline{𝔽₂}, lifted to an arbitrary universe so that the counterexample exists in every universe.

Equations

• KoetheCounterexample.GroundField = AlgebraicClosure (ULift.{?u.1, 0} (ZMod 2))

instance KoetheCounterexample.countable_groundField : Countable GroundField

theorem KoetheCounterexample.counterexample : ∃ (R : Type u) (x : Ring R) (I : TwoSidedIdeal R), (∀ x_1 ∈ I, IsNilpotent x_1) ∧ ∃ W ∈ TwoSidedIdeal.matrix (Fin 2) I, ¬IsNilpotent W

A counterexample to nilness of finite matrix ideals. In every universe there is a ring R with a nil two-sided ideal I such that the matrix ideal M_2(I) of M_2(R) contains a non-nilpotent matrix.