The conjugate graph of a real-linear map

For a real-linear automorphism K and a real-linear operator Ψ of a complex normed space E, the conjugate graph conjGraph K Ψ = {(K z, Ψ z) | z ∈ E} is a real subspace of E × E (TauCeti.conjGraph). When K is a conjugation, a real-linear automorphism anticommuting with i, the map (u, w) ↦ (K u, w) is complex linear from (E, -i) × (E, i) to E × E, and the conjugate graph is the image of the graph of Ψ in (E, -i) × (E, i).

For such K:

• the conjugate graph of the identity is maximal totally real (TauCeti.isMaximalTotallyReal_conjGraph_id);
• the conjugate graph of Ψ is the conjugate graph of the identity moved by the map (u, w) ↦ (u, Q u + P w), with P the complex-linear part of Ψ and Q that of Ψ ∘ K⁻¹ (TauCeti.conjGraph_eq_map).

These are used in TauCeti.LinearAlgebra.TotallyReal.Maslov.Symplectic to read the graph of a linear symplectic map as a maximal totally real subspace.

References

• J. Robbin and D. Salamon, The Maslov index for paths, Topology 32 (1993), 827–844, Section 4 (graphs of linear symplectic maps).

noncomputable def TauCeti.conjGraph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (K : E ≃L[ℝ] E) (Ψ : E →L[ℝ] E) : Submodule ℝ (E × E)

The conjugate graph {(K z, Ψ z) | z ∈ E} of a real-linear operator Ψ of a complex normed space, for a real-linear automorphism K. When K is a conjugation, this is the graph of Ψ in (E, -i) × (E, i), read in E × E through K on the first factor.

@[simp]

theorem TauCeti.mem_conjGraph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {K : E ≃L[ℝ] E} {Ψ : E →L[ℝ] E} {x : E × E} : x ∈ conjGraph K Ψ ↔ ∃ (z : E), (K z, Ψ z) = x

theorem TauCeti.isMaximalTotallyReal_conjGraph_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {K : E ≃L[ℝ] E} (hK : ∀ (z : E), K (Complex.I • z) = -(Complex.I • K z)) : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ (E × E)) Complex.I)) (conjGraph K (ContinuousLinearMap.id ℝ E))

The conjugate graph of the identity is maximal totally real. For an automorphism K anticommuting with i, the subspace {(K z, z)} of E × E is complementary to its image under multiplication by i.

theorem TauCeti.conjGraph_eq_map {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {K : E ≃L[ℝ] E} (hK : ∀ (z : E), K (Complex.I • z) = -(Complex.I • K z)) (Ψ : E →L[ℝ] E) : conjGraph K Ψ = Submodule.map ((LinearMap.fst ℝ E E).prod (↑(ContinuousLinearMap.restrictScalars ℝ (Ψ ∘SL ↑K.symm).complexLinearPart) ∘ₗ LinearMap.fst ℝ E E + ↑(ContinuousLinearMap.restrictScalars ℝ Ψ.complexLinearPart) ∘ₗ LinearMap.snd ℝ E E)) (conjGraph K (ContinuousLinearMap.id ℝ E))

The conjugate graph of Ψ is the conjugate graph of the identity moved by the real-linear map (u, w) ↦ (u, Q u + P w), where P is the complex-linear part of Ψ and Q that of Ψ ∘ K⁻¹.