Prove2Me

Points of Sp∗(2n)\mathrm{Sp}^*(2n) with the same sign of det⁡(Id−A)\det(\mathrm{Id}-A) lie in one path component

Proved
CauchyRiemannIndex.spStar_joinedIn_of_sign_det_eq

by Mazecto · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

cauchy-riemannconley-zehnder-indexsymplectic-geometry

Let Sp∗(2n)={A∈Sp(2n,R):det⁡(Id−A)≠0}\mathrm{Sp}^*(2n)=\{A\in\mathrm{Sp}(2n,\mathbb R):\det(\mathrm{Id}-A)\neq0\} be the set of symplectic matrices without eigenvalue 11. If A,B∈Sp∗(2n)A,B\in\mathrm{Sp}^*(2n) satisfy

sign⁡det⁡(Id−A)=sign⁡det⁡(Id−B),\operatorname{sign}\det(\mathrm{Id}-A)=\operatorname{sign}\det(\mathrm{Id}-B),

then AA and BB are joined by a continuous path in Sp∗(2n)\mathrm{Sp}^*(2n).

Since det⁡(Id−⋅)\det(\mathrm{Id}-\cdot) has constant sign on each path component of Sp∗(2n)\mathrm{Sp}^*(2n), this shows that Sp∗(2n)\mathrm{Sp}^*(2n) has at most two path components, distinguished by that sign (Gutt, §2; Wendl, Lecture 3, §3.4).

Formalization Note. R2n×2n\mathbb R^{2n\times2n} is Mat n (real matrices indexed by Fin n ⊕ Fin n) and J0=(0−IdId0)J_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix} is Matrix.J; IsSymplectic A is membership in Matrix.symplecticGroup. Sp∗(2n)\mathrm{Sp}^*(2n) is SpStar n from the setting definitions, the sign is Real.sign, and the conclusion is JoinedIn (SpStar n) A B.

Preamble
import Definitions.Def_CauchyRiemannIndex_Setting
import Mathlib.Topology.Connected.PathConnected
import Mathlib.Data.Real.Sign
Formal statement
namespace CauchyRiemannIndex

open Matrix

/-- Two symplectic matrices without eigenvalue `1` whose values of `det(1 - ·)` have the same
sign lie in the same path component of `Sp*`. -/
theorem spStar_joinedIn_of_sign_det_eq (n : ℕ) (A B : Mat n) (hA : A ∈ SpStar n)
    (hB : B ∈ SpStar n) (h : Real.sign (1 - A).det = Real.sign (1 - B).det) :
    JoinedIn (SpStar n) A B := by
  sorry

end CauchyRiemannIndex
Source
C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 3, §3.4, p. 62; J. Gutt, Generalized Conley-Zehnder index, Ann. Fac. Sci. Toulouse 23 (2014), arXiv:1307.7239, §2 (the map ρ^\hat\rho, eq. (9))

View graph