1. FormalConjecturesForMathlib
  2. Algebra
  3. MvPolynomial
  4. RegularFunction
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module public import Mathlib.Algebra.MvPolynomial.Monad public import Mathlib.Algebra.MvPolynomial.PDeriv public import Mathlib.Data.Matrix.Basicpublic section

Regular functions between affine spaces

A regular function from $k^σ$ to $k^τ$ is a $τ$-indexed family of polynomials in the variables $σ$, i.e. a vector valued polynomial function. This file provides the basic API: the Jacobian matrix, composition, the identity, and evaluation at a point.

namespace MvPolynomialvariable {k : Type*} [CommRing k]variable {σ τ ι : Type*}variable (k σ τ) in

The type of regular functions from $k^σ$ to $k^τ$.

abbrev RegularFunction := τ → MvPolynomial σ knamespace RegularFunction

The Jacobian of a vector valued polynomial function, viewed as a polynomial.

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

The composition of two vector valued polynomial functions.

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

The evaluation of a regular function f over k at some point a with coordinates in some algebra over k

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

aeval is compatible with composition of regular functions.

k:Type u_1inst✝:CommRing kσ:Type u_5τ:Type u_6ι:Type u_7F:RegularFunction k σ τG:RegularFunction k τ ιa:σ → ki:ι⊢ G.aeval (fun i ↦ (MvPolynomial.aeval a) (F i)) i = G.aeval (F.aeval a) i All goals completed! 🐙end RegularFunctionend MvPolynomial