import Mathlib

noncomputable section

open Matrix Function

/-! # A counterexample to the Jacobian conjecture in dimension three

We formalize the polynomial map

  F : ℂ³ → ℂ³

whose Jacobian determinant is the constant `-2`, but which is not injective.

The final theorem `jacobianConjecture3_false` states the failure of the polynomial-inverse formulation of the Jacobian conjecture in dimension three. -/

namespace MvPolynomial

variable {R : Type} {σ : Type}

/-- The formal Jacobian matrix of a family of multivariate polynomials. -/ def jacobianMatrix [CommSemiring R] [DecidableEq σ] (F : σ → MvPolynomial σ R) : Matrix σ σ (MvPolynomial σ R) := Matrix.of fun i j ↦ pderiv j (F i)

/-- The formal Jacobian determinant. -/ def jacobianDet [CommRing R] [Fintype σ] [DecidableEq σ] (F : σ → MvPolynomial σ R) : MvPolynomial σ R := (jacobianMatrix F).det

/-- Evaluation of a polynomial map at a point. -/ def evalMap [CommSemiring R] (F : σ → MvPolynomial σ R) (p : σ → R) : σ → R := fun i ↦ eval p (F i)

end MvPolynomial

open MvPolynomial

namespace JacobianCounterexample

variable (K : Type) [Field K]

/-- The three components of the polynomial counterexample.

The variables `X 0`, `X 1`, `X 2` correspond respectively to `x`, `y`, `z`. -/ def F : Fin 3 → MvPolynomial (Fin 3) K := ![ (1 + X 0 X 1) ^ 3 * X 2 + X 1 ^ 2 * (1 + X 0 * X 1) * (C 4 + C 3 * (X 0 * X 1)),

    X 1
      + C 3 * X 0 * (1 + X 0 * X 1) ^ 2 * X 2
      + C 3 * X 0 * X 1 ^ 2
          * (C 4 + C 3 * (X 0 * X 1)),

    C 2 * X 0
      - C 3 * X 0 ^ 2 * X 1
      - X 0 ^ 3 * X 2
  ]

/-- The formal Jacobian determinant of `F` is the constant polynomial `-2`. -/ theorem jacobianDet_F : jacobianDet (F K) = C (-2) := by simp only [ jacobianDet, jacobianMatrix, det_fin_three, of_apply, F, cons_val_zero, cons_val_one, cons_val_two, head_cons, tail_cons, map_add, map_sub, 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_neg, map_ofNat] ring

variable {K}

/-- The point `(0, 0, -1/4)` maps to `(-1/4, 0, 0)`. -/ theorem evalMap_F_p0 : evalMap (F K) ![0, 0, -(1 / 4)] = ![-(1 / 4), 0, 0] := by funext i fin_cases i <;> simp [evalMap, F]

/-- Provided `2 ≠ 0`, the point `(1, -3/2, 13/2)` also maps to `(-1/4, 0, 0)`. -/ theorem evalMap_F_p1 (h2 : (2 : K) ≠ 0) : evalMap (F K) ![1, -(3 / 2), 13 / 2] = ![-(1 / 4), 0, 0] := by have h4 : (4 : K) ≠ 0 := (by norm_num : (2 : K) * 2 = 4) ▸ mul_ne_zero h2 h2 funext i fin_cases i <;> simp [evalMap, F] <;> field_simp [h4] <;> ring

end JacobianCounterexample

open JacobianCounterexample

/-- The Jacobian determinant of the displayed map over `ℂ` is a unit. Indeed, it is the nonzero constant `-2`. -/ theorem F_jacobian_isUnit : IsUnit (jacobianDet (F ℂ)) := by rw [jacobianDet_F] exact (isUnit_iff_ne_zero.mpr (by norm_num : (-2 : ℂ) ≠ 0)).map C

/-- The polynomial map `F : ℂ³ → ℂ³` is not injective. -/ theorem F_not_injective : ¬ Injective (evalMap (F ℂ)) := by intro hInjective

  have hp :
      (![0, 0, -(1 / 4)] : Fin 3 → ℂ) =
        ![1, -(3 / 2), 13 / 2] :=
    hInjective
      ((evalMap_F_p0 (K := ℂ)).trans
        (evalMap_F_p1 (K := ℂ) (by norm_num)).symm)

  exact zero_ne_one (congrFun hp 0)

/-- The injectivity consequence of the dimension-three Jacobian conjecture is false over `ℂ`. -/ theorem unitJacobian_does_not_imply_injective : ¬ ∀ P : Fin 3 → MvPolynomial (Fin 3) ℂ, IsUnit (jacobianDet P) → Injective (evalMap P) := by intro h exact F_not_injective (h (F ℂ) F_jacobian_isUnit)

/-! We now formulate the polynomial-inverse version explicitly. -/

/-- Polynomial self-maps of affine three-space over `ℂ`. -/ abbrev PolyMap3 := Fin 3 → MvPolynomial (Fin 3) ℂ

/-- A polynomial map has a polynomial two-sided inverse, viewed as functions on `ℂ³`. -/ def HasPolynomialInverse (P : PolyMap3) : Prop := ∃ Q : PolyMap3, LeftInverse (evalMap Q) (evalMap P) ∧ RightInverse (evalMap Q) (evalMap P)

/-- The polynomial-inverse formulation of the Jacobian conjecture in dimension three. -/ def JacobianConjecture3 : Prop := ∀ P : PolyMap3, IsUnit (jacobianDet P) → HasPolynomialInverse P

/-- The Jacobian conjecture in dimension three is false. -/ theorem jacobianConjecture3_false : ¬ JacobianConjecture3 := by intro hJC unfold JacobianConjecture3 at hJC

  apply unitJacobian_does_not_imply_injective
  intro P hP

  rcases hJC P hP with ⟨Q, hleft, _⟩
  exact hleft.injective

#print axioms jacobianDet_F #print axioms F_not_injective #print axioms jacobianConjecture3_false