Keller map

IsKellerMapdef

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

Builds on

Jacobian matrix

Used by

Facts about Keller maps
Jacobian conjecture

From Mathlib

Algebra.MvPolynomial.Nilpotent

import Conjectura.Defs.Mathematics.AlgebraicGeometry.KellerMap · 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