import Mathlib
noncomputable section
open Matrix Function
/-! # A counterexample to the Jacobian conjecture in dimension three
We formalize the polynomial map
F : ℂ³ → ℂ³
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
]
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)
/-! 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