Facts about Keller maps

Conjectura.Theorems.Mathematics.AlgebraicGeometry.KellerMap

/-
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.Defs.Mathematics.AlgebraicGeometry.KellerMap

/-! # Facts about Keller maps

## Source

Adapted for Conjectura from [formal-conjectures](https://github.com/google-deepmind/formal-conjectures) (Google DeepMind), `FormalConjectures/Wikipedia/JacobianConjecture.lean`. Split into one concept per module; no mathematical content changed.
-/

namespace Conjectura.AlgebraicGeometry

/-- The unit-determinant hypothesis really is "non-zero constant determinant" over a field.
A sanity theorem: it pins the formalization to the literature's statement. -/
theorem isKellerMap_iff_det_eq_C {k σ : Type} [Field k] [Fintype σ] [DecidableEq σ]
    (F : RegularFunction k σ σ) :
    IsKellerMap F ↔ (∃ c : k, c ≠ 0 ∧ F.Jacobian.det = MvPolynomial.C c) := by
  simp [IsKellerMap, MvPolynomial.isUnit_iff_eq_C_of_isReduced, isUnit_iff_ne_zero]

/-- Non-vacuity: the hypothesis is satisfiable, so the conjecture is not quantifying over an
empty class. -/
theorem isKellerMap_id {k σ : Type} [CommRing k] [Fintype σ] [DecidableEq σ] :
    IsKellerMap (RegularFunction.id k σ) := by
  suffices (RegularFunction.id k σ).Jacobian = 1 by simp [IsKellerMap, this]
  ext i j
  simp [RegularFunction.Jacobian, RegularFunction.id, Matrix.one_eq_pi_single]

end Conjectura.AlgebraicGeometry