Regular function

Conjectura.Defs.Mathematics.AlgebraicGeometry.RegularFunction

/-
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
-/
import Mathlib.Algebra.MvPolynomial.Monad
import Mathlib.Data.Fin.VecNotation

/-! # Regular function

## Source

Adapted for Conjectura from [formal-conjectures](https://github.com/google-deepmind/formal-conjectures) (Google DeepMind), `FormalConjectures/Wikipedia/JacobianConjecture.lean`. Split into one concept per module; no mathematical content changed.
-/

namespace Conjectura.AlgebraicGeometry

open MvPolynomial

/-- 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

namespace RegularFunction

variable {k : Type*} [CommRing k] {σ τ ι : Type*}

/-- **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)

variable (k σ) in
/-- The **identity** regular function: each coordinate is its own variable. -/
noncomputable def id : RegularFunction k σ σ := MvPolynomial.X

/-- **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)

end RegularFunction

end Conjectura.AlgebraicGeometry