Regular function

RegularFunctionabbrev

A regular function k^σ → k^τ is a tuple of multivariate polynomials, one per output coordinate. It is the formal stand-in for "polynomial map", and the object every statement in this area is about.

abbrev RegularFunction (k : Type*) [CommRing k] (σ τ : Type*) := τ → MvPolynomial σ k

compdef

Composition of regular functions, by polynomial substitution.

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

iddef

The identity regular function: each coordinate is its own variable.

noncomputable def id : RegularFunction k σ σ := MvPolynomial.X

aevaldef

Evaluation of a regular function at a point of k^σ.

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

Used by

From Mathlib

import Conjectura.Defs.Mathematics.AlgebraicGeometry.RegularFunction · maintainer — open · raw source

Adapted for Conjectura from formal-conjectures (Google DeepMind), `FormalConjectures/Wikipedia/JacobianConjecture.lean`. Split into one concept per module; no mathematical content changed.

Copyright (c) 2025 The Formal Conjectures Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Formal Conjectures Authors

Full credits