Facts about Keller maps
isKellerMap_iff_det_eq_Ctheorem
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]isKellerMap_idtheorem
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]Builds on
import Conjectura.Theorems.Mathematics.AlgebraicGeometry.KellerMap · maintainer — open · raw source
Adapted for Conjectura from formal-conjectures (Google DeepMind), `FormalConjectures/Wikipedia/JacobianConjecture.lean`. Split into one concept per module; no mathematical content changed.
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