Jacobian matrix

Conjectura.Defs.Mathematics.AlgebraicGeometry.Jacobian

/-
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
import Mathlib.Algebra.MvPolynomial.PDeriv
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic

/-! # Jacobian matrix

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

/-- The **Jacobian matrix** of a `RegularFunction`: the matrix of formal partial derivatives
`∂Fⱼ/∂xᵢ`. Note that its entries are polynomials, not scalars — it is a matrix that varies
from point to point. -/
noncomputable def RegularFunction.Jacobian {k : Type*} [CommRing k] {σ τ : Type*}
    (F : RegularFunction k σ τ) : Matrix σ τ (MvPolynomial σ k) :=
  Matrix.of fun i j => MvPolynomial.pderiv i (F j)

end Conjectura.AlgebraicGeometry