The Maslov index is additive under the direct sum

The Maslov index μ(Λ) of a loop of maximal totally real subspaces is a winding number, and a winding number adds over a direct sum. This file proves the corresponding direct-sum axiom

μ(Λ ⊕ Λ') = μ(Λ) + μ(Λ'),

where Λ ⊕ Λ' is the loop t ↦ Λ t ⊕ Λ' t of coordinate subspaces of E × E', packaged as TauCeti.TotallyRealLoop.prod, and its counterpart for the relative Maslov index of two paths with common endpoints,

μ(Λ ⊕ Λ', Γ ⊕ Γ') = μ(Λ, Γ) + μ(Λ', Γ'),

where TauCeti.TotallyRealPath.prod is the direct sum of two paths. The direct sum of two loops is built from the direct sum of the underlying paths. These direct-sum constructions are defined for complex seminormed spaces; the Maslov index results use finite-dimensional complex normed spaces.

The two ingredients are multiplicative. The Maslov phase of a direct sum is the product of the two phases, ρ(L₀ ⊕ L₀', L ⊕ L') = ρ(L₀, L) ρ(L₀', L'), because an automorphism carrying L₀ to L and L₀' to L' is carried out blockwise, its determinant is the product of the two block determinants, and the determinant phase is multiplicative. And the degree of a pointwise product of loops in the circle is the sum of the degrees. Composing the two, and reading the Maslov index as the degree of the loop of phases relative to an arbitrary reference subspace, gives the axiom; for paths, the relative phase loop of the direct sum is likewise the product of the two relative phase loops.

The linear-algebra input, that a coordinate submodule L.prod M of a product of complex modules is maximal totally real whenever the two summands are, is TauCeti.IsMaximalTotallyReal.isMaximalTotallyReal_prod (TauCeti/LinearAlgebra/TotallyReal/Complex.lean), and rests on TauCeti.LinearMap.lsmul_restrictScalars_prodMap (TauCeti/LinearAlgebra/Prod.lean), which says that multiplication by a scalar on a product is the product map of the two multiplications.

The axiom is the additivity half of the standard list of properties of the Maslov index (Robbin--Salamon, The Maslov index for paths, Topology 32 (1993); McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Appendix C.3). It combines two loops that vary independently: it is the statement needed whenever a totally real boundary condition, or a pair of complex bundles, is a direct sum of two such conditions or bundles, each with its own loop of totally real subspaces. Summing over the separate boundary components of a Cauchy--Riemann operator on a surface, each of which carries a loop of its own, is a further step built on top of this one.

Main declarations

• TauCeti.IsMaximalTotallyReal.maslovPhase_prod: the Maslov phase of a direct sum is the product of the two phases.
• TauCeti.TotallyRealPath.prod, TauCeti.TotallyRealLoop.prod: the path, respectively loop, of coordinate subspaces of a pair of paths or loops.
• TauCeti.TotallyRealPath.relativeMaslovIndex_prod: the direct-sum axiom of the relative Maslov index.
• TauCeti.TotallyRealLoop.maslovPhasePath_prod_apply: the loop of Maslov phases of a direct sum is the product of the two loops of Maslov phases.
• TauCeti.TotallyRealLoop.maslovIndex_prod: the direct-sum axiom of the Maslov index of loops.
• TauCeti.TotallyRealLoop.maslovIndex_prod_rotation: the two half-turns, taken in the two summands, have Maslov index the sum of the two complex dimensions.

References

• J. Robbin and D. Salamon, The Maslov index for paths, Topology 32 (1993), the axioms of the Maslov index of a loop of Lagrangian subspaces, one of which is the direct-sum axiom.
• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Appendix C.3 (the Maslov index of a loop of totally real subspaces, and the boundary Maslov index of a bundle pair).

theorem TauCeti.IsMaximalTotallyReal.maslovPhase_prod {E : Type u_1} {E' : Type u_2} [AddCommGroup E] [Module ℝ E] [Module ℂ E] [IsScalarTower ℝ ℂ E] {L : Submodule ℝ E} [AddCommGroup E'] [Module ℝ E'] [Module ℂ E'] [IsScalarTower ℝ ℂ E'] {M : Submodule ℝ E'} [FiniteDimensional ℂ E] [FiniteDimensional ℂ E'] {L' : Submodule ℝ E} {M' : Submodule ℝ E'} (hL : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L) (hM : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E') Complex.I)) M) (hL' : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L') (hM' : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E') Complex.I)) M') : ⋯.maslovPhase ⋯ = hL.maslovPhase hL' * hM.maslovPhase hM'

The Maslov phase of a direct sum is the product of the two phases: ρ(L₀ ⊕ L₀', L ⊕ L') = ρ(L₀, L) ρ(L₀', L').

noncomputable def TauCeti.TotallyRealPath.prod {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℂ E] {E' : Type u_2} [SeminormedAddCommGroup E'] [NormedSpace ℂ E'] (Λ : TotallyRealPath E) (Λ' : TotallyRealPath E') : TotallyRealPath (E × E')

The path of coordinate subspaces of a pair of paths of maximal totally real subspaces: the direct sum Λ ⊕ Λ' of t ↦ Λ t and t ↦ Λ' t, in the product of the ambient spaces.

@[simp]

theorem TauCeti.TotallyRealPath.prod_apply {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℂ E] {E' : Type u_2} [SeminormedAddCommGroup E'] [NormedSpace ℂ E'] (Λ : TotallyRealPath E) (Λ' : TotallyRealPath E') (t : ↑unitInterval) : ↑(Λ.prod Λ') t = (↑Λ t).prod (↑Λ' t)

@[simp]

theorem TauCeti.TotallyRealPath.relativeMaslovIndex_prod {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℂ E'] [FiniteDimensional ℂ E'] (Λ Γ : TotallyRealPath E) (Λ' Γ' : TotallyRealPath E') (h₀ : ↑Λ 0 = ↑Γ 0) (h₁ : ↑Λ 1 = ↑Γ 1) (h₀' : ↑Λ' 0 = ↑Γ' 0) (h₁' : ↑Λ' 1 = ↑Γ' 1) : (Λ.prod Λ').relativeMaslovIndex (Γ.prod Γ') ⋯ ⋯ = Λ.relativeMaslovIndex Γ h₀ h₁ + Λ'.relativeMaslovIndex Γ' h₀' h₁'

The direct-sum axiom of the relative Maslov index: μ(Λ ⊕ Λ', Γ ⊕ Γ') = μ(Λ, Γ) + μ(Λ', Γ').

noncomputable def TauCeti.TotallyRealLoop.prod {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℂ E] {E' : Type u_2} [SeminormedAddCommGroup E'] [NormedSpace ℂ E'] (Λ : TotallyRealLoop E) (Λ' : TotallyRealLoop E') : TotallyRealLoop (E × E')

The loop of coordinate subspaces of a pair of loops of maximal totally real subspaces: the direct sum Λ ⊕ Λ' of t ↦ Λ t and t ↦ Λ' t, in the product of the ambient spaces.

@[simp]

theorem TauCeti.TotallyRealLoop.prod_apply {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℂ E] {E' : Type u_2} [SeminormedAddCommGroup E'] [NormedSpace ℂ E'] (Λ : TotallyRealLoop E) (Λ' : TotallyRealLoop E') (t : ↑unitInterval) : ↑(Λ.prod Λ') t = (↑Λ t).prod (↑Λ' t)

theorem TauCeti.TotallyRealLoop.maslovPhasePath_prod_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℂ E'] [FiniteDimensional ℂ E'] (Λ : TotallyRealLoop E) (Λ' : TotallyRealLoop E') (t : ↑unitInterval) : ↑((Λ.prod Λ').maslovPhasePath t) = ↑(Λ.maslovPhasePath t) * ↑(Λ'.maslovPhasePath t)

The loop of Maslov phases of a direct sum is the product of the two loops of Maslov phases: read as a complex number, the phase of the direct sum at t is the product of the two phases at t.

@[simp]

theorem TauCeti.TotallyRealLoop.maslovIndex_prod {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℂ E'] [FiniteDimensional ℂ E'] (Λ : TotallyRealLoop E) (Λ' : TotallyRealLoop E') : (Λ.prod Λ').maslovIndex = Λ.maslovIndex + Λ'.maslovIndex

The direct-sum axiom of the Maslov index. The Maslov index of the direct sum of two loops of maximal totally real subspaces is the sum of their Maslov indices.

theorem TauCeti.TotallyRealLoop.maslovIndex_prod_rotation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℂ E'] [FiniteDimensional ℂ E'] {L₁ : Submodule ℝ E} {L₂ : Submodule ℝ E'} (hL₁ : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L₁) (hL₂ : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E') Complex.I)) L₂) : ((rotation hL₁).prod (rotation hL₂)).maslovIndex = ↑(Module.finrank ℂ E) + ↑(Module.finrank ℂ E')

The direct sum of the two half-turns has Maslov index the sum of the two complex dimensions.