Backward shifts and exact polynomial mortality

The coefficientwise band identity below retains the pencil's independent formal variable. It does not deduce polynomial nilpotence from one specialization.

@[reducible, inline]

abbrev KoetheCounterexample.ShiftWitness.Space (K : Type v) : Type v

The full sequence space on which the backward shifts act.

Equations

• KoetheCounterexample.ShiftWitness.Space K = (ℕ → K)

@[reducible, inline]

abbrev KoetheCounterexample.ShiftWitness.End (K : Type v) [Field K] : Type v

The endomorphism algebra of the sequence space.

Equations

• KoetheCounterexample.ShiftWitness.End K = Module.End K (KoetheCounterexample.ShiftWitness.Space K)

def KoetheCounterexample.ShiftWitness.backShift {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] (v : ℕ → Triple k) (i : Fin 3) : End K

Backward weighted shifts: composition follows the forward chronological order of the shared Pencil.wordProd.

Equations

• KoetheCounterexample.ShiftWitness.backShift v i = { toFun := fun (u : KoetheCounterexample.ShiftWitness.Space K) (n : ℕ) => (algebraMap k K) (v n i) * u (n + 1), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem KoetheCounterexample.ShiftWitness.backShift_apply {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] (v : ℕ → Triple k) (i : Fin 3) (u : Space K) (n : ℕ) : (backShift v i) u n = (algebraMap k K) (v n i) * u (n + 1)

def KoetheCounterexample.ShiftWitness.HasBand {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] {ι : Type u_1} (m : ℕ) (Q : Matrix ι ι (Polynomial (End K))) (C : ℕ → Matrix ι ι (Polynomial k)) : Prop

Exact coefficient action of a polynomial matrix supported on one shift band.

Equations

• One or more equations did not get rendered due to their size.

theorem KoetheCounterexample.ShiftWitness.hasBand_one {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] {ι : Type u_1} [DecidableEq ι] : HasBand 0 1 fun (x : ℕ) => 1

theorem KoetheCounterexample.ShiftWitness.HasBand.mul {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] {ι : Type u_1} [Fintype ι] {m l : ℕ} {Q T : Matrix ι ι (Polynomial (End K))} {C D : ℕ → Matrix ι ι (Polynomial k)} (hQ : HasBand m Q C) (hT : HasBand l T D) : HasBand (m + l) (Q * T) fun (n : ℕ) => C n * D (n + m)

Multiplication of bands keeps the chronological order and shifts the second kernel by the width of the first band.

theorem KoetheCounterexample.ShiftWitness.linear_combination_apply {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] (v : ℕ → Triple k) (b : Fin 3 → k) (u : Space K) (n : ℕ) : (∑ i : Fin 3, (algebraMap k (End K)) (b i) * backShift v i) u n = (algebraMap k K) (∑ i : Fin 3, v n i * b i) * u (n + 1)

theorem KoetheCounterexample.ShiftWitness.pencil_hasBand {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] {d : ℕ} (P : Pencil k d) (v : ℕ → Triple k) : HasBand 1 (P.lift (backShift v)) fun (n : ℕ) => P.eval (v n)

The band kernel of a lifted pencil is its scalar polynomial evaluation at the edge vector.

@[simp]

theorem KoetheCounterexample.ShiftWitness.window_zero {k : Type u} [Field k] {d : ℕ} (P : Pencil k d) (v : ℕ → Triple k) (n : ℕ) : P.window v n 0 = 1

theorem KoetheCounterexample.ShiftWitness.window_succ {k : Type u} [Field k] {d : ℕ} (P : Pencil k d) (v : ℕ → Triple k) (n N : ℕ) : P.window v n (N + 1) = P.eval (v n) * P.window v (n + 1) N

theorem KoetheCounterexample.ShiftWitness.pencil_pow_hasBand {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] {d : ℕ} (P : Pencil k d) (v : ℕ → Triple k) (N : ℕ) : HasBand N (P.lift (backShift v) ^ N) fun (n : ℕ) => P.window v n N

All coefficients of every power have the window kernel, not just its value at a chosen rational function.

theorem KoetheCounterexample.ShiftWitness.pencil_nil_of_windows {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] {d : ℕ} (P : Pencil k d) (v : ℕ → Triple k) (N : ℕ) (hN : ∀ (n : ℕ), P.window v n N = 0) : P.lift (backShift v) ^ N = 0

Uniformly zero windows imply actual nilpotence in the polynomial matrix ring over the endomorphisms.

theorem KoetheCounterexample.ShiftWitness.all_pencils_nil {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] (v : ℕ → Triple k) (hv : UniversalMortalSequence k v) (d : ℕ) (P : Pencil k d) : IsNilpotent (P.lift (backShift v))