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 β†’

Counterexample to the Jacobian conjecture in dimension three

Conjectura.Vendor.JacobianCounterexample

/-
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.Statements.Mathematics.AlgebraicGeometry.JacobianConjecture
import Conjectura.Theorems.Mathematics.AlgebraicGeometry.RegularFunction

/-! # Counterexample to the Jacobian conjecture in dimension three

## Source

Vendored for Conjectura from
[formal-conjectures](https://github.com/google-deepmind/formal-conjectures)
(Google DeepMind), formalised by Paul Lezeau. Released under Apache 2.0.
-/

namespace Conjectura.AlgebraicGeometry

open MvPolynomial RegularFunction

section Counterexample

variable (k : Type*) [CommRing k]

local notation "𝑋" => (MvPolynomial.X 0 : MvPolynomial (Fin 3) k)
local notation "π‘Œ" => (MvPolynomial.X 1 : MvPolynomial (Fin 3) k)
local notation "𝑍" => (MvPolynomial.X 2 : MvPolynomial (Fin 3) k)

/-- AlpΓΆge's counterexample: a self-map of `kΒ³` with Jacobian determinant `-2`
that is not injective. -/
noncomputable abbrev F : RegularFunction k (Fin 3) (Fin 3) :=
  ![(1 + 𝑋 * π‘Œ)^3 * 𝑍 + π‘Œ^2 * (1 + 𝑋 * π‘Œ) * (4 + 3 * 𝑋 * π‘Œ),
    π‘Œ + 3 * 𝑋 * (1 + 𝑋 * π‘Œ)^2 * 𝑍 + 3 * 𝑋 * π‘Œ^2 * (4 + 3 * 𝑋 * π‘Œ),
    2 * 𝑋 - 3 * 𝑋^2 * π‘Œ - 𝑋^3 * 𝑍]

/-- A variant with Jacobian determinant `1`, which works in every characteristic. -/
noncomputable abbrev G : RegularFunction k (Fin 3) (Fin 3) :=
  ![(1 + 2 * 𝑋 * π‘Œ)^3 * 𝑍 + 4 * π‘Œ^2 * (1 + 2 * 𝑋 * π‘Œ) * (2 + 3 * (𝑋 * π‘Œ)),
    π‘Œ + 3 * 𝑋 * (1 + 2 * 𝑋 * π‘Œ)^2 * 𝑍 + 12 * 𝑋 * π‘Œ^2 * (2 + 3 * (𝑋 * π‘Œ)),
    -𝑋 + 3 * 𝑋^2 * π‘Œ + 𝑋^3 * 𝑍]

theorem det_jacobian_G : (G k).Jacobian.det = 1 := by
  simp only [G, Jacobian, ← map_ofNat (C : k β†’+* MvPolynomial (Fin 3) k), Matrix.det_fin_three,
    Matrix.of_apply, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two,
    Matrix.head_cons, Matrix.tail_cons, map_add, map_neg, Derivation.map_one_eq_zero, pderiv_mul,
    pderiv_pow, pderiv_C, pderiv_X_self, pderiv_X_of_ne, ne_eq, Fin.reduceEq, not_false_eq_true]
  simp only [map_ofNat]
  ring

/-- `G` identifies the two distinct points `(1, 0, 1)` and `(0, 3, -71)`. -/
theorem aeval_G_eq : (G k).aeval ![1, 0, (1 : k)] = (G k).aeval ![0, 3, -71] := by
  funext i
  fin_cases i <;> simp [RegularFunction.aeval]; grind

end Counterexample

end Conjectura.AlgebraicGeometry