Type projections of an almost complex structure

The complexification of a real almost complex structure J splits into its i- and -i-eigenspaces. The projections onto these summands are (1 - i J) / 2 and (1 + i J) / 2, respectively. We use Mathlib's submodule projections, so their images and kernels are the existing eigenspaces, rather than new carriers for the type components.

Conjugation exchanges the projections, and scalar extension of a map intertwining almost complex structures commutes with both. The pure-tensor formulas fix the normalization of v ↦ v^(1,0); its restriction to the real vectors is injective. These are the fibrewise operations for complex tangent type decompositions.

The conventions follow Demailly, Complex Analytic and Differential Geometry, Chapter I, the decomposition of the complexified tangent space of an almost complex manifold.

noncomputable def TauCeti.AlmostComplexStructure.holomorphicProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : TensorProduct ℝ ℂ V →ₗ[ℂ] TensorProduct ℝ ℂ V

Projection onto the (1,0) vectors, along the (0,1) vectors, in the complexification.

noncomputable def TauCeti.AlmostComplexStructure.antiholomorphicProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : TensorProduct ℝ ℂ V →ₗ[ℂ] TensorProduct ℝ ℂ V

Projection onto the (0,1) vectors, along the (1,0) vectors, in the complexification.

theorem TauCeti.AlmostComplexStructure.holomorphicProjection_def {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : J.holomorphicProjection = (Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I).projection (Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-Complex.I)) ⋯

The holomorphic projection is the native projection onto the positive eigenspace.

theorem TauCeti.AlmostComplexStructure.antiholomorphicProjection_def {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : J.antiholomorphicProjection = (Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-Complex.I)).projection (Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I) ⋯

The antiholomorphic projection is the native projection onto the negative eigenspace.

theorem TauCeti.AlmostComplexStructure.holomorphicProjection_add_antiholomorphicProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : J.holomorphicProjection u + J.antiholomorphicProjection u = u

Every complexified vector is the sum of its two type components.

theorem TauCeti.AlmostComplexStructure.antiholomorphicProjection_apply_eq_sub {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : J.antiholomorphicProjection u = u - J.holomorphicProjection u

The antiholomorphic component is the complement of the holomorphic component.

theorem TauCeti.AlmostComplexStructure.holomorphicProjection_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : J.holomorphicProjection u = 2⁻¹ • (u - Complex.I • (LinearMap.baseChange ℂ J.toLinearMap) u)

The explicit (1,0) projection is (u - i J u) / 2.

theorem TauCeti.AlmostComplexStructure.antiholomorphicProjection_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : J.antiholomorphicProjection u = 2⁻¹ • (u + Complex.I • (LinearMap.baseChange ℂ J.toLinearMap) u)

The explicit (0,1) projection is (u + i J u) / 2.

@[simp]

theorem TauCeti.AlmostComplexStructure.range_holomorphicProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : J.holomorphicProjection.range = Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I

@[simp]

theorem TauCeti.AlmostComplexStructure.range_antiholomorphicProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : J.antiholomorphicProjection.range = Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-Complex.I)

theorem TauCeti.AlmostComplexStructure.holomorphicProjection_apply_mem {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : J.holomorphicProjection u ∈ Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I

The holomorphic component lies in the i-eigenspace of the complexified structure.

theorem TauCeti.AlmostComplexStructure.antiholomorphicProjection_apply_mem {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : J.antiholomorphicProjection u ∈ Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-Complex.I)

The antiholomorphic component lies in the -i-eigenspace of the complexified structure.

@[simp]

theorem TauCeti.AlmostComplexStructure.baseChange_apply_holomorphicProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : (LinearMap.baseChange ℂ J.toLinearMap) (J.holomorphicProjection u) = Complex.I • J.holomorphicProjection u

The complexified structure acts by i on the holomorphic component.

@[simp]

theorem TauCeti.AlmostComplexStructure.baseChange_apply_antiholomorphicProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : (LinearMap.baseChange ℂ J.toLinearMap) (J.antiholomorphicProjection u) = -Complex.I • J.antiholomorphicProjection u

The complexified structure acts by -i on the antiholomorphic component.

@[simp]

theorem TauCeti.AlmostComplexStructure.ker_holomorphicProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : J.holomorphicProjection.ker = Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-Complex.I)

@[simp]

theorem TauCeti.AlmostComplexStructure.ker_antiholomorphicProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : J.antiholomorphicProjection.ker = Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I

@[simp]

theorem TauCeti.AlmostComplexStructure.holomorphicProjection_eq_self_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : J.holomorphicProjection u = u ↔ (LinearMap.baseChange ℂ J.toLinearMap) u = Complex.I • u

A vector is of type (1,0) exactly when the holomorphic projection fixes it.

@[simp]

theorem TauCeti.AlmostComplexStructure.antiholomorphicProjection_eq_self_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : J.antiholomorphicProjection u = u ↔ (LinearMap.baseChange ℂ J.toLinearMap) u = -Complex.I • u

A vector is of type (0,1) exactly when the antiholomorphic projection fixes it.

@[simp]

theorem TauCeti.AlmostComplexStructure.holomorphicProjection_eq_zero_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : J.holomorphicProjection u = 0 ↔ (LinearMap.baseChange ℂ J.toLinearMap) u = -Complex.I • u

@[simp]

theorem TauCeti.AlmostComplexStructure.antiholomorphicProjection_eq_zero_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : J.antiholomorphicProjection u = 0 ↔ (LinearMap.baseChange ℂ J.toLinearMap) u = Complex.I • u

@[simp]

theorem TauCeti.AlmostComplexStructure.holomorphicProjection_holomorphicProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : J.holomorphicProjection (J.holomorphicProjection u) = J.holomorphicProjection u

@[simp]

theorem TauCeti.AlmostComplexStructure.antiholomorphicProjection_antiholomorphicProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : J.antiholomorphicProjection (J.antiholomorphicProjection u) = J.antiholomorphicProjection u

@[simp]

theorem TauCeti.AlmostComplexStructure.holomorphicProjection_antiholomorphicProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : J.holomorphicProjection (J.antiholomorphicProjection u) = 0

@[simp]

theorem TauCeti.AlmostComplexStructure.antiholomorphicProjection_holomorphicProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : J.antiholomorphicProjection (J.holomorphicProjection u) = 0

theorem TauCeti.AlmostComplexStructure.holomorphicProjection_tmul {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (c : ℂ) (v : V) : J.holomorphicProjection (c ⊗ₜ[ℝ] v) = 2⁻¹ • (c ⊗ₜ[ℝ] v - (Complex.I * c) ⊗ₜ[ℝ] J.toLinearMap v)

On a pure tensor, the (1,0) projection is (c ⊗ v - (i c) ⊗ J v) / 2.

theorem TauCeti.AlmostComplexStructure.antiholomorphicProjection_tmul {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (c : ℂ) (v : V) : J.antiholomorphicProjection (c ⊗ₜ[ℝ] v) = 2⁻¹ • (c ⊗ₜ[ℝ] v + (Complex.I * c) ⊗ₜ[ℝ] J.toLinearMap v)

On a pure tensor, the (0,1) projection is (c ⊗ v + (i c) ⊗ J v) / 2.

@[simp]

theorem TauCeti.AlmostComplexStructure.tmulConj_holomorphicProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : (tmulConj V) (J.holomorphicProjection u) = J.antiholomorphicProjection ((tmulConj V) u)

Canonical conjugation exchanges the two type projections.

@[simp]

theorem TauCeti.AlmostComplexStructure.tmulConj_antiholomorphicProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (u : TensorProduct ℝ ℂ V) : (tmulConj V) (J.antiholomorphicProjection u) = J.holomorphicProjection ((tmulConj V) u)

Canonical conjugation exchanges the two type projections in the reverse direction.

theorem TauCeti.AlmostComplexStructure.baseChange_holomorphicProjection {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : AlmostComplexStructure V) (K : AlmostComplexStructure W) (f : V →ₗ[ℝ] W) (hf : IsComplexLinearMap J K f) (u : TensorProduct ℝ ℂ V) : (LinearMap.baseChange ℂ f) (J.holomorphicProjection u) = K.holomorphicProjection ((LinearMap.baseChange ℂ f) u)

Scalar extension of an intertwining map preserves the holomorphic projection.

theorem TauCeti.AlmostComplexStructure.baseChange_antiholomorphicProjection {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : AlmostComplexStructure V) (K : AlmostComplexStructure W) (f : V →ₗ[ℝ] W) (hf : IsComplexLinearMap J K f) (u : TensorProduct ℝ ℂ V) : (LinearMap.baseChange ℂ f) (J.antiholomorphicProjection u) = K.antiholomorphicProjection ((LinearMap.baseChange ℂ f) u)

Scalar extension of an intertwining map preserves the antiholomorphic projection.

theorem TauCeti.AlmostComplexStructure.holomorphicProjection_one_tmul_injective {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : Function.Injective fun (v : V) => J.holomorphicProjection (1 ⊗ₜ[ℝ] v)

Projection to (1,0) vectors is injective on the embedded real vector space.