Semantic input substitutions

An input substitution expresses every old input as a scalar function of a new input vector. It covers ordinary restrictions, variable identifications, and affine or higher-degree substitutions without imposing basis-specific syntax.

@[reducible, inline]

abbrev Algebraic.InputSubstitution (U : Type u) (n k : ℕ) : Type u

A substitution of n old inputs by scalar functions of k new inputs.

Equations

• Algebraic.InputSubstitution U n k = (Fin n → Algebraic.ScalarFunction U k)

def Algebraic.InputSubstitution.apply {U : Type u_1} {n k : ℕ} (substitution : InputSubstitution U n k) (input : Fin k → U) : Fin n → U

Evaluate an input substitution on a new input vector.

Equations

• substitution.apply input oldInput = substitution oldInput input

def Algebraic.InputSubstitution.id {U : Type u_1} {n : ℕ} : InputSubstitution U n n

The identity input substitution.

Equations

• Algebraic.InputSubstitution.id input values = values input

@[simp]

theorem Algebraic.InputSubstitution.id_apply {n : ℕ} {U : Type u_1} (input : Fin n → U) : id.apply input = input

def Algebraic.InputSubstitution.comp {U : Type u_1} {n k l : ℕ} (outer : InputSubstitution U n k) (inner : InputSubstitution U k l) : InputSubstitution U n l

Compose input substitutions, applying inner before outer.

Equations

• outer.comp inner oldInput input = outer oldInput (inner.apply input)

@[simp]

theorem Algebraic.InputSubstitution.comp_apply {U : Type u_1} {n k l : ℕ} (outer : InputSubstitution U n k) (inner : InputSubstitution U k l) (input : Fin l → U) : (outer.comp inner).apply input = outer.apply (inner.apply input)

@[simp]

theorem Algebraic.InputSubstitution.comp_id {U : Type u_1} {n k : ℕ} (substitution : InputSubstitution U n k) : substitution.comp id = substitution

@[simp]

theorem Algebraic.InputSubstitution.id_comp {U : Type u_1} {n k : ℕ} (substitution : InputSubstitution U n k) : id.comp substitution = substitution

theorem Algebraic.InputSubstitution.comp_assoc {U : Type u_1} {n k l r : ℕ} (first : InputSubstitution U n k) (second : InputSubstitution U k l) (third : InputSubstitution U l r) : (first.comp second).comp third = first.comp (second.comp third)

def Algebraic.InputSubstitution.fix {n : ℕ} {U : Type u_1} (selected : Fin (n + 1)) (value : U) : InputSubstitution U (n + 1) n

Fix one input of an (n + 1)-input function and reindex the others.

Equations

• Algebraic.InputSubstitution.fix selected value oldInput input = selected.insertNth value input oldInput

@[simp]

theorem Algebraic.InputSubstitution.fix_selected {n : ℕ} {U : Type u_1} (selected : Fin (n + 1)) (value : U) (input : Fin n → U) : (fix selected value).apply input selected = value

@[simp]

theorem Algebraic.InputSubstitution.fix_succAbove {n : ℕ} {U : Type u_1} (selected : Fin (n + 1)) (value : U) (input : Fin n → U) (remaining : Fin n) : (fix selected value).apply input (selected.succAbove remaining) = input remaining

def Algebraic.Target.substitute {U : Type u_1} {n m k : ℕ} (target : Target U n m) (substitution : InputSubstitution U n k) : Target U k m

Restrict a target along an input substitution.

Equations

• target.substitute substitution input = target (substitution.apply input)

@[simp]

theorem Algebraic.Target.substitute_apply {U : Type u_1} {n m k : ℕ} (target : Target U n m) (substitution : InputSubstitution U n k) (input : Fin k → U) : target.substitute substitution input = target (substitution.apply input)

@[simp]

theorem Algebraic.Target.substitute_id {U : Type u_1} {n m : ℕ} (target : Target U n m) : target.substitute InputSubstitution.id = target

theorem Algebraic.Target.substitute_comp {U : Type u_1} {n m k l : ℕ} (target : Target U n m) (outer : InputSubstitution U n k) (inner : InputSubstitution U k l) : (target.substitute outer).substitute inner = target.substitute (outer.comp inner)