Relative Maslov index of paths of totally real subspaces #

In a finite-dimensional complex normed space, for two paths Λ, Γ of maximal totally real subspaces with the same endpoints, the Maslov phases t ↦ ρ(Γ t, Λ t) form a loop in the circle based at 1. Its degree is the relative Maslov index μ(Λ, Γ), an integer measuring the relative homotopy class detected by the Maslov phases; the crossing-form index for a single path is a further construction.

The relative index has the formal properties of the Robbin--Salamon Maslov index for paths:

it vanishes on the diagonal, μ(Λ, Λ) = 0, and is antisymmetric, μ(Γ, Λ) = -μ(Λ, Γ) (TauCeti.TotallyRealPath.relativeMaslovIndex_swap);
it is a cocycle, μ(Λ, Γ) + μ(Γ, Δ) = μ(Λ, Δ) (TauCeti.TotallyRealPath.relativeMaslovIndex_add);
it is additive under catenation of paths, μ(Λ₁ ⬝ Λ₂, Γ₁ ⬝ Γ₂) = μ(Λ₁, Γ₁) + μ(Λ₂, Γ₂) (TauCeti.TotallyRealPath.relativeMaslovIndex_trans), and reversing both paths negates it (TauCeti.TotallyRealPath.relativeMaslovIndex_symm);
it is natural: moving both paths by the same continuous path of complex-linear automorphisms does not change it (TauCeti.TotallyRealPath.relativeMaslovIndex_map);
it is invariant under homotopies of the pair, given by continuous two-parameter frames, during which the two paths keep common endpoints (TauCeti.TotallyRealPath.relativeMaslovIndex_eq_of_homotopy);
it is additive under direct sums, μ(Λ ⊕ Λ', Γ ⊕ Γ') = μ(Λ, Γ) + μ(Λ', Γ') (TauCeti.TotallyRealPath.relativeMaslovIndex_prod, in TauCeti/LinearAlgebra/TotallyReal/Maslov/Prod.lean);
for two loops with the same base subspace it is the difference of their Maslov indices, μ(Λ, Γ) = μ(Λ) - μ(Γ) (TauCeti.TotallyRealLoop.relativeMaslovIndex_toTotallyRealPath).

The paths are given, like loops, by continuous frames of complex-linear automorphisms acting on one maximal totally real subspace; reversal (TauCeti.TotallyRealPath.symm), catenation (TauCeti.TotallyRealPath.trans) and the pointwise image under a path of automorphisms (TauCeti.TotallyRealPath.map) are constructed on such frames. These basic path constructions are defined for complex seminormed spaces; the Maslov phase and index theory below uses finite-dimensional complex normed spaces.

The Maslov phase and its loop degree follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Appendix C.3. The relative path viewpoint and the naturality, catenation, homotopy and direct-sum properties are those of the Robbin--Salamon Maslov index for paths.

Main declarations #

TauCeti.TotallyRealPath: paths of maximal totally real subspaces.
TauCeti.TotallyRealPath.symm, TauCeti.TotallyRealPath.trans: reversal and catenation.
TauCeti.TotallyRealPath.map: the pointwise image under a path of automorphisms.
TauCeti.TotallyRealLoop.toTotallyRealPath: a loop, read as a path.
TauCeti.TotallyRealPath.relativeMaslovPhasePath: the loop t ↦ ρ(Γ t, Λ t).
TauCeti.TotallyRealPath.relativeMaslovIndex: its degree.
TauCeti.TotallyRealPath.relativeMaslovIndex_eq_degree: the relative index is the degree of every loop of the circle with the values ρ(Γ t, Λ t).

References #

D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Appendix C.3.
J. Robbin and D. Salamon, The Maslov index for paths, Topology 32 (1993), 827--844, Theorem 2.3 (the axioms of the Maslov index for paths, including naturality, catenation, homotopy invariance and the direct sum).