Almost complex structures as complex module structures

A pointwise almost complex structure J on a real module V (a real-linear endomorphism with J ∘ J = -1, from TauCeti.AlmostComplexStructure) is the same data as a complex vector space structure on V extending the real one: scalar multiplication by a + b·i is a • v + b • J v, and conversely multiplication by i recovers J. This file makes that classical correspondence (McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.1) precise.

The forward direction AlmostComplexStructure.complexModule turns J into a Module ℂ V; it is deliberately a def, not an instance, because the complex structure depends on the chosen J and is not canonical. The backward direction AlmostComplexStructure.ofComplexModule reads an almost complex structure off any complex module structure compatible with the real scalars. The round-trip lemmas say that ofComplexModule applied to complexModule J returns J, and that the module structure induced from ofComplexModule recovers the original complex module structure.

Main declarations

• TauCeti.AlmostComplexStructure.complexModule: the Module ℂ V with (a + b·i) • v = a • v + b • J v.
• TauCeti.AlmostComplexStructure.complexModule_smul_def: the defining scalar action.
• TauCeti.AlmostComplexStructure.complexModule_I_smul: i • v = J v in the induced module.
• TauCeti.AlmostComplexStructure.complexModule_ofReal_smul: the induced action restricts to the original real action.
• TauCeti.AlmostComplexStructure.complexModule_isScalarTower: ℝ, ℂ, V form a scalar tower.
• TauCeti.AlmostComplexStructure.ofComplexModule: the almost complex structure v ↦ i • v on a complex module.
• TauCeti.AlmostComplexStructure.ofComplexModule_complexModule: the round trip recovers J.
• TauCeti.AlmostComplexStructure.complexModule_ofComplexModule: the opposite round trip recovers the original complex module structure.

@[implicit_reducible]

def TauCeti.AlmostComplexStructure.complexModule {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : Module ℂ V

The complex vector space structure on a real module V induced by an almost complex structure J: the scalar a + b·i acts as a • v + b • J v.

This is a def rather than an instance because the complex structure is not canonical: it depends on the chosen J. It uses Complex.liftAux to extend the real scalars through the endomorphism algebra. Restricted to the real scalars it is the original Module ℝ V (complexModule_isScalarTower, complexModule_ofReal_smul).

Equations

• J.complexModule = Module.compHom V (Complex.liftAux J.toLinearMap ⋯).toRingHom

@[simp]

theorem TauCeti.AlmostComplexStructure.complexModule_smul_def {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (z : ℂ) (v : V) : z • v = z.re • v + z.im • J.toLinearMap v

The defining formula for the complex action induced by an almost complex structure.

theorem TauCeti.AlmostComplexStructure.complexModule_I_smul {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : Complex.I • v = J.toLinearMap v

In the induced complex structure, multiplication by i is J.

theorem TauCeti.AlmostComplexStructure.complexModule_ofReal_smul {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (r : ℝ) (v : V) : ↑r • v = r • v

The induced complex action restricts along ℝ → ℂ to the original real action.

theorem TauCeti.AlmostComplexStructure.complexModule_isScalarTower {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : IsScalarTower ℝ ℂ V

ℝ, ℂ, and V form a scalar tower for the induced complex structure: the real scalars act the same whether through ℝ or through ℂ.

def TauCeti.AlmostComplexStructure.ofComplexModule (V : Type u_2) [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] : AlmostComplexStructure V

The almost complex structure v ↦ i • v on a complex module whose real scalars are compatible with the ambient real structure. This is the inverse construction to complexModule.

Equations

• TauCeti.AlmostComplexStructure.ofComplexModule V = { toLinearMap := ↑ℝ ((LinearMap.lsmul ℂ V) Complex.I), square_neg := ⋯ }

@[simp]

theorem TauCeti.AlmostComplexStructure.ofComplexModule_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] (v : V) : (ofComplexModule V).toLinearMap v = Complex.I • v

The almost complex structure read from a complex module acts by multiplication by i.

@[simp]

theorem TauCeti.AlmostComplexStructure.ofComplexModule_complexModule {V : Type u_2} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : ofComplexModule V = J

Reading the almost complex structure back off the induced complex module recovers J.

@[simp]

theorem TauCeti.AlmostComplexStructure.complexModule_ofComplexModule {V : Type u_2} [AddCommGroup V] [Module ℝ V] [m : Module ℂ V] [IsScalarTower ℝ ℂ V] : (ofComplexModule V).complexModule = m

The complex module induced by ofComplexModule is the original module structure.