sympy verification: polynomial map C^3->C^3 with constant Jacobian -2, non-injective (3 distinct points -> (-1/4,0,0)), 3-to-1

verify.py

#!/usr/bin/env python3
"""
Verify the claimed properties of the polynomial map F: C^3 -> C^3

    F0 = (1+xy)^3 z + y^2 (1+xy)(4+3xy)
    F1 = y + 3x(1+xy)^2 z + 3x y^2 (4+3xy)
    F2 = 2x - 3x^2 y - x^3 z

Claims checked:
  1. det(Jacobian F) is the constant -2  (nonzero constant everywhere)
  2. three DISTINCT points map to the single point (-1/4, 0, 0)  -> not injective
  3. the generic fiber has 3 points          -> the map is 3-to-1

Requires: sympy  (pip install sympy)
"""
import sympy as sp

x, y, z = sp.symbols('x y z')
u = 1 + x*y            # the "1+xy" block
w = 4 + 3*x*y          # the "4+3xy" block

F0 = u**3 * z + y**2 * u * w
F1 = y + 3*x * u**2 * z + 3*x * y**2 * w
F2 = 2*x - 3*x**2 * y - x**3 * z
F = [F0, F1, F2]

print("Map (expanded):")
for name, f in zip("F0 F1 F2".split(), F):
    print(f"  {name} =", sp.expand(f))

# ---- Claim 1: Jacobian determinant is the constant -2 -----------------------
J = sp.Matrix([[sp.diff(f, v) for v in (x, y, z)] for f in F])
det = sp.expand(J.det())
P = sp.Poly(det, x, y, z)
print("\n[1] det(Jacobian) =", det,
      "| total degree =", P.total_degree(),
      "| #terms =", len(P.terms()))
assert det == -2 and P.total_degree() == 0, "determinant is NOT the constant -2"
print("    -> nonzero constant everywhere: PASS")

# ---- Claim 2: three distinct points share the image (-1/4, 0, 0) -----------
pts = [(0, 0, sp.Rational(-1, 4)),
       (1, sp.Rational(-3, 2), sp.Rational(13, 2)),
       (-1, sp.Rational(3, 2), sp.Rational(13, 2))]
target = (sp.Rational(-1, 4), 0, 0)

print("\n[2] images:")
for p in pts:
    sub = dict(zip((x, y, z), p))
    img = tuple(sp.simplify(f.subs(sub)) for f in F)
    print(f"    F{p} = {img}")
    assert img == target, f"{p} does not map to {target}"
assert len({p for p in pts}) == 3, "points are not distinct"
print("    -> 3 distinct points, same image: PASS (map is NOT injective)")

# ---- Claim 3: generic fiber size (map degree) ------------------------------
a, b, c = sp.Rational(7, 3), sp.Rational(-2, 5), sp.Rational(11, 4)  # generic target
fiber = sp.solve([F0 - a, F1 - b, F2 - c], [x, y, z], dict=True)
print(f"\n[3] preimages of generic point ({a},{b},{c}): count =", len(fiber))
print("    -> map is 3-to-1 generically: PASS" if len(fiber) == 3 else "    -> unexpected")

print("\nAll checks passed.")