FormalConjectures.Wikipedia.JacobianConjecture

FormalConjectures
Wikipedia
JacobianConjecture

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Jacobian conjecture

Reference: Wikipedia

namespace JacobianConjecturesection Conjectureopen MvPolynomial RegularFunctionvariable (k : Type*)name_poly_vars X, Y, Z over k

Alpöge/Fable's counterexample: a polynomial self-map of k³ with Jacobian determinant -2 which is not injective.

noncomputable abbrev F [CommRing k] : RegularFunction k (Fin 3) (Fin 3) :=
  ![(1 + X * Y)^3 * Z + Y ^ 2 * (1 + X * Y) * (4 + 3 * X * Y),
    Y + 3 * X * (1 + X * Y) ^ 2 * Z + 3 * X * Y ^ 2 * (4 + 3 * X * Y),
    2 * X - 3 * X ^ 2 * Y - X ^ 3 * Z]

A variant of Alpöge/Fable's counterexample: a polynomial self-map of k³ with Jacobian determinant 1 which is not injective.

noncomputable abbrev G [CommRing k] : RegularFunction k (Fin 3) (Fin 3) :=
  ![(1 + 2 * X * Y) ^ 3 * Z + 4 * Y ^ 2 * (1 + 2 * X * Y) * (2 + 3 * (X * Y)),
    Y + 3 * X * (1 + 2 * X * Y) ^ 2 * Z + 12 * X * Y ^ 2 * (2 + 3 * (X * Y)),
    -X + 3 * X ^ 2 * Y + X ^ 3 * Z]

@[category API, AMS 14]
lemma det_jacobian_F [CommRing k] : (F k).Jacobian.det = -2 := byk:Type u_1inst✝:CommRing k⊢ (F k).Jacobian.det = -2
  simp only [Jacobian, F, Fin.isValue, ← map_ofNat (C : k →+* MvPolynomial (Fin 3) k),
    Matrix.det_fin_three, Matrix.of_apply, Matrix.cons_val_zero, map_add, Derivation.leibniz,
    pderiv_X, ne_eq, Fin.reduceEq, not_false_eq_true, Pi.single_eq_of_ne, smul_eq_mul, mul_zero,
    Derivation.leibniz_pow, Nat.add_one_sub_one, Derivation.map_one_eq_zero, one_ne_zero,
    Pi.single_eq_same, mul_one, zero_add, nsmul_eq_mul, Nat.cast_ofNat, derivation_C, add_zero,
    pow_one,  Matrix.cons_val_one, zero_ne_one, Matrix.cons_val_two, Nat.succ_eq_add_one,
    Nat.reduceAdd, Matrix.tail_cons, Matrix.head_cons, map_sub, sub_self, zero_sub, mul_neg,
    sub_zero, neg_mul, sub_neg_eq_add]k:Type u_1inst✝:CommRing k⊢ -((Z * (C 3 * ((1 + X * Y) ^ 2 * Y)) + (Y ^ 2 * (1 + X * Y) * (Y * C 3) + (C 4 + C 3 * X * Y) * (Y ^ 2 * Y))) *
                  (1 + Z * (C 3 * X * (C 2 * ((1 + X * Y) * X))) +
                    (C 3 * X * Y ^ 2 * (C 3 * X) + (C 4 + C 3 * X * Y) * (C 3 * X * (C 2 * Y)))) *
                X ^ 3) +
            (Z * (C 3 * ((1 + X * Y) ^ 2 * Y)) +
                  (Y ^ 2 * (1 + X * Y) * (Y * C 3) + (C 4 + C 3 * X * Y) * (Y ^ 2 * Y))) *
                (C 3 * X ^ 2) *
              (C 3 * X * (1 + X * Y) ^ 2) +
          (Z * (C 3 * X * (C 2 * ((1 + X * Y) * Y)) + (1 + X * Y) ^ 2 * C 3) +
                (C 3 * X * Y ^ 2 * (Y * C 3) + (C 4 + C 3 * X * Y) * (Y ^ 2 * C 3))) *
              (Z * (C 3 * ((1 + X * Y) ^ 2 * X)) +
                (Y ^ 2 * (1 + X * Y) * (C 3 * X) + (C 4 + C 3 * X * Y) * (Y ^ 2 * X + (1 + X * Y) * (C 2 * Y)))) *
            X ^ 3 +
        -((Z * (C 3 * X * (C 2 * ((1 + X * Y) * Y)) + (1 + X * Y) ^ 2 * C 3) +
                (C 3 * X * Y ^ 2 * (Y * C 3) + (C 4 + C 3 * X * Y) * (Y ^ 2 * C 3))) *
              (C 3 * X ^ 2) *
            (1 + X * Y) ^ 3) +
      (C 2 - Y * (C 3 * (C 2 * X)) - Z * (C 3 * X ^ 2)) *
          (Z * (C 3 * ((1 + X * Y) ^ 2 * X)) +
            (Y ^ 2 * (1 + X * Y) * (C 3 * X) + (C 4 + C 3 * X * Y) * (Y ^ 2 * X + (1 + X * Y) * (C 2 * Y)))) *
        (C 3 * X * (1 + X * Y) ^ 2) -
    (C 2 - Y * (C 3 * (C 2 * X)) - Z * (C 3 * X ^ 2)) *
        (1 + Z * (C 3 * X * (C 2 * ((1 + X * Y) * X))) +
          (C 3 * X * Y ^ 2 * (C 3 * X) + (C 4 + C 3 * X * Y) * (C 3 * X * (C 2 * Y)))) *
      (1 + X * Y) ^ 3 =
  -C 2
  simp only [map_ofNat]k:Type u_1inst✝:CommRing k⊢ -((Z * (3 * ((1 + X * Y) ^ 2 * Y)) + (Y ^ 2 * (1 + X * Y) * (Y * 3) + (4 + 3 * X * Y) * (Y ^ 2 * Y))) *
                  (1 + Z * (3 * X * (2 * ((1 + X * Y) * X))) +
                    (3 * X * Y ^ 2 * (3 * X) + (4 + 3 * X * Y) * (3 * X * (2 * Y)))) *
                X ^ 3) +
            (Z * (3 * ((1 + X * Y) ^ 2 * Y)) + (Y ^ 2 * (1 + X * Y) * (Y * 3) + (4 + 3 * X * Y) * (Y ^ 2 * Y))) *
                (3 * X ^ 2) *
              (3 * X * (1 + X * Y) ^ 2) +
          (Z * (3 * X * (2 * ((1 + X * Y) * Y)) + (1 + X * Y) ^ 2 * 3) +
                (3 * X * Y ^ 2 * (Y * 3) + (4 + 3 * X * Y) * (Y ^ 2 * 3))) *
              (Z * (3 * ((1 + X * Y) ^ 2 * X)) +
                (Y ^ 2 * (1 + X * Y) * (3 * X) + (4 + 3 * X * Y) * (Y ^ 2 * X + (1 + X * Y) * (2 * Y)))) *
            X ^ 3 +
        -((Z * (3 * X * (2 * ((1 + X * Y) * Y)) + (1 + X * Y) ^ 2 * 3) +
                (3 * X * Y ^ 2 * (Y * 3) + (4 + 3 * X * Y) * (Y ^ 2 * 3))) *
              (3 * X ^ 2) *
            (1 + X * Y) ^ 3) +
      (2 - Y * (3 * (2 * X)) - Z * (3 * X ^ 2)) *
          (Z * (3 * ((1 + X * Y) ^ 2 * X)) +
            (Y ^ 2 * (1 + X * Y) * (3 * X) + (4 + 3 * X * Y) * (Y ^ 2 * X + (1 + X * Y) * (2 * Y)))) *
        (3 * X * (1 + X * Y) ^ 2) -
    (2 - Y * (3 * (2 * X)) - Z * (3 * X ^ 2)) *
        (1 + Z * (3 * X * (2 * ((1 + X * Y) * X))) + (3 * X * Y ^ 2 * (3 * X) + (4 + 3 * X * Y) * (3 * X * (2 * Y)))) *
      (1 + X * Y) ^ 3 =
  -2
  ringAll goals completed! 🐙

@[category API, AMS 14]
lemma det_jacobian_G [CommRing k] : (G k).Jacobian.det = 1 := byk:Type u_1inst✝:CommRing k⊢ (G k).Jacobian.det = 1
  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]k:Type u_1inst✝:CommRing k⊢ (↑3 * (1 + C 2 * X * Y) ^ (3 - 1) * (0 + ((0 * X + C 2 * 1) * Y + C 2 * X * 0)) * Z + (1 + C 2 * X * Y) ^ 3 * 0 +
                  (((0 * Y ^ 2 + C 4 * (↑2 * Y ^ (2 - 1) * 0)) * (1 + C 2 * X * Y) +
                        C 4 * Y ^ 2 * (0 + ((0 * X + C 2 * 1) * Y + C 2 * X * 0))) *
                      (C 2 + C 3 * (X * Y)) +
                    C 4 * Y ^ 2 * (1 + C 2 * X * Y) * (0 + (0 * (X * Y) + C 3 * (1 * Y + X * 0))))) *
                (1 +
                    (((0 * X + C 3 * 0) * (1 + C 2 * X * Y) ^ 2 +
                          C 3 * X * (↑2 * (1 + C 2 * X * Y) ^ (2 - 1) * (0 + ((0 * X + C 2 * 0) * Y + C 2 * X * 1)))) *
                        Z +
                      C 3 * X * (1 + C 2 * X * Y) ^ 2 * 0) +
                  (((0 * X + C 12 * 0) * Y ^ 2 + C 12 * X * (↑2 * Y ^ (2 - 1) * 1)) * (C 2 + C 3 * (X * Y)) +
                    C 12 * X * Y ^ 2 * (0 + (0 * (X * Y) + C 3 * (0 * Y + X * 1))))) *
              (-0 + ((0 * X ^ 2 + C 3 * (↑2 * X ^ (2 - 1) * 0)) * Y + C 3 * X ^ 2 * 0) +
                (↑3 * X ^ (3 - 1) * 0 * Z + X ^ 3 * 1)) -
            (↑3 * (1 + C 2 * X * Y) ^ (3 - 1) * (0 + ((0 * X + C 2 * 1) * Y + C 2 * X * 0)) * Z +
                    (1 + C 2 * X * Y) ^ 3 * 0 +
                  (((0 * Y ^ 2 + C 4 * (↑2 * Y ^ (2 - 1) * 0)) * (1 + C 2 * X * Y) +
                        C 4 * Y ^ 2 * (0 + ((0 * X + C 2 * 1) * Y + C 2 * X * 0))) *
                      (C 2 + C 3 * (X * Y)) +
                    C 4 * Y ^ 2 * (1 + C 2 * X * Y) * (0 + (0 * (X * Y) + C 3 * (1 * Y + X * 0))))) *
                (-0 + ((0 * X ^ 2 + C 3 * (↑2 * X ^ (2 - 1) * 0)) * Y + C 3 * X ^ 2 * 1) +
                  (↑3 * X ^ (3 - 1) * 0 * Z + X ^ 3 * 0)) *
              (0 +
                  (((0 * X + C 3 * 0) * (1 + C 2 * X * Y) ^ 2 +
                        C 3 * X * (↑2 * (1 + C 2 * X * Y) ^ (2 - 1) * (0 + ((0 * X + C 2 * 0) * Y + C 2 * X * 0)))) *
                      Z +
                    C 3 * X * (1 + C 2 * X * Y) ^ 2 * 1) +
                (((0 * X + C 12 * 0) * Y ^ 2 + C 12 * X * (↑2 * Y ^ (2 - 1) * 0)) * (C 2 + C 3 * (X * Y)) +
                  C 12 * X * Y ^ 2 * (0 + (0 * (X * Y) + C 3 * (0 * Y + X * 0))))) -
          (0 +
                  (((0 * X + C 3 * 1) * (1 + C 2 * X * Y) ^ 2 +
                        C 3 * X * (↑2 * (1 + C 2 * X * Y) ^ (2 - 1) * (0 + ((0 * X + C 2 * 1) * Y + C 2 * X * 0)))) *
                      Z +
                    C 3 * X * (1 + C 2 * X * Y) ^ 2 * 0) +
                (((0 * X + C 12 * 1) * Y ^ 2 + C 12 * X * (↑2 * Y ^ (2 - 1) * 0)) * (C 2 + C 3 * (X * Y)) +
                  C 12 * X * Y ^ 2 * (0 + (0 * (X * Y) + C 3 * (1 * Y + X * 0))))) *
              (↑3 * (1 + C 2 * X * Y) ^ (3 - 1) * (0 + ((0 * X + C 2 * 0) * Y + C 2 * X * 1)) * Z +
                  (1 + C 2 * X * Y) ^ 3 * 0 +
                (((0 * Y ^ 2 + C 4 * (↑2 * Y ^ (2 - 1) * 1)) * (1 + C 2 * X * Y) +
                      C 4 * Y ^ 2 * (0 + ((0 * X + C 2 * 0) * Y + C 2 * X * 1))) *
                    (C 2 + C 3 * (X * Y)) +
                  C 4 * Y ^ 2 * (1 + C 2 * X * Y) * (0 + (0 * (X * Y) + C 3 * (0 * Y + X * 1))))) *
            (-0 + ((0 * X ^ 2 + C 3 * (↑2 * X ^ (2 - 1) * 0)) * Y + C 3 * X ^ 2 * 0) +
              (↑3 * X ^ (3 - 1) * 0 * Z + X ^ 3 * 1)) +
        (0 +
                (((0 * X + C 3 * 1) * (1 + C 2 * X * Y) ^ 2 +
                      C 3 * X * (↑2 * (1 + C 2 * X * Y) ^ (2 - 1) * (0 + ((0 * X + C 2 * 1) * Y + C 2 * X * 0)))) *
                    Z +
                  C 3 * X * (1 + C 2 * X * Y) ^ 2 * 0) +
              (((0 * X + C 12 * 1) * Y ^ 2 + C 12 * X * (↑2 * Y ^ (2 - 1) * 0)) * (C 2 + C 3 * (X * Y)) +
                C 12 * X * Y ^ 2 * (0 + (0 * (X * Y) + C 3 * (1 * Y + X * 0))))) *
            (-0 + ((0 * X ^ 2 + C 3 * (↑2 * X ^ (2 - 1) * 0)) * Y + C 3 * X ^ 2 * 1) +
              (↑3 * X ^ (3 - 1) * 0 * Z + X ^ 3 * 0)) *
          (↑3 * (1 + C 2 * X * Y) ^ (3 - 1) * (0 + ((0 * X + C 2 * 0) * Y + C 2 * X * 0)) * Z +
              (1 + C 2 * X * Y) ^ 3 * 1 +
            (((0 * Y ^ 2 + C 4 * (↑2 * Y ^ (2 - 1) * 0)) * (1 + C 2 * X * Y) +
                  C 4 * Y ^ 2 * (0 + ((0 * X + C 2 * 0) * Y + C 2 * X * 0))) *
                (C 2 + C 3 * (X * Y)) +
              C 4 * Y ^ 2 * (1 + C 2 * X * Y) * (0 + (0 * (X * Y) + C 3 * (0 * Y + X * 0))))) +
      (-1 + ((0 * X ^ 2 + C 3 * (↑2 * X ^ (2 - 1) * 1)) * Y + C 3 * X ^ 2 * 0) +
            (↑3 * X ^ (3 - 1) * 1 * Z + X ^ 3 * 0)) *
          (↑3 * (1 + C 2 * X * Y) ^ (3 - 1) * (0 + ((0 * X + C 2 * 0) * Y + C 2 * X * 1)) * Z +
              (1 + C 2 * X * Y) ^ 3 * 0 +
            (((0 * Y ^ 2 + C 4 * (↑2 * Y ^ (2 - 1) * 1)) * (1 + C 2 * X * Y) +
                  C 4 * Y ^ 2 * (0 + ((0 * X + C 2 * 0) * Y + C 2 * X * 1))) *
                (C 2 + C 3 * (X * Y)) +
              C 4 * Y ^ 2 * (1 + C 2 * X * Y) * (0 + (0 * (X * Y) + C 3 * (0 * Y + X * 1))))) *
        (0 +
            (((0 * X + C 3 * 0) * (1 + C 2 * X * Y) ^ 2 +
                  C 3 * X * (↑2 * (1 + C 2 * X * Y) ^ (2 - 1) * (0 + ((0 * X + C 2 * 0) * Y + C 2 * X * 0)))) *
                Z +
              C 3 * X * (1 + C 2 * X * Y) ^ 2 * 1) +
          (((0 * X + C 12 * 0) * Y ^ 2 + C 12 * X * (↑2 * Y ^ (2 - 1) * 0)) * (C 2 + C 3 * (X * Y)) +
            C 12 * X * Y ^ 2 * (0 + (0 * (X * Y) + C 3 * (0 * Y + X * 0))))) -
    (-1 + ((0 * X ^ 2 + C 3 * (↑2 * X ^ (2 - 1) * 1)) * Y + C 3 * X ^ 2 * 0) + (↑3 * X ^ (3 - 1) * 1 * Z + X ^ 3 * 0)) *
        (1 +
            (((0 * X + C 3 * 0) * (1 + C 2 * X * Y) ^ 2 +
                  C 3 * X * (↑2 * (1 + C 2 * X * Y) ^ (2 - 1) * (0 + ((0 * X + C 2 * 0) * Y + C 2 * X * 1)))) *
                Z +
              C 3 * X * (1 + C 2 * X * Y) ^ 2 * 0) +
          (((0 * X + C 12 * 0) * Y ^ 2 + C 12 * X * (↑2 * Y ^ (2 - 1) * 1)) * (C 2 + C 3 * (X * Y)) +
            C 12 * X * Y ^ 2 * (0 + (0 * (X * Y) + C 3 * (0 * Y + X * 1))))) *
      (↑3 * (1 + C 2 * X * Y) ^ (3 - 1) * (0 + ((0 * X + C 2 * 0) * Y + C 2 * X * 0)) * Z + (1 + C 2 * X * Y) ^ 3 * 1 +
        (((0 * Y ^ 2 + C 4 * (↑2 * Y ^ (2 - 1) * 0)) * (1 + C 2 * X * Y) +
              C 4 * Y ^ 2 * (0 + ((0 * X + C 2 * 0) * Y + C 2 * X * 0))) *
            (C 2 + C 3 * (X * Y)) +
          C 4 * Y ^ 2 * (1 + C 2 * X * Y) * (0 + (0 * (X * Y) + C 3 * (0 * Y + X * 0))))) =
  1
  simp only [map_ofNat]k:Type u_1inst✝:CommRing k⊢ (↑3 * (1 + 2 * X * Y) ^ (3 - 1) * (0 + ((0 * X + 2 * 1) * Y + 2 * X * 0)) * Z + (1 + 2 * X * Y) ^ 3 * 0 +
                  (((0 * Y ^ 2 + 4 * (↑2 * Y ^ (2 - 1) * 0)) * (1 + 2 * X * Y) +
                        4 * Y ^ 2 * (0 + ((0 * X + 2 * 1) * Y + 2 * X * 0))) *
                      (2 + 3 * (X * Y)) +
                    4 * Y ^ 2 * (1 + 2 * X * Y) * (0 + (0 * (X * Y) + 3 * (1 * Y + X * 0))))) *
                (1 +
                    (((0 * X + 3 * 0) * (1 + 2 * X * Y) ^ 2 +
                          3 * X * (↑2 * (1 + 2 * X * Y) ^ (2 - 1) * (0 + ((0 * X + 2 * 0) * Y + 2 * X * 1)))) *
                        Z +
                      3 * X * (1 + 2 * X * Y) ^ 2 * 0) +
                  (((0 * X + 12 * 0) * Y ^ 2 + 12 * X * (↑2 * Y ^ (2 - 1) * 1)) * (2 + 3 * (X * Y)) +
                    12 * X * Y ^ 2 * (0 + (0 * (X * Y) + 3 * (0 * Y + X * 1))))) *
              (-0 + ((0 * X ^ 2 + 3 * (↑2 * X ^ (2 - 1) * 0)) * Y + 3 * X ^ 2 * 0) +
                (↑3 * X ^ (3 - 1) * 0 * Z + X ^ 3 * 1)) -
            (↑3 * (1 + 2 * X * Y) ^ (3 - 1) * (0 + ((0 * X + 2 * 1) * Y + 2 * X * 0)) * Z + (1 + 2 * X * Y) ^ 3 * 0 +
                  (((0 * Y ^ 2 + 4 * (↑2 * Y ^ (2 - 1) * 0)) * (1 + 2 * X * Y) +
                        4 * Y ^ 2 * (0 + ((0 * X + 2 * 1) * Y + 2 * X * 0))) *
                      (2 + 3 * (X * Y)) +
                    4 * Y ^ 2 * (1 + 2 * X * Y) * (0 + (0 * (X * Y) + 3 * (1 * Y + X * 0))))) *
                (-0 + ((0 * X ^ 2 + 3 * (↑2 * X ^ (2 - 1) * 0)) * Y + 3 * X ^ 2 * 1) +
                  (↑3 * X ^ (3 - 1) * 0 * Z + X ^ 3 * 0)) *
              (0 +
                  (((0 * X + 3 * 0) * (1 + 2 * X * Y) ^ 2 +
                        3 * X * (↑2 * (1 + 2 * X * Y) ^ (2 - 1) * (0 + ((0 * X + 2 * 0) * Y + 2 * X * 0)))) *
                      Z +
                    3 * X * (1 + 2 * X * Y) ^ 2 * 1) +
                (((0 * X + 12 * 0) * Y ^ 2 + 12 * X * (↑2 * Y ^ (2 - 1) * 0)) * (2 + 3 * (X * Y)) +
                  12 * X * Y ^ 2 * (0 + (0 * (X * Y) + 3 * (0 * Y + X * 0))))) -
          (0 +
                  (((0 * X + 3 * 1) * (1 + 2 * X * Y) ^ 2 +
                        3 * X * (↑2 * (1 + 2 * X * Y) ^ (2 - 1) * (0 + ((0 * X + 2 * 1) * Y + 2 * X * 0)))) *
                      Z +
                    3 * X * (1 + 2 * X * Y) ^ 2 * 0) +
                (((0 * X + 12 * 1) * Y ^ 2 + 12 * X * (↑2 * Y ^ (2 - 1) * 0)) * (2 + 3 * (X * Y)) +
                  12 * X * Y ^ 2 * (0 + (0 * (X * Y) + 3 * (1 * Y + X * 0))))) *
              (↑3 * (1 + 2 * X * Y) ^ (3 - 1) * (0 + ((0 * X + 2 * 0) * Y + 2 * X * 1)) * Z + (1 + 2 * X * Y) ^ 3 * 0 +
                (((0 * Y ^ 2 + 4 * (↑2 * Y ^ (2 - 1) * 1)) * (1 + 2 * X * Y) +
                      4 * Y ^ 2 * (0 + ((0 * X + 2 * 0) * Y + 2 * X * 1))) *
                    (2 + 3 * (X * Y)) +
                  4 * Y ^ 2 * (1 + 2 * X * Y) * (0 + (0 * (X * Y) + 3 * (0 * Y + X * 1))))) *
            (-0 + ((0 * X ^ 2 + 3 * (↑2 * X ^ (2 - 1) * 0)) * Y + 3 * X ^ 2 * 0) +
              (↑3 * X ^ (3 - 1) * 0 * Z + X ^ 3 * 1)) +
        (0 +
                (((0 * X + 3 * 1) * (1 + 2 * X * Y) ^ 2 +
                      3 * X * (↑2 * (1 + 2 * X * Y) ^ (2 - 1) * (0 + ((0 * X + 2 * 1) * Y + 2 * X * 0)))) *
                    Z +
                  3 * X * (1 + 2 * X * Y) ^ 2 * 0) +
              (((0 * X + 12 * 1) * Y ^ 2 + 12 * X * (↑2 * Y ^ (2 - 1) * 0)) * (2 + 3 * (X * Y)) +
                12 * X * Y ^ 2 * (0 + (0 * (X * Y) + 3 * (1 * Y + X * 0))))) *
            (-0 + ((0 * X ^ 2 + 3 * (↑2 * X ^ (2 - 1) * 0)) * Y + 3 * X ^ 2 * 1) +
              (↑3 * X ^ (3 - 1) * 0 * Z + X ^ 3 * 0)) *
          (↑3 * (1 + 2 * X * Y) ^ (3 - 1) * (0 + ((0 * X + 2 * 0) * Y + 2 * X * 0)) * Z + (1 + 2 * X * Y) ^ 3 * 1 +
            (((0 * Y ^ 2 + 4 * (↑2 * Y ^ (2 - 1) * 0)) * (1 + 2 * X * Y) +
                  4 * Y ^ 2 * (0 + ((0 * X + 2 * 0) * Y + 2 * X * 0))) *
                (2 + 3 * (X * Y)) +
              4 * Y ^ 2 * (1 + 2 * X * Y) * (0 + (0 * (X * Y) + 3 * (0 * Y + X * 0))))) +
      (-1 + ((0 * X ^ 2 + 3 * (↑2 * X ^ (2 - 1) * 1)) * Y + 3 * X ^ 2 * 0) + (↑3 * X ^ (3 - 1) * 1 * Z + X ^ 3 * 0)) *
          (↑3 * (1 + 2 * X * Y) ^ (3 - 1) * (0 + ((0 * X + 2 * 0) * Y + 2 * X * 1)) * Z + (1 + 2 * X * Y) ^ 3 * 0 +
            (((0 * Y ^ 2 + 4 * (↑2 * Y ^ (2 - 1) * 1)) * (1 + 2 * X * Y) +
                  4 * Y ^ 2 * (0 + ((0 * X + 2 * 0) * Y + 2 * X * 1))) *
                (2 + 3 * (X * Y)) +
              4 * Y ^ 2 * (1 + 2 * X * Y) * (0 + (0 * (X * Y) + 3 * (0 * Y + X * 1))))) *
        (0 +
            (((0 * X + 3 * 0) * (1 + 2 * X * Y) ^ 2 +
                  3 * X * (↑2 * (1 + 2 * X * Y) ^ (2 - 1) * (0 + ((0 * X + 2 * 0) * Y + 2 * X * 0)))) *
                Z +
              3 * X * (1 + 2 * X * Y) ^ 2 * 1) +
          (((0 * X + 12 * 0) * Y ^ 2 + 12 * X * (↑2 * Y ^ (2 - 1) * 0)) * (2 + 3 * (X * Y)) +
            12 * X * Y ^ 2 * (0 + (0 * (X * Y) + 3 * (0 * Y + X * 0))))) -
    (-1 + ((0 * X ^ 2 + 3 * (↑2 * X ^ (2 - 1) * 1)) * Y + 3 * X ^ 2 * 0) + (↑3 * X ^ (3 - 1) * 1 * Z + X ^ 3 * 0)) *
        (1 +
            (((0 * X + 3 * 0) * (1 + 2 * X * Y) ^ 2 +
                  3 * X * (↑2 * (1 + 2 * X * Y) ^ (2 - 1) * (0 + ((0 * X + 2 * 0) * Y + 2 * X * 1)))) *
                Z +
              3 * X * (1 + 2 * X * Y) ^ 2 * 0) +
          (((0 * X + 12 * 0) * Y ^ 2 + 12 * X * (↑2 * Y ^ (2 - 1) * 1)) * (2 + 3 * (X * Y)) +
            12 * X * Y ^ 2 * (0 + (0 * (X * Y) + 3 * (0 * Y + X * 1))))) *
      (↑3 * (1 + 2 * X * Y) ^ (3 - 1) * (0 + ((0 * X + 2 * 0) * Y + 2 * X * 0)) * Z + (1 + 2 * X * Y) ^ 3 * 1 +
        (((0 * Y ^ 2 + 4 * (↑2 * Y ^ (2 - 1) * 0)) * (1 + 2 * X * Y) +
              4 * Y ^ 2 * (0 + ((0 * X + 2 * 0) * Y + 2 * X * 0))) *
            (2 + 3 * (X * Y)) +
          4 * Y ^ 2 * (1 + 2 * X * Y) * (0 + (0 * (X * Y) + 3 * (0 * Y + X * 0))))) =
  1
  ringAll goals completed! 🐙

F identifies the two distinct points (0, 0, -1/4) and (1, -3/2, 13/2).

@[category API, AMS 14]
lemma aeval_F_eq [Field k] [CharZero k] :
    (F k).aeval ![(0 : k), 0, -1/4] = (F k).aeval ![(1 : k), -3/2, 13/2]  := byk:Type u_1inst✝¹:Field kinst✝:CharZero k⊢ (F k).aeval ![0, 0, -1 / 4] = (F k).aeval ![1, -3 / 2, 13 / 2]
  funext ik:Type u_1inst✝¹:Field kinst✝:CharZero ki:Fin 3⊢ (F k).aeval ![0, 0, -1 / 4] i = (F k).aeval ![1, -3 / 2, 13 / 2] i
  fin_cases i«0»k:Type u_1inst✝¹:Field kinst✝:CharZero k⊢ (F k).aeval ![0, 0, -1 / 4] ((fun i ↦ i) ⟨0, ⋯⟩) = (F k).aeval ![1, -3 / 2, 13 / 2] ((fun i ↦ i) ⟨0, ⋯⟩)«1»k:Type u_1inst✝¹:Field kinst✝:CharZero k⊢ (F k).aeval ![0, 0, -1 / 4] ((fun i ↦ i) ⟨1, ⋯⟩) = (F k).aeval ![1, -3 / 2, 13 / 2] ((fun i ↦ i) ⟨1, ⋯⟩)«2»k:Type u_1inst✝¹:Field kinst✝:CharZero k⊢ (F k).aeval ![0, 0, -1 / 4] ((fun i ↦ i) ⟨2, ⋯⟩) = (F k).aeval ![1, -3 / 2, 13 / 2] ((fun i ↦ i) ⟨2, ⋯⟩) <;>«0»k:Type u_1inst✝¹:Field kinst✝:CharZero k⊢ (F k).aeval ![0, 0, -1 / 4] ((fun i ↦ i) ⟨0, ⋯⟩) = (F k).aeval ![1, -3 / 2, 13 / 2] ((fun i ↦ i) ⟨0, ⋯⟩)«1»k:Type u_1inst✝¹:Field kinst✝:CharZero k⊢ (F k).aeval ![0, 0, -1 / 4] ((fun i ↦ i) ⟨1, ⋯⟩) = (F k).aeval ![1, -3 / 2, 13 / 2] ((fun i ↦ i) ⟨1, ⋯⟩)«2»k:Type u_1inst✝¹:Field kinst✝:CharZero k⊢ (F k).aeval ![0, 0, -1 / 4] ((fun i ↦ i) ⟨2, ⋯⟩) = (F k).aeval ![1, -3 / 2, 13 / 2] ((fun i ↦ i) ⟨2, ⋯⟩) simp [RegularFunction.aeval]«2»k:Type u_1inst✝¹:Field kinst✝:CharZero k⊢ 0 = 2 - 3 * (-3 / 2) - 13 / 2 <;>«0»k:Type u_1inst✝¹:Field kinst✝:CharZero k⊢ -1 / 4 = (1 + -3 / 2) ^ 3 * (13 / 2) + (-3 / 2) ^ 2 * (1 + -3 / 2) * (4 + 3 * (-3 / 2))«1»k:Type u_1inst✝¹:Field kinst✝:CharZero k⊢ 0 = -3 / 2 + 3 * (1 + -3 / 2) ^ 2 * (13 / 2) + 3 * (-3 / 2) ^ 2 * (4 + 3 * (-3 / 2))«2»k:Type u_1inst✝¹:Field kinst✝:CharZero k⊢ 0 = 2 - 3 * (-3 / 2) - 13 / 2 grindAll goals completed! 🐙

G identifies the two distinct points (1, 0, 1) and (0, 3, -71).

@[category API, AMS 14]
lemma aeval_G_eq [CommRing k] :
    (G k).aeval ![1, 0, (1 : k)] = (G k).aeval ![0, 3, -71] := byk:Type u_1inst✝:CommRing k⊢ (G k).aeval ![1, 0, 1] = (G k).aeval ![0, 3, -71]
  funext ik:Type u_1inst✝:CommRing ki:Fin 3⊢ (G k).aeval ![1, 0, 1] i = (G k).aeval ![0, 3, -71] i
  fin_cases i«0»k:Type u_1inst✝:CommRing k⊢ (G k).aeval ![1, 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) = (G k).aeval ![0, 3, -71] ((fun i ↦ i) ⟨0, ⋯⟩)«1»k:Type u_1inst✝:CommRing k⊢ (G k).aeval ![1, 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) = (G k).aeval ![0, 3, -71] ((fun i ↦ i) ⟨1, ⋯⟩)«2»k:Type u_1inst✝:CommRing k⊢ (G k).aeval ![1, 0, 1] ((fun i ↦ i) ⟨2, ⋯⟩) = (G k).aeval ![0, 3, -71] ((fun i ↦ i) ⟨2, ⋯⟩) <;>«0»k:Type u_1inst✝:CommRing k⊢ (G k).aeval ![1, 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) = (G k).aeval ![0, 3, -71] ((fun i ↦ i) ⟨0, ⋯⟩)«1»k:Type u_1inst✝:CommRing k⊢ (G k).aeval ![1, 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) = (G k).aeval ![0, 3, -71] ((fun i ↦ i) ⟨1, ⋯⟩)«2»k:Type u_1inst✝:CommRing k⊢ (G k).aeval ![1, 0, 1] ((fun i ↦ i) ⟨2, ⋯⟩) = (G k).aeval ![0, 3, -71] ((fun i ↦ i) ⟨2, ⋯⟩) simp [RegularFunction.aeval]All goals completed! 🐙; grindAll goals completed! 🐙

The predicate that the Jacobian conjecture holds for a given field and variable index type (i.e. number of variables).

def JacobianConjectureProp (k σ : Type*) [CommRing k] [Fintype σ] [DecidableEq σ] : Prop :=
  ∀ (F : RegularFunction k σ σ), IsUnit F.Jacobian.det →
    ∃ (G : RegularFunction k σ σ), G.comp F = id k σ ∧
    F.comp G = id k σ

set_option linter.style.answer_attribute false in

The Jacobian Conjecture: any regular function (i.e. vector valued polynomial function from) kⁿ → kᵐ whose Jacobian is a non-zero constant has an inverse that is given by a regular function, where k is a field of characteristic 0.

This is false: F has Jacobian determinant 1 but identifies two distinct points, so it admits no inverse. This counterexample works in all characteristics.


@[category research solved, AMS 14]
theorem jacobian_conjecture {k : Type} [CommRing k] [Nontrivial k] :
    answer(False) ↔ ∀ {σ : Type} [Fintype σ] [DecidableEq σ], JacobianConjectureProp k σ := byk:Typeinst✝¹:CommRing kinst✝:Nontrivial k⊢ False ↔ ∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σ
  rw [false_iffk:Typeinst✝¹:CommRing kinst✝:Nontrivial k⊢ ¬∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σk:Typeinst✝¹:CommRing kinst✝:Nontrivial k⊢ ¬∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σ]k:Typeinst✝¹:CommRing kinst✝:Nontrivial k⊢ ¬∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σ
  intro hk:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σ⊢ False
  obtain ⟨H, -, hGH⟩ := h (G k) (det_jacobian_G k ▸ isUnit_one)k:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)⊢ False
  have hleft : Function.LeftInverse (H.aeval (S₁ := k)) ((G k).aeval) := fun a => byk:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)a:Fin 3 → k⊢ H.aeval ((G k).aeval a) = ak:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)hleft:Function.LeftInverse H.aeval (G k).aeval⊢ False
    rw [← RegularFunction.comp_aeval,k:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)a:Fin 3 → k⊢ ((G k).comp H).aeval a = ak:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)a:Fin 3 → k⊢ (RegularFunction.id k (Fin 3)).aeval a = ak:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)hleft:Function.LeftInverse H.aeval (G k).aeval⊢ False hGHk:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)a:Fin 3 → k⊢ (RegularFunction.id k (Fin 3)).aeval a = ak:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)a:Fin 3 → k⊢ (RegularFunction.id k (Fin 3)).aeval a = ak:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)hleft:Function.LeftInverse H.aeval (G k).aeval⊢ False]k:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)a:Fin 3 → k⊢ (RegularFunction.id k (Fin 3)).aeval a = ak:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)hleft:Function.LeftInverse H.aeval (G k).aeval⊢ False
    funext tk:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)a:Fin 3 → kt:Fin 3⊢ (RegularFunction.id k (Fin 3)).aeval a t = a tk:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)hleft:Function.LeftInverse H.aeval (G k).aeval⊢ False
    simp [RegularFunction.aeval, RegularFunction.id]k:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)hleft:Function.LeftInverse H.aeval (G k).aeval⊢ Falsek:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)hleft:Function.LeftInverse H.aeval (G k).aeval⊢ False
  have h1 : (1 : k) = 0 := congrFun (hleft.injective (aeval_G_eq k)) 0k:Typeinst✝¹:CommRing kinst✝:Nontrivial kh:∀ {σ : Type} [inst : Fintype σ] [inst_1 : DecidableEq σ], JacobianConjectureProp k σH:RegularFunction k (Fin 3) (Fin 3)hGH:(G k).comp H = RegularFunction.id k (Fin 3)hleft:Function.LeftInverse H.aeval (G k).aevalh1:1 = 0⊢ False
  norm_num at h1All goals completed! 🐙

Does the Jacobian conjecture hold in the two variable case?

@[category research open, AMS 14]
theorem jacobian_conjecture_two_variables :
    answer(sorry) ↔ ∀ {k : Type} [Field k] [CharZero k], JacobianConjectureProp k (Fin 2) := by⊢ True ↔ ∀ {k : Type} [inst : Field k] [CharZero k], JacobianConjectureProp k (Fin 2)
  sorryAll goals completed! 🐙

end Conjecturesection Testsopen MvPolynomial RegularFunctionvariable {k σ : Type} [Fintype σ] [DecidableEq σ] [Field k]

-- Let's check that we've stated the "invertible Jacobian" condition correctly
-- by proving an equivalence
@[category API, AMS 14]
lemma sanity_check_condition_1 (F : RegularFunction k σ σ) :
    IsUnit F.Jacobian.det ↔ (∃ (c : k), c ≠ 0 ∧ F.Jacobian.det = .C c) := byk:Typeσ:Typeinst✝²:Fintype σinst✝¹:DecidableEq σinst✝:Field kF:RegularFunction k σ σ⊢ IsUnit F.Jacobian.det ↔ ∃ c, c ≠ 0 ∧ F.Jacobian.det = C c
  simp [MvPolynomial.isUnit_iff_eq_C_of_isReduced, isUnit_iff_ne_zero]All goals completed! 🐙



-- Let's apply the conjecture to a trivial case to make sure things
-- are working as expected.
@[category test, AMS 14]
theorem jacobian_conjecture_identity (H : JacobianConjectureProp k σ) :
    ∃ (G : RegularFunction k σ σ), G.comp (id k σ) = id k σ ∧
    (id k σ).comp G = id k σ := byk:Typeσ:Typeinst✝²:Fintype σinst✝¹:DecidableEq σinst✝:Field kH:JacobianConjectureProp k σ⊢ ∃ G, G.comp (RegularFunction.id k σ) = RegularFunction.id k σ ∧ (RegularFunction.id k σ).comp G = RegularFunction.id k σ
  apply Hk:Typeσ:Typeinst✝²:Fintype σinst✝¹:DecidableEq σinst✝:Field kH:JacobianConjectureProp k σ⊢ IsUnit (RegularFunction.id k σ).Jacobian.det
  suffices (RegularFunction.id k σ).Jacobian = 1 byk:Typeσ:Typeinst✝²:Fintype σinst✝¹:DecidableEq σinst✝:Field kH:JacobianConjectureProp k σthis:(RegularFunction.id k σ).Jacobian = 1⊢ IsUnit (RegularFunction.id k σ).Jacobian.detk:Typeσ:Typeinst✝²:Fintype σinst✝¹:DecidableEq σinst✝:Field kH:JacobianConjectureProp k σ⊢ (RegularFunction.id k σ).Jacobian = 1 simp [this, isUnit_one, Matrix.det_one]k:Typeσ:Typeinst✝²:Fintype σinst✝¹:DecidableEq σinst✝:Field kH:JacobianConjectureProp k σ⊢ (RegularFunction.id k σ).Jacobian = 1k:Typeσ:Typeinst✝²:Fintype σinst✝¹:DecidableEq σinst✝:Field kH:JacobianConjectureProp k σ⊢ (RegularFunction.id k σ).Jacobian = 1
  ext i jk:Typeσ:Typeinst✝²:Fintype σinst✝¹:DecidableEq σinst✝:Field kH:JacobianConjectureProp k σi:σj:σm✝:σ →₀ ℕ⊢ coeff m✝ ((RegularFunction.id k σ).Jacobian i j) = coeff m✝ (1 i j)
  simp [RegularFunction.Jacobian, RegularFunction.id, Matrix.one_eq_pi_single]All goals completed! 🐙

end Testsend JacobianConjecture