Keller map

Conjectura.Defs.Mathematics.AlgebraicGeometry.KellerMap

/-
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.Jacobian
import Mathlib.Algebra.MvPolynomial.Nilpotent

/-! # Keller map

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

/-- A **Keller map** is a polynomial self-map whose `RegularFunction.Jacobian` determinant is a
unit. Over a field this is the same as the determinant being a non-zero constant, which is how
the condition is usually stated. -/
def IsKellerMap {k σ : Type*} [CommRing k] [Fintype σ] [DecidableEq σ]
    (F : RegularFunction k σ σ) : Prop :=
  IsUnit F.Jacobian.det

end Conjectura.AlgebraicGeometry