The complex-linear part of a symplectic matrix is invertible

Proved

ConleyZehnder.complexLinearDet_ne_zero

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

conley-zehnder-indexmaslov-indexsymplectic-geometrysymplectic-group

For every $A\in\mathrm{Sp}(2n)$ , the complex-linear part

C_A=\tfrac12\,(A-J_0AJ_0)=\begin{pmatrix}X&-Y\\Y&X\end{pmatrix}

is invertible as a complex matrix: $\det(X+iY)\neq0$ .

In particular $\hat\rho(A)=\det_{\mathbb C}C_A/|\det_{\mathbb C}C_A|$ is a well-defined point of $S^1$ for every symplectic $A$ .

Preamble

import Definitions.Def_ConleyZehnder_Setting

Formal statement

namespace ConleyZehnder

/-- Gutt, proof of Corollary 12: for every symplectic `A`, the `ℂ`-linear part
`½(A - J₀AJ₀)` is invertible, i.e. `det_ℂ C_A ≠ 0`. -/
theorem complexLinearDet_ne_zero {n : ℕ} (A : Mat n) (hA : IsSymplectic A) :
    complexLinearDet A ≠ 0 := by sorry

end ConleyZehnder

Source

Gutt, Generalized Conley-Zehnder index, Ann. Fac. Sci. Toulouse Math. 23 (2014) 907-932, https://doi.org/10.5802/afst.1430 (arXiv:1307.7239), proof of Corollary 12, p. 9 (formula (9)); Salamon, Lectures on Floer homology, IAS/Park City Math. Ser. 7 (1999) 143-229, https://doi.org/10.1090/pcms/007/05

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Throughout, for a natural number $n$ (including $n=0$ ), $\mathrm{Mat}_n$ denotes the real $2n\times 2n$ matrices whose rows and columns are indexed by two copies of $\{0,\dots,n-1\}$ : a first (" $q$ ") block and a second (" $p$ ") block. $\mathrm{Id}$ is the identity matrix. $J_0\in\mathrm{Mat}_n$ is the block matrix

J_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix}.

A matrix $A$ is called symplectic if $A\,J_0\,A^{\mathsf T}=J_0$ . A path is a continuous map $[0,1]\to\mathrm{Mat}_n$ (with the usual Euclidean topology on matrix entries); the set of paths carries the compact-open topology (equivalently the topology of uniform convergence). Products, inverses and transposes of paths below are always taken pointwise in $t$ . For $n=0$ all matrices are the empty $0\times 0$ matrix, whose determinant is $1$ .

For $A\in\mathrm{Mat}_n$ , let $C_A=\tfrac12(A-J_0AJ_0)$ , let $X$ be its upper-left ( $q$ -row, $q$ -column) $n\times n$ block and $Y$ its lower-left ( $p$ -row, $q$ -column) block, and let $d(A)=\det_{\mathbb C}(X+iY)$ be the determinant of the complex $n\times n$ matrix $X+iY$ .

Claim. For every $n\in\mathbb N$ and every symplectic $A\in\mathrm{Mat}_n$ (i.e. $AJ_0A^{\mathsf T}=J_0$ ),

d(A)\neq 0.

For $n=0$ the claim is $1\neq 0$ .

Human review

Endorsed by Shuze Chen · Oct 9, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph