Downstream witness from a universal mortal sequence

The only theorem hypothesis in the final construction is scalar linearization, stated at the concrete backward-shift operator algebra. The unrestricted nil_of_all_pencils_nil theorem can be supplied directly to this hypothesis. All window-to-polynomial and nonnilpotent-matrix bridges are proved here.

The witness ring is the unitization over k of the positive shift algebra, and its nil ideal is the kernel of the scalar projection. The universe of the existential witness is exactly the universe of the ground field.

@[instance_reducible]

noncomputable def KoetheCounterexample.ShiftWitness.moduleEnd {k : Type u} [Field k] : Module k (End (RatFunc k))

The k-module structure on the endomorphism algebra, chosen to be definitionally the one coming from its k-algebra structure so that NonUnitalSubalgebra and Module.End agree.

Equations

• KoetheCounterexample.ShiftWitness.moduleEnd = Algebra.toModule

noncomputable def KoetheCounterexample.ShiftWitness.positiveAlgebra {k : Type u} [Field k] (v : ℕ → Triple k) : NonUnitalSubalgebra k (End (RatFunc k))

The positive algebra is generated over k, NOT over RatFunc k.

Equations

• KoetheCounterexample.ShiftWitness.positiveAlgebra v = NonUnitalAlgebra.adjoin k (Set.range (KoetheCounterexample.ShiftWitness.backShift v))

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

Once the positive shift algebra is nil, the rational-function eigenvector gives a nil ideal and nonnilpotent matrix in its actual unitization.

theorem KoetheCounterexample.ShiftWitness.exists_nilideal_nonnil_matrix {k : Type u} [Field k] (v : ℕ → Triple k) (hv : UniversalMortalSequence k v) (hlinear : ∀ (a : Fin 3 → End (RatFunc k)), (∀ (d : ℕ) (P : Pencil k d), IsNilpotent (P.lift a)) → ∀ x ∈ NonUnitalAlgebra.adjoin k (Set.range a), IsNilpotent x) : ∃ (R : Type u) (x : Ring R) (I : TwoSidedIdeal R), (∀ x_1 ∈ I, IsNilpotent x_1) ∧ ∃ W ∈ TwoSidedIdeal.matrix (Fin 2) I, ¬IsNilpotent W

Universe-preserving existential form of the requested nil-ideal plus nonnilpotent Fin 2 matrix witness. Scalar linearization is an explicit theorem argument, not an axiom. Only its specialization to the concrete operator algebra is needed, so a universe-polymorphic linearization theorem plugs in directly.