feat: add symplectic matrices have determinant 1 eval problem

LeanEval/LinearAlgebra/SymplecticDet.lean

@@ -0,0 +1,35 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace LinearAlgebra
+
+/-!
+# Symplectic matrices have determinant 1
+
+§39 of Oliver Knill's *Some Fundamental Theorems in Mathematics*. For any
+commutative ring `R` and `2n × 2n` symplectic matrix `A` over `R` (i.e.
+`A * J * Aᵀ = J` with `J = [[0, -I], [I, 0]]`), one has `det A = 1`.
+
+Taking determinants of `Aᵀ J A = J` only forces `(det A)² = 1`; the sign
+requires the Pfaffian argument (`det A = Pf(Aᵀ J A) / Pf(J) = 1`).
+
+mathlib has `Matrix.symplecticGroup l R` and proves `symplectic_det`
+(`IsUnit (det A)`) but the determinant-equals-one claim is an open TODO in
+`Mathlib/LinearAlgebra/SymplecticGroup.lean`. No formalization of the
+identity was found in any other proof assistant.
+-/
+
+open Matrix
+
+/-- **Symplectic matrices have determinant 1.** For any commutative ring `R`
+and `2n × 2n` symplectic matrix `A` over `R`, `A.det = 1`. -/
+@[eval_problem]
+theorem symplectic_matrix_det
+    {l R : Type*} [DecidableEq l] [Fintype l] [CommRing R]
+    {A : Matrix (l ⊕ l) (l ⊕ l) R} (_hA : A ∈ Matrix.symplecticGroup l R) :
+    A.det = 1 := by
+  sorry
+
+end LinearAlgebra
+end LeanEval

manifests/problems.toml

@@ -673,3 +673,14 @@ module = "LeanEval.Geometry.Uniformization"
 holes = ["uniformization"]
 submitter = "Junyan Xu"
 source = "John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, Chapter 1."
+
+[[problem]]
+id = "symplectic_matrix_det"
+title = "Symplectic matrices have determinant 1"
+test = false
+module = "LeanEval.LinearAlgebra.SymplecticDet"
+holes = ["symplectic_matrix_det"]
+submitter = "Kim Morrison"
+notes = "§39 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. For any commutative ring R and 2n × 2n symplectic matrix A over R (A * J * Aᵀ = J with J = [[0, -I], [I, 0]]), det A = 1. Taking determinants of AᵀJA = J only forces (det A)² = 1; the sign requires the Pfaffian argument. Mathlib has `Matrix.symplecticGroup` and proves `symplectic_det` (IsUnit (det A)) but the equals-1 claim is an explicit TODO in Mathlib/LinearAlgebra/SymplecticGroup.lean; no formalization of the identity was found in any other proof assistant."
+source = "Folklore (Pfaffian computation). Listed as §39 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Marked as an open TODO at the head of Mathlib/LinearAlgebra/SymplecticGroup.lean (rev 5450b53e5ddc)."
+informal_solution = "Apply the Pfaffian: for any 2n × 2n matrix M and antisymmetric 2n × 2n matrix Ω, Pf(Mᵀ Ω M) = det(M) · Pf(Ω). With Ω = J (so Pf(J) ≠ 0) and Aᵀ J A = J for A ∈ Sp_{2n}(R), one gets Pf(J) = det(A) · Pf(J), hence det A = 1. (This requires the Pfaffian for matrices over a commutative ring R; the construction is purely algebraic.)"