Polynomial maps between affine spaces

8 fully proved

Mv Polynomial

AbbreviationRegular functions#✓fully proved

For a commutative semiring \(k\) and index types \(\sigma\) and \(\tau\), a regular function from \(k^\sigma\) to \(k^\tau\) is a family \(F = (F_t)_{t \in \tau}\) of polynomials in the variables \(X_s\), \(s \in \sigma\), with coefficients in \(k\).

The components are formal polynomials, not functions on \(k^\sigma\).

abbrev RegularFunction := τ → MvPolynomial σ k

Used by 7

Used byEvaluation of a regular function at a point · Composition of regular functions · Evaluation respects composition · Associativity of composition of regular functions · The identity is a right unit for composition · The identity is a left unit for composition · Jacobian matrix of a regular function

Regular Function

DefinitionJacobian matrix of a regular function#✓fully proved

The Jacobian of a regular function \(F = (F_j)_{j \in \tau}\) from \(k^\sigma\) to \(k^\tau\) is the \(\tau \times \sigma\) matrix, with entries in the polynomial ring \(k[X_i : i \in \sigma]\), whose entry in row \(j\) and column \(i\) is the formal partial derivative \(\partial F_j / \partial X_i\).

Rows are indexed by the components and columns by the variables, following the usual matrix convention, so the Jacobian multiplies column vectors indexed by \(\sigma\).

noncomputable def Jacobian (F : RegularFunction k σ τ) :
    Matrix τ σ (MvPolynomial σ k) :=
  Matrix.of fun j i => MvPolynomial.pderiv i (F j)

Uses 1

Statement usesRegular functions

DefinitionComposition of regular functions#✓fully proved

For regular functions \(G\) from \(k^\tau\) to \(k^\iota\) and \(F\) from \(k^\sigma\) to \(k^\tau\), the composition \(G \circ F\) is the regular function from \(k^\sigma\) to \(k^\iota\) whose \(i\)-th component, for \(i \in \iota\), is the polynomial obtained from \(G_i\) by substituting \(F_t\) for the variable \(X_t\) for every \(t \in \tau\).

noncomputable def comp
    (G : RegularFunction k τ ι) (F : RegularFunction k σ τ) :
    RegularFunction k σ ι :=
  fun (i : ι) ↦ MvPolynomial.bind₁ F (G i)

Uses 1 · Used by 4

Statement usesRegular functions

Used byEvaluation respects composition · Associativity of composition of regular functions · The identity is a right unit for composition · The identity is a left unit for composition

LemmaThe identity is a left unit for composition#✓fully proved

For every regular function \(F\) from \(k^\sigma\) to \(k^\tau\), composing the identity regular function on \(k^\tau\), whose components are the variables \(X_t\) for \(t \in \tau\), with \(F\) gives \(F\), that is, \(\mathrm{id} \circ F = F\).

lemma id_comp (F : RegularFunction k σ τ) : (id k τ).comp F = F

Uses 2

Statement usesRegular functions · Composition of regular functions

LemmaThe identity is a right unit for composition#✓fully proved

For every regular function \(F\) from \(k^\sigma\) to \(k^\tau\), composing \(F\) with the identity regular function on \(k^\sigma\), whose components are the variables \(X_s\) for \(s \in \sigma\), gives \(F\), that is, \(F \circ \mathrm{id} = F\).

lemma comp_id (F : RegularFunction k σ τ) : F.comp (id k σ) = F

Uses 2

Statement usesRegular functions · Composition of regular functions

LemmaAssociativity of composition of regular functions#✓fully proved

For regular functions \(H\) from \(k^\iota\) to \(k^\kappa\), \(G\) from \(k^\tau\) to \(k^\iota\) and \(F\) from \(k^\sigma\) to \(k^\tau\), we have \((H \circ G) \circ F = H \circ (G \circ F)\).

lemma comp_assoc (H : RegularFunction k ι κ) (G : RegularFunction k τ ι)
    (F : RegularFunction k σ τ) :
    (H.comp G).comp F = H.comp (G.comp F)

Uses 2

Statement usesRegular functions · Composition of regular functions

DefinitionEvaluation of a regular function at a point#✓fully proved

Let \(k\) be a commutative semiring and let \(S\) be a commutative \(k\)-algebra. For a regular function \(F\) from \(k^\sigma\) to \(k^\tau\) and a point \(a \in S^\sigma\), the evaluation of \(F\) at \(a\) is the point \(F(a) \in S^\tau\) whose \(t\)-th coordinate, for \(t \in \tau\), is the value of the polynomial \(F_t\) at \(a\), obtained by substituting \(a_s\) for \(X_s\) for every \(s \in \sigma\).

noncomputable def aeval {σ τ : Type*} {S₁ : Type*} [CommSemiring S₁] [Algebra k S₁]
    (F : RegularFunction k σ τ) : (σ → S₁) → τ → S₁ :=
  fun a t ↦ MvPolynomial.aeval a (F t)

Uses 1 · Used by 1

Statement usesRegular functions

Used byEvaluation respects composition

LemmaEvaluation respects composition#✓fully proved

Let \(k\) be a commutative semiring and let \(S\) be a commutative \(k\)-algebra. For regular functions \(G\) from \(k^\tau\) to \(k^\iota\) and \(F\) from \(k^\sigma\) to \(k^\tau\) and every point \(a \in S^\sigma\), write \(F(a) \in S^\tau\) for the evaluation of \(F\) at \(a\). Then evaluating the composition \(G \circ F\) at \(a\) gives \(G(F(a))\), the evaluation of \(G\) at the point \(F(a)\).

lemma comp_aeval
    {σ τ ι S₁ : Type*} [CommSemiring S₁] [Algebra k S₁]
    (G : RegularFunction k τ ι) (F : RegularFunction k σ τ)
    (a : σ → S₁) : (G.comp F).aeval a = G.aeval (F.aeval a)

Uses 3

Statement usesRegular functions · Evaluation of a regular function at a point · Composition of regular functions

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.