Jacobian conjecture

JacobianConjecturePropdef

The Jacobian conjecture for a ring k and index type σ: every IsKellerMap is an IsPolynomialAutomorphism. Open over a field of characteristic zero in every dimension above one.

def JacobianConjectureProp (k σ : Type*) [CommRing k] [Fintype σ] [DecidableEq σ] : Prop :=
  ∀ F : RegularFunction k σ σ, IsKellerMap F → IsPolynomialAutomorphism F

Builds on

Keller map
Polynomial automorphism

Used by

Counterexample to the Jacobian conjecture in dimension three
Problem JC-002
Problem JC-003

import Conjectura.Statements.Mathematics.AlgebraicGeometry.JacobianConjecture · 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