Continuity of the Maslov phase along continuous frames

The Maslov phase ρ(L₀, Λ x) = ρ(L₀, L₁) · det(A x) / conj (det A x) relative to a fixed maximal totally real subspace L₀ varies continuously along any continuous frame x ↦ A x L₁ of maximal totally real subspaces over a topological space X (TauCeti.IsMaximalTotallyReal.continuous_maslovPhase_of_frame), where ρ is TauCeti.IsMaximalTotallyReal.maslovPhase. The lemma constructs continuous circle-valued phase maps from families of maximal totally real subspaces that admit continuous frames, covering in particular paths and loops of frames.

The loop and path theorems in TauCeti.LinearAlgebra.TotallyReal.Maslov.Index and TauCeti.LinearAlgebra.TotallyReal.Maslov.Path are specializations to the parameter spaces [0, 1].

References

• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Appendix C.3.

theorem TauCeti.IsMaximalTotallyReal.continuous_maslovPhase_of_frame {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {X : Type u_2} [TopologicalSpace X] {L₀ L₁ : Submodule ℝ E} (hL₀ : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L₀) (hL₁ : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L₁) {Λ : X → Submodule ℝ E} (hΛ : ∀ (x : X), IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) (Λ x)) {A : X → E ≃L[ℂ] E} (hAc : Continuous fun (x : X) => ↑(A x)) (hA : ∀ (x : X), Λ x = Submodule.map (↑ℝ ↑↑(A x)) L₁) : Continuous fun (x : X) => hL₀.maslovPhase ⋯

The Maslov phase relative to a fixed maximal totally real subspace varies continuously along any continuous frame x ↦ A x L₁ of maximal totally real subspaces over a topological space X.