Facts about regular functions

Conjectura.Theorems.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 Conjectura.Defs.Mathematics.AlgebraicGeometry.RegularFunction

/-! # Facts about regular functions

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

namespace RegularFunction

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

/-- Evaluation commutes with composition. -/
lemma comp_aeval (F : RegularFunction k σ τ) (G : RegularFunction k τ ι) (a : σ → k) :
    (F.comp G).aeval a = G.aeval (F.aeval a) := by
  ext i
  rw [aeval, comp, MvPolynomial.aeval_bind₁, ← aeval]
  rfl

end RegularFunction

end Conjectura.AlgebraicGeometry