The Maslov index of a loop moved by a loop of automorphisms

Let Λ be a loop of maximal totally real subspaces of a finite-dimensional complex normed space E and B a loop of complex-linear automorphisms of E. The pointwise image t ↦ B t (Λ t) (TauCeti.TotallyRealLoop.map) is again such a loop, and its Maslov index is

μ(B Λ) = μ(Λ) + 2 deg (det B),

where deg (det B) is the winding number of the loop of determinants, read as the degree of the circle loop t ↦ det (B t) / ‖det (B t)‖ of normalized determinants (ContinuousLinearEquiv.normalizedDet, TauCeti.TotallyRealLoop.maslovIndex_map). The reason is that the Maslov phase ρ(L₀, A L₀) = det A / conj (det A) is multiplicative and that z / conj z = (z / ‖z‖) ^ 2 for z ≠ 0. In particular a constant automorphism does not change the Maslov index (TauCeti.TotallyRealLoop.maslovIndex_map_const), and since the degree is a homotopy invariant, the Maslov index of B Λ only depends on the free homotopy class of the loop B (TauCeti.TotallyRealLoop.maslovIndex_map_eq_of_homotopy).

This is the product axiom of the Maslov index of totally real loops, complementing homotopy invariance and the normalization (TauCeti.LinearAlgebra.TotallyReal.Maslov.Index) and the direct-sum axiom (TauCeti.LinearAlgebra.TotallyReal.Maslov.Prod). It is the formula that controls a change of trivialization: the boundary Maslov index of a bundle pair over a surface with boundary is computed from the boundary loop in a trivialization, and two trivializations of a bundle over a disk differ along the boundary by a loop of automorphisms that extends over the disk, whose determinant therefore has degree zero.

Main declarations

• TauCeti.TotallyRealLoop.maslovIndex_map: μ(B Λ) = μ(Λ) + 2 deg (det B).
• TauCeti.TotallyRealLoop.maslovIndex_map_const: a constant automorphism preserves the Maslov index.
• TauCeti.TotallyRealLoop.maslovIndex_map_eq_of_homotopy: moving a loop by freely homotopic loops of automorphisms gives loops with the same Maslov index.

References

• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Appendix C.3 (the product axiom of the Maslov index of loops of totally real subspaces).

theorem TauCeti.TotallyRealLoop.maslovIndex_map {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] (Λ : TotallyRealLoop E) (B : ↑unitInterval → E ≃L[ℂ] E) (hB : Continuous fun (t : ↑unitInterval) => ↑(B t)) (hB01 : B 0 = B 1) {x : Circle} (δ : Path x x) (hδ : ∀ (t : ↑unitInterval), LinearMap.det ↑↑(B t) = ↑‖LinearMap.det ↑↑(B t)‖ * ↑(δ t)) : (Λ.map B hB hB01).maslovIndex = Λ.maslovIndex + 2 * Circle.degree δ

The Maslov index under a loop of automorphisms. If B is a loop of complex-linear automorphisms and δ is the circle loop of normalized determinants, det (B t) = ‖det (B t)‖ δ t, then μ(B Λ) = μ(Λ) + 2 deg δ.

@[simp]

theorem TauCeti.TotallyRealLoop.maslovIndex_map_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] (Λ : TotallyRealLoop E) (A : E ≃L[ℂ] E) : (Λ.map (fun (x : ↑unitInterval) => A) ⋯ ⋯).maslovIndex = Λ.maslovIndex

Naturality of the Maslov index. Moving a loop of maximal totally real subspaces by a fixed complex-linear automorphism does not change its Maslov index.

theorem TauCeti.TotallyRealLoop.maslovIndex_map_eq_of_homotopy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] (Λ : TotallyRealLoop E) (B : ↑unitInterval × ↑unitInterval → E ≃L[ℂ] E) (hB : Continuous fun (p : ↑unitInterval × ↑unitInterval) => ↑(B p)) (hB01 : ∀ (s : ↑unitInterval), B (s, 0) = B (s, 1)) : (Λ.map (fun (t : ↑unitInterval) => B (0, t)) ⋯ ⋯).maslovIndex = (Λ.map (fun (t : ↑unitInterval) => B (1, t)) ⋯ ⋯).maslovIndex

Homotopy invariance in the frame. If B is a free homotopy of loops of complex-linear automorphisms, B (s, 0) = B (s, 1) for every s, then moving a loop of maximal totally real subspaces by B (0, ·) or by B (1, ·) gives loops with the same Maslov index.