The Maslov index of loops of linear symplectic maps through their graphs

Let E be a complex inner product space, with its standard symplectic form ω(x, y) = Im ⟪x, y⟫. A real-linear map Ψ : E → E preserving ω is a linear symplectic map. Its graph is a Lagrangian subspace of (E × E, -ω ⊕ ω), which is totally real for the complex structure (-i) ⊕ i. To read it as a maximal totally real subspace of a complex space we use a conjugation K of E, a real-linear automorphism anticommuting with i, such as coordinatewise conjugation on ℂⁿ: the map (u, w) ↦ (K u, w) is complex linear from (E, -i) × (E, i) to E × E, and carries the graph of Ψ to

conjGraph K Ψ = {(K z, Ψ z) | z ∈ E} (TauCeti.conjGraph).

Write P = Ψ.complexLinearPart for the complex-linear part of Ψ. The symplectic condition makes P invertible (ContinuousLinearMap.complexLinearPartEquiv). The complex-linear automorphism (u, w) ↦ (u, Q u + P w) of E × E, with Q = (Ψ ∘ K⁻¹).complexLinearPart, carries the conjugate graph of the identity onto the conjugate graph of Ψ (TauCeti.conjGraph_eq_map). The conjugate graph of the identity is maximal totally real, so a continuous loop Ψ of linear symplectic maps gives a loop of maximal totally real subspaces t ↦ conjGraph K (Ψ t) (TauCeti.symplecticGraphLoop), with frames given by these automorphisms. Its Maslov index is the Maslov index of the symplectic loop, normalized as by Robbin and Salamon through the graph.

The main theorem computes it: if det (P t) = |det (P t)| δ t for a loop δ in the circle, then

μ(t ↦ conjGraph K (Ψ t)) = 2 deg δ

(TauCeti.maslovIndex_symplecticGraphLoop). The proof deforms the frame (u, w) ↦ (u, s Q u + P w) to s = 0, where the loop is the conjugate graph of the identity moved by the automorphisms id × P t. Consequences:

• the index does not depend on the conjugation (TauCeti.maslovIndex_symplecticGraphLoop_congr_conj);
• composing with a loop U of complex-linear maps on either side adds 2 deg (det U) (TauCeti.maslovIndex_symplecticGraphLoop_comp_left, TauCeti.maslovIndex_symplecticGraphLoop_comp_right), which is how the index changes with a unitary trivialization;
• the full rotation t ↦ e^{2πit} of an n-dimensional space (TauCeti.rotationLoop) has index 2n (TauCeti.maslovIndex_symplecticGraphLoop_rotationLoop);
• homotopic loops of linear symplectic maps have the same index (TauCeti.maslovIndex_symplecticGraphLoop_eq_of_homotopy).

A loop δ as in the main theorem always exists (TauCeti.exists_path_det_complexLinearPart).

References

• J. Robbin and D. Salamon, The Maslov index for paths, Topology 32 (1993), 827–844, Section 4 (the Maslov index of symplectic paths through their graphs).
• D. McDuff and D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford University Press, 2017, Section 2.3 (the Maslov index of loops of symplectic matrices).

The graph loop of a loop of linear symplectic maps

noncomputable def TauCeti.symplecticGraphLoop {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (K : E ≃L[ℝ] E) (hK : ∀ (z : E), K (Complex.I • z) = -(Complex.I • K z)) (Ψ : ↑unitInterval → E →L[ℝ] E) (hΨ : Continuous Ψ) (hsymp : ∀ (t : ↑unitInterval) (x y : E), (inner ℂ ((Ψ t) x) ((Ψ t) y)).im = (inner ℂ x y).im) (hΨ01 : Ψ 0 = Ψ 1) : TotallyRealLoop (E × E)

The graph loop of a continuous loop Ψ of real-linear maps preserving the symplectic form Im ⟪·, ·⟫: the loop t ↦ conjGraph K (Ψ t) = {(K z, Ψ t z)} of maximal totally real subspaces of E × E, for a conjugation K. Its Maslov index is the Maslov index of the symplectic loop.

@[simp]

theorem TauCeti.symplecticGraphLoop_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] {K : E ≃L[ℝ] E} (hK : ∀ (z : E), K (Complex.I • z) = -(Complex.I • K z)) (Ψ : ↑unitInterval → E →L[ℝ] E) (hΨ : Continuous Ψ) (hsymp : ∀ (t : ↑unitInterval) (x y : E), (inner ℂ ((Ψ t) x) ((Ψ t) y)).im = (inner ℂ x y).im) (hΨ01 : Ψ 0 = Ψ 1) (t : ↑unitInterval) : ↑(symplecticGraphLoop K hK Ψ hΨ hsymp hΨ01) t = conjGraph K (Ψ t)

theorem TauCeti.maslovIndex_symplecticGraphLoop {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] {K : E ≃L[ℝ] E} (hK : ∀ (z : E), K (Complex.I • z) = -(Complex.I • K z)) (Ψ : ↑unitInterval → E →L[ℝ] E) (hΨ : Continuous Ψ) (hsymp : ∀ (t : ↑unitInterval) (x y : E), (inner ℂ ((Ψ t) x) ((Ψ t) y)).im = (inner ℂ x y).im) (hΨ01 : Ψ 0 = Ψ 1) {x : Circle} (δ : Path x x) (hδ : ∀ (t : ↑unitInterval), LinearMap.det ↑(Ψ t).complexLinearPart = ↑‖LinearMap.det ↑(Ψ t).complexLinearPart‖ * ↑(δ t)) : (symplecticGraphLoop K hK Ψ hΨ hsymp hΨ01).maslovIndex = 2 * Circle.degree δ

The Maslov index of a loop of linear symplectic maps. If the determinants of the complex-linear parts are det (P t) = |det (P t)| δ t for a loop δ in the circle, the graph loop has Maslov index 2 deg δ.

theorem TauCeti.exists_path_det_complexLinearPart {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] {Ψ : ↑unitInterval → E →L[ℝ] E} (hΨ : Continuous Ψ) (hsymp : ∀ (t : ↑unitInterval) (x y : E), (inner ℂ ((Ψ t) x) ((Ψ t) y)).im = (inner ℂ x y).im) (hΨ01 : Ψ 0 = Ψ 1) : ∃ (x : Circle) (δ : Path x x), ∀ (t : ↑unitInterval), LinearMap.det ↑(Ψ t).complexLinearPart = ↑‖LinearMap.det ↑(Ψ t).complexLinearPart‖ * ↑(δ t)

The complex-linear parts of a loop of linear symplectic maps have a loop δ of normalized determinants, det (P t) = |det (P t)| δ t, as asked for by TauCeti.maslovIndex_symplecticGraphLoop.

theorem TauCeti.maslovIndex_symplecticGraphLoop_congr_conj {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] {K : E ≃L[ℝ] E} (hK : ∀ (z : E), K (Complex.I • z) = -(Complex.I • K z)) {K' : E ≃L[ℝ] E} (hK' : ∀ (z : E), K' (Complex.I • z) = -(Complex.I • K' z)) (Ψ : ↑unitInterval → E →L[ℝ] E) (hΨ : Continuous Ψ) (hsymp : ∀ (t : ↑unitInterval) (x y : E), (inner ℂ ((Ψ t) x) ((Ψ t) y)).im = (inner ℂ x y).im) (hΨ01 : Ψ 0 = Ψ 1) : (symplecticGraphLoop K hK Ψ hΨ hsymp hΨ01).maslovIndex = (symplecticGraphLoop K' hK' Ψ hΨ hsymp hΨ01).maslovIndex

The Maslov index of the graph loop does not depend on the conjugation.

theorem TauCeti.maslovIndex_symplecticGraphLoop_comp_left {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] {K : E ≃L[ℝ] E} (hK : ∀ (z : E), K (Complex.I • z) = -(Complex.I • K z)) (Ψ : ↑unitInterval → E →L[ℝ] E) (hΨ : Continuous Ψ) (hsymp : ∀ (t : ↑unitInterval) (x y : E), (inner ℂ ((Ψ t) x) ((Ψ t) y)).im = (inner ℂ x y).im) (hΨ01 : Ψ 0 = Ψ 1) (U : ↑unitInterval → E →L[ℂ] E) (hUΨ : Continuous fun (t : ↑unitInterval) => ContinuousLinearMap.restrictScalars ℝ (U t) ∘SL Ψ t) (hsympU : ∀ (t : ↑unitInterval) (x y : E), (inner ℂ ((ContinuousLinearMap.restrictScalars ℝ (U t) ∘SL Ψ t) x) ((ContinuousLinearMap.restrictScalars ℝ (U t) ∘SL Ψ t) y)).im = (inner ℂ x y).im) (hUΨ01 : ContinuousLinearMap.restrictScalars ℝ (U 0) ∘SL Ψ 0 = ContinuousLinearMap.restrictScalars ℝ (U 1) ∘SL Ψ 1) {y : Circle} (δ : Path y y) (hδ : ∀ (t : ↑unitInterval), LinearMap.det ↑(U t) = ↑‖LinearMap.det ↑(U t)‖ * ↑(δ t)) : (symplecticGraphLoop K hK (fun (t : ↑unitInterval) => ContinuousLinearMap.restrictScalars ℝ (U t) ∘SL Ψ t) hUΨ hsympU hUΨ01).maslovIndex = (symplecticGraphLoop K hK Ψ hΨ hsymp hΨ01).maslovIndex + 2 * Circle.degree δ

Composing on the left with a loop of complex-linear maps. If U t ∘ Ψ t is again a loop of linear symplectic maps and det (U t) = |det (U t)| δ t, the Maslov index of the graph loop increases by 2 deg δ.

theorem TauCeti.maslovIndex_symplecticGraphLoop_comp_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] {K : E ≃L[ℝ] E} (hK : ∀ (z : E), K (Complex.I • z) = -(Complex.I • K z)) (Ψ : ↑unitInterval → E →L[ℝ] E) (hΨ : Continuous Ψ) (hsymp : ∀ (t : ↑unitInterval) (x y : E), (inner ℂ ((Ψ t) x) ((Ψ t) y)).im = (inner ℂ x y).im) (hΨ01 : Ψ 0 = Ψ 1) (U : ↑unitInterval → E →L[ℂ] E) (hΨU : Continuous fun (t : ↑unitInterval) => Ψ t ∘SL ContinuousLinearMap.restrictScalars ℝ (U t)) (hsympU : ∀ (t : ↑unitInterval) (x y : E), (inner ℂ ((Ψ t ∘SL ContinuousLinearMap.restrictScalars ℝ (U t)) x) ((Ψ t ∘SL ContinuousLinearMap.restrictScalars ℝ (U t)) y)).im = (inner ℂ x y).im) (hΨU01 : Ψ 0 ∘SL ContinuousLinearMap.restrictScalars ℝ (U 0) = Ψ 1 ∘SL ContinuousLinearMap.restrictScalars ℝ (U 1)) {y : Circle} (δ : Path y y) (hδ : ∀ (t : ↑unitInterval), LinearMap.det ↑(U t) = ↑‖LinearMap.det ↑(U t)‖ * ↑(δ t)) : (symplecticGraphLoop K hK (fun (t : ↑unitInterval) => Ψ t ∘SL ContinuousLinearMap.restrictScalars ℝ (U t)) hΨU hsympU hΨU01).maslovIndex = (symplecticGraphLoop K hK Ψ hΨ hsymp hΨ01).maslovIndex + 2 * Circle.degree δ

Composing on the right with a loop of complex-linear maps. If Ψ t ∘ U t is again a loop of linear symplectic maps and det (U t) = |det (U t)| δ t, the Maslov index of the graph loop increases by 2 deg δ.

theorem TauCeti.maslovIndex_symplecticGraphLoop_rotationLoop {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] {K : E ≃L[ℝ] E} (hK : ∀ (z : E), K (Complex.I • z) = -(Complex.I • K z)) : (symplecticGraphLoop K hK (rotationLoop E) ⋯ ⋯ ⋯).maslovIndex = 2 * ↑(Module.finrank ℂ E)

Normalization. The full rotation t ↦ e^{2πit} of a complex inner product space of dimension n has graph loop of Maslov index 2n.

theorem TauCeti.maslovIndex_symplecticGraphLoop_eq_of_homotopy {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] {K : E ≃L[ℝ] E} (hK : ∀ (z : E), K (Complex.I • z) = -(Complex.I • K z)) (Ψ : ↑unitInterval × ↑unitInterval → E →L[ℝ] E) (hΨ : Continuous Ψ) (hsymp : ∀ (p : ↑unitInterval × ↑unitInterval) (x y : E), (inner ℂ ((Ψ p) x) ((Ψ p) y)).im = (inner ℂ x y).im) (hΨ01 : ∀ (s : ↑unitInterval), Ψ (s, 0) = Ψ (s, 1)) : (symplecticGraphLoop K hK (fun (t : ↑unitInterval) => Ψ (0, t)) ⋯ ⋯ ⋯).maslovIndex = (symplecticGraphLoop K hK (fun (t : ↑unitInterval) => Ψ (1, t)) ⋯ ⋯ ⋯).maslovIndex

Homotopy invariance. Homotopic loops of linear symplectic maps, through closed loops of linear symplectic maps, have graph loops of the same Maslov index.