I wish you'd share some conversations from experienced programmers too. How do they ask questions?

It's fun if you ask ChatGPT to guess the identity of its interlocutor :) It will guess math researcher or paper author without hints, but if you give it some additional hints, "this was shared over the internet", "it's someone willing to work with AI", it will guess Terence Tao as the first choice.

Never meet your heros.

Sense of vertigo that this is the same AI that plans meals and recommends movies for me. Incredible range.

Anybody have a cache/mirror of this? This is blocked by a corporate firewall... sigh

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

[flagged]

[dead]