Finite homogeneous-linear systems

A system has a distinguished input, finitely many internal states, and an output row. Its coefficients are linear combinations of the three generators, with no scalar/identity edges. Represents is the elimination property of the internal system. We construct this property directly, without needing a matrix inverse or a nilpotence assumption on the ambient algebra.

noncomputable def KoetheCounterexample.Linearization.edge {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (a : Fin 3 → R) (c : Triple k) : Polynomial R

Evaluate one homogeneous-linear edge, as a constant polynomial.

Equations

• KoetheCounterexample.Linearization.edge a c = Polynomial.C (∑ i : Fin 3, (algebraMap k R) (c i) * a i)

@[simp]

theorem KoetheCounterexample.Linearization.edge_zero {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (a : Fin 3 → R) : edge a 0 = 0

@[simp]

theorem KoetheCounterexample.Linearization.edge_add {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (a : Fin 3 → R) (c d : Triple k) : edge a (c + d) = edge a c + edge a d

@[simp]

theorem KoetheCounterexample.Linearization.edge_smul {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (a : Fin 3 → R) (r : k) (c : Triple k) : edge a (r • c) = Polynomial.C ((algebraMap k R) r) * edge a c

def KoetheCounterexample.Linearization.letter {k : Type u} [Field k] (i : Fin 3) : Triple k

Coefficients selecting just one letter.

Equations

• KoetheCounterexample.Linearization.letter i j = if j = i then 1 else 0

@[simp]

theorem KoetheCounterexample.Linearization.edge_letter {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (a : Fin 3 → R) (i : Fin 3) : edge a (letter i) = Polynomial.C (a i)

structure KoetheCounterexample.Linearization.System (k : Type u) [Field k] : Type (max 1 u)

A finite homogeneous-linear system. The root is not among State.

• State : Type

  The internal states.

• fintype : Fintype self.State

  The states are finitely many.

• decEq : DecidableEq self.State

  Equality of states is decidable.

• head : Triple k

  The coefficient of the input in the output row.

• out : self.State → Triple k

  The coefficient of each internal state in the output row.

• input : self.State → Triple k

  The coefficient of the input in each internal equation.

• step : self.State → self.State → Triple k

  The coefficient of each internal state in each internal equation.

def KoetheCounterexample.Linearization.Represents {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (S : System k) (a : Fin 3 → R) (x : R) : Prop

Every solution of the internal equations gives the specified output. All equations take place in the polynomial ring over the possibly noncommutative algebra R.

Equations

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

def KoetheCounterexample.Linearization.Linearizable {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (a : Fin 3 → R) (x : R) : Prop

The elements admitting one of these finite linearizations.

Equations

• KoetheCounterexample.Linearization.Linearizable a x = ∃ (S : KoetheCounterexample.Linearization.System k), KoetheCounterexample.Linearization.Represents S a x

def KoetheCounterexample.Linearization.System.atom {k : Type u} [Field k] (c : Triple k) : System k

A single homogeneous-linear output, with no internal states.

Equations

• KoetheCounterexample.Linearization.System.atom c = { State := Empty, fintype := inferInstance, decEq := inferInstance, head := c, out := Empty.elim, input := Empty.elim, step := Empty.elim }

def KoetheCounterexample.Linearization.System.add {k : Type u} [Field k] (S T : System k) : System k

Disjoint union of systems, adding their output rows.

Equations

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

def KoetheCounterexample.Linearization.System.smul {k : Type u} [Field k] (r : k) (S : System k) : System k

Only the output row is scaled.

Equations

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

def KoetheCounterexample.Linearization.System.prepend {k : Type u} [Field k] (i : Fin 3) (S : System k) : System k

Prepend a generator: a new internal state computes the old output, and one generator edge joins the new output to that state.

Equations

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

theorem KoetheCounterexample.Linearization.System.sum_atom_state {k : Type u} [Field k] {M : Type u_1} [AddCommMonoid M] (c : Triple k) (g : (atom c).State → M) : ∑ j : (atom c).State, g j = 0

A sum over the (empty) state type of an atom vanishes.

theorem KoetheCounterexample.Linearization.System.sum_add_state {k : Type u} [Field k] {M : Type u_1} [AddCommMonoid M] (S T : System k) (g : (S.add T).State → M) : ∑ j : (S.add T).State, g j = ∑ j : S.State, g (Sum.inl j) + ∑ j : T.State, g (Sum.inr j)

A sum over the states of S.add T splits into the two summands.

theorem KoetheCounterexample.Linearization.System.sum_prepend_state {k : Type u} [Field k] {M : Type u_1} [AddCommMonoid M] (i : Fin 3) (S : System k) (g : (prepend i S).State → M) : ∑ j : (prepend i S).State, g j = g none + ∑ j : S.State, g (some j)

A sum over the states of S.prepend i isolates the new state.

@[simp]

theorem KoetheCounterexample.Linearization.represents_atom {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (a : Fin 3 → R) (c : Triple k) : Represents (System.atom c) a (∑ i : Fin 3, (algebraMap k R) (c i) * a i)

theorem KoetheCounterexample.Linearization.linearizable_zero {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (a : Fin 3 → R) : Linearizable a 0

theorem KoetheCounterexample.Linearization.linearizable_letter {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] (a : Fin 3 → R) (i : Fin 3) : Linearizable a (a i)

theorem KoetheCounterexample.Linearization.Represents.add {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] {S T : System k} {a : Fin 3 → R} {x y : R} (hS : Represents S a x) (hT : Represents T a y) : Represents (S.add T) a (x + y)

theorem KoetheCounterexample.Linearization.Represents.smul {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] {S : System k} {a : Fin 3 → R} {x : R} (hS : Represents S a x) (r : k) : Represents (System.smul r S) a (r • x)

theorem KoetheCounterexample.Linearization.Represents.prepend {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] {S : System k} {a : Fin 3 → R} {x : R} (hS : Represents S a x) (i : Fin 3) : Represents (System.prepend i S) a (a i * x)

theorem KoetheCounterexample.Linearization.linearizable_add {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] {a : Fin 3 → R} {x y : R} (hx : Linearizable a x) (hy : Linearizable a y) : Linearizable a (x + y)

theorem KoetheCounterexample.Linearization.linearizable_smul {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] {a : Fin 3 → R} {x : R} (hx : Linearizable a x) (r : k) : Linearizable a (r • x)

theorem KoetheCounterexample.Linearization.linearizable_prepend {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] {a : Fin 3 → R} {x : R} (hx : Linearizable a x) (i : Fin 3) : Linearizable a (a i * x)