Totally real factors of the standard product almost complex structure

The general doubled-module lemmas in TauCeti.LinearAlgebra.TotallyReal.Basic are phrased for the Mathlib map LinearEquiv.skewSwap, which sends (x, y) to (-y, x). The symplectic layer has its own bundled version of the same map, TauCeti.AlmostComplexStructure.product. This file bridges the two so the geometric standard structure reuses the algebraic results rather than restating them.

Main declarations

• TauCeti.AlmostComplexStructure.product_toLinearMap_eq_skewSwap: the standard product almost complex structure is the skewSwap doubled-module complex structure.
• TauCeti.Submodule.isMaximalTotallyReal_prod_top_bot_product and TauCeti.Submodule.isMaximalTotallyReal_prod_bot_top_product: the two coordinate factors of V × V are maximal totally real for the standard product almost complex structure.

theorem TauCeti.AlmostComplexStructure.product_toLinearMap_eq_skewSwap {V : Type u_1} [AddCommGroup V] [Module ℝ V] : (product V).toLinearMap = ↑(LinearEquiv.skewSwap ℝ V V)

The standard product almost complex structure on V × V is the skewSwap doubled-module complex structure: both send (x, y) to (-y, x).

theorem TauCeti.Submodule.isMaximalTotallyReal_prod_top_bot_product {V : Type u_1} [AddCommGroup V] [Module ℝ V] : IsMaximalTotallyReal (AlmostComplexStructure.product V).toLinearMap (⊤.prod ⊥)

The first factor in V × V is maximal totally real for the standard product almost complex structure.

theorem TauCeti.Submodule.isMaximalTotallyReal_prod_bot_top_product {V : Type u_1} [AddCommGroup V] [Module ℝ V] : IsMaximalTotallyReal (AlmostComplexStructure.product V).toLinearMap (⊥.prod ⊤)

The second factor in V × V is maximal totally real for the standard product almost complex structure.