Loops of totally real subspaces #
Let E be a complex seminormed space. A loop of maximal totally real subspaces of E
(TauCeti.TotallyRealLoop) is a family Λ : [0, 1] → Submodule ℝ E with Λ 0 = Λ 1 of the form
Λ t = A t L₀, where L₀ is maximal totally real and A is a continuous path of complex-linear
automorphisms of E. In finite-dimensional normed spaces, this is the usual notion of a
continuous loop in the totally real Grassmannian GL(n, ℂ) / GL(n, ℝ), since paths in that
homogeneous space lift to GL(n, ℂ). Such loops give boundary conditions for Cauchy--Riemann
operators.
Main declarations #
TauCeti.TotallyRealLoop: loops of maximal totally real subspaces.TauCeti.TotallyRealLoop.isMaximalTotallyReal: every subspace of such a loop is maximal totally real.TauCeti.TotallyRealLoop.const: the constant loop at a maximal totally real subspace.TauCeti.exists_frame_map: composing a frame with a continuous family of automorphisms gives a frame of the image.TauCeti.TotallyRealLoop.map: the pointwise imaget ↦ B t (Λ t)under a loopBof complex-linear automorphisms.TauCeti.TotallyRealLoop.symm: the loopt ↦ Λ (1 - t)traversed backwards.TauCeti.TotallyRealLoop.rotation: the half-turnt ↦ e^{iπt} L₀, which closes up since-L₀ = L₀.TauCeti.TotallyRealLoop.rotationZPow: thek-fold half-turnt ↦ e^{iπkt} L₀for an integerk, which closes up sincee^{iπk} = ±1.
References #
- D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Appendix C.3 (loops of totally real subspaces as boundary conditions).
Composing a frame with a continuous family of complex-linear automorphisms gives a frame of
the image: if Λ x = A x L₀ for a continuous family A, then B x (Λ x) = (B x ∘ A x) L₀, and
x ↦ B x ∘ A x is again continuous.
A loop of maximal totally real subspaces of a complex seminormed space E, parametrized by
the unit interval: a family Λ t with Λ 0 = Λ 1 of the form Λ t = A t L₀ for a maximal
totally real subspace L₀ and a continuous path A of complex-linear automorphisms.
- toFun : ↑unitInterval → Submodule ℝ E
The subspace at time
t. - exists_frame : ∃ (L₀ : Submodule ℝ E), IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L₀ ∧ ∃ (A : ↑unitInterval → E ≃L[ℂ] E), (Continuous fun (t : ↑unitInterval) => ↑(A t)) ∧ ∀ (t : ↑unitInterval), ↑self t = Submodule.map (↑ℝ ↑↑(A t)) L₀
The loop is moved by a continuous frame of complex-linear automorphisms from a maximal totally real subspace.
The loop is closed.
Instances For
Every subspace of a loop of maximal totally real subspaces is maximal totally real.
The constant loop at a maximal totally real subspace.
Instances For
The pointwise image t ↦ B t (Λ t) of a loop of maximal totally real subspaces under a loop
B of complex-linear automorphisms.
Instances For
The reverse t ↦ Λ (1 - t) of a loop of maximal totally real subspaces: the same loop
traversed backwards.
Instances For
Reversing a loop twice gives the loop back.
The loop t ↦ e^{iπt} L₀, t ∈ [0, 1], turning a maximal totally real subspace L₀ through
half a revolution; it closes up because -L₀ = L₀.
Instances For
The loop t ↦ e^{iπkt} L₀, t ∈ [0, 1], turning a maximal totally real subspace L₀ through
k half revolutions, for an integer k; it closes up because e^{iπk} = ±1 and -L₀ = L₀. For
k = 1 it is the half-turn TauCeti.TotallyRealLoop.rotation
(TauCeti.TotallyRealLoop.rotationZPow_one). On the unit circle θ = 2πt, this is the loop
θ ↦ e^{ikθ/2} L₀.
Instances For
The single half-turn is the half-turn TauCeti.TotallyRealLoop.rotation.
Zero half-turns give the constant loop.