Conjectura
Sign inRegister
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Jacobian conjecture

Conjectura.Statements.Mathematics.AlgebraicGeometry.JacobianConjecture

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

/-! # Jacobian conjecture

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

end Conjectura.AlgebraicGeometry