Complexification of almost complex structures

An almost complex structure on a real vector space extends complex-linearly to its complexification. Its square remains -1, and its i- and -i-eigenspaces are complementary. These complementary eigenspaces supply the two pieces used to construct a weight-one Hodge structure from the real almost complex structure. A real vector v decomposes as 1 ⊗ v = v^(1,0) + v^(0,1), with v^(1,0) = (v - i J v) / 2 in the i-eigenspace and v^(0,1) = (v + i J v) / 2 in the -i-eigenspace.

A real bilinear map B : V → V → V anti-commuting with J in each argument, such as the Nijenhuis tensor of an almost complex structure on a manifold, has a complex-bilinear extension LinearMap.BilinMap.baseChange ℂ B. It anti-commutes with the complexified complex structure in each argument, so it maps eigenvectors for ±i in either argument into the eigenspace for ∓i. Hence it sends two vectors of type (0,1) to a vector of type (1,0), two vectors of type (1,0) to a vector of type (0,1), and vanishes on a vector of type (1,0) and one of type (0,1).

A real-linear map l : V → N into a complex vector space extends complex-linearly to the complexification by LinearMap.liftBaseChange. It is complex-linear for J exactly when its extension vanishes on the vectors of type (0,1), and conjugate-linear exactly when its extension vanishes on the vectors of type (1,0).

Main declarations

• TauCeti.AlmostComplexStructure.isCompl_eigenspace_baseChange_I_neg_I: its i- and -i-eigenspaces are complementary.
• TauCeti.AlmostComplexStructure.holomorphicPart and TauCeti.AlmostComplexStructure.antiholomorphicPart: the components v^(1,0) and v^(0,1) of a real vector, with TauCeti.AlmostComplexStructure.holomorphicPart_mem_eigenspace_baseChange_I, TauCeti.AlmostComplexStructure.antiholomorphicPart_mem_eigenspace_baseChange_neg_I and TauCeti.AlmostComplexStructure.holomorphicPart_add_antiholomorphicPart.
• TauCeti.AlmostComplexStructure.holomorphicPart_injective and TauCeti.AlmostComplexStructure.range_holomorphicPart, with their (0,1) counterparts: taking the (1,0)-part is a real-linear isomorphism of V onto the i-eigenspace, and taking the (0,1)-part one onto the -i-eigenspace.
• TauCeti.AlmostComplexStructure.baseChange_holomorphicPart and TauCeti.AlmostComplexStructure.baseChange_antiholomorphicPart: the complexified complex structure commutes with taking the (1,0)- and (0,1)-parts.
• TauCeti.AlmostComplexStructure.one_tmul_add_I_tmul_mem_eigenspace_baseChange_I_iff and TauCeti.AlmostComplexStructure.one_tmul_add_I_tmul_mem_eigenspace_baseChange_neg_I_iff: the vector 1 ⊗ v + I ⊗ w has type (1,0) exactly when w = -J v, and type (0,1) exactly when w = J v.
• TauCeti.AlmostComplexStructure.eigenspace_neg_baseChange_I: the vectors of type (1,0) for -J are the vectors of type (0,1) for J.
• TauCeti.AlmostComplexStructure.tmulConj_holomorphicPart and TauCeti.AlmostComplexStructure.tmulConj_antiholomorphicPart: conjugation of the complexification exchanges the (1,0)- and (0,1)-parts.
• TauCeti.AlmostComplexStructure.bilinMap_baseChange_baseChange_left and TauCeti.AlmostComplexStructure.bilinMap_baseChange_baseChange_right: the complex-bilinear extension of a bilinear map anti-commuting with J anti-commutes with the complexified J.
• TauCeti.AlmostComplexStructure.bilinMap_baseChange_mem_eigenspace_neg_of_mem_left and TauCeti.AlmostComplexStructure.bilinMap_baseChange_mem_eigenspace_neg_of_mem_right: the complex-bilinear extension of a bilinear map anti-commuting with J maps eigenvectors for μ in either argument into the eigenspace for -μ.
• TauCeti.AlmostComplexStructure.bilinMap_baseChange_eq_zero_of_mem_eigenspace_I_of_mem_neg_I: it vanishes on a vector of type (1,0) and one of type (0,1).
• TauCeti.AlmostComplexStructure.bilinMap_baseChange_antiholomorphicPart_antiholomorphicPart and TauCeti.AlmostComplexStructure.bilinMap_baseChange_holomorphicPart_holomorphicPart: B(v^(0,1), w^(0,1)) = (B v w)^(1,0) and B(v^(1,0), w^(1,0)) = (B v w)^(0,1).
• TauCeti.AlmostComplexStructure.eigenspace_neg_I_le_ker_liftBaseChange_iff and TauCeti.AlmostComplexStructure.eigenspace_I_le_ker_liftBaseChange_iff: complex-linear and conjugate-linear maps through their complex-linear extensions.

theorem TauCeti.AlmostComplexStructure.baseChange_comp_self {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : LinearMap.baseChange ℂ J.toLinearMap ∘ₗ LinearMap.baseChange ℂ J.toLinearMap = -LinearMap.id

The complex-linear extension of an almost complex structure squares to minus the identity.

theorem TauCeti.AlmostComplexStructure.isCompl_eigenspace_baseChange_I_neg_I {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : IsCompl (Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I) (Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-Complex.I))

The i- and -i-eigenspaces of the complexification of an almost complex structure are complementary.

The (1,0) and (0,1) parts of a real vector

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

The (1,0)-part v^(1,0) = (v - i J v) / 2 of a real vector v, the component of 1 ⊗ v in the i-eigenspace of the complexified complex structure.

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

The (0,1)-part v^(0,1) = (v + i J v) / 2 of a real vector v, the component of 1 ⊗ v in the -i-eigenspace of the complexified complex structure.

theorem TauCeti.AlmostComplexStructure.holomorphicPart_apply {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : J.holomorphicPart v = 2⁻¹ • (1 ⊗ₜ[ℝ] v - Complex.I • 1 ⊗ₜ[ℝ] J.toLinearMap v)

theorem TauCeti.AlmostComplexStructure.antiholomorphicPart_apply {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : J.antiholomorphicPart v = 2⁻¹ • (1 ⊗ₜ[ℝ] v + Complex.I • 1 ⊗ₜ[ℝ] J.toLinearMap v)

@[simp]

theorem TauCeti.AlmostComplexStructure.holomorphicPart_add_antiholomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : J.holomorphicPart v + J.antiholomorphicPart v = 1 ⊗ₜ[ℝ] v

A real vector is the sum of its (1,0)- and (0,1)-parts.

@[simp]

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

The (1,0)-part of J v is i times the (1,0)-part of v.

@[simp]

theorem TauCeti.AlmostComplexStructure.antiholomorphicPart_apply_apply {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : J.antiholomorphicPart (J.toLinearMap v) = -Complex.I • J.antiholomorphicPart v

The (0,1)-part of J v is -i times the (0,1)-part of v.

@[simp]

theorem TauCeti.AlmostComplexStructure.baseChange_holomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : (LinearMap.baseChange ℂ J.toLinearMap) (J.holomorphicPart v) = J.holomorphicPart (J.toLinearMap v)

The complexified complex structure maps the (1,0)-part of v to the (1,0)-part of J v.

@[simp]

theorem TauCeti.AlmostComplexStructure.baseChange_antiholomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : (LinearMap.baseChange ℂ J.toLinearMap) (J.antiholomorphicPart v) = J.antiholomorphicPart (J.toLinearMap v)

The complexified complex structure maps the (0,1)-part of v to the (0,1)-part of J v.

theorem TauCeti.AlmostComplexStructure.holomorphicPart_mem_eigenspace_baseChange_I {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : J.holomorphicPart v ∈ Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I

The (1,0)-part of a real vector lies in the i-eigenspace of the complexified complex structure.

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

The (0,1)-part of a real vector lies in the -i-eigenspace of the complexified complex structure.

Vectors of type (1,0) and (0,1) in real coordinates

theorem TauCeti.AlmostComplexStructure.one_tmul_add_I_tmul_mem_eigenspace_baseChange_I_iff {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v w : V) : 1 ⊗ₜ[ℝ] v + Complex.I ⊗ₜ[ℝ] w ∈ Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I ↔ w = -J.toLinearMap v

The vector 1 ⊗ v + I ⊗ w of the complexification has type (1,0), that is, lies in the i-eigenspace of the complexified complex structure, exactly when w = -J v.

theorem TauCeti.AlmostComplexStructure.one_tmul_add_I_tmul_mem_eigenspace_baseChange_neg_I_iff {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v w : V) : 1 ⊗ₜ[ℝ] v + Complex.I ⊗ₜ[ℝ] w ∈ Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-Complex.I) ↔ w = J.toLinearMap v

The vector 1 ⊗ v + I ⊗ w of the complexification has type (0,1), that is, lies in the -i-eigenspace of the complexified complex structure, exactly when w = J v.

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

The vectors of type (1,0) for -J are the vectors of type (0,1) for J.

Real and imaginary parts of the (1,0) and (0,1) parts

@[simp]

theorem TauCeti.AlmostComplexStructure.realPart_holomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : (realPart V) (J.holomorphicPart v) = 2⁻¹ • v

The real part of v^(1,0) is v / 2.

@[simp]

theorem TauCeti.AlmostComplexStructure.imaginaryPart_holomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : (imaginaryPart V) (J.holomorphicPart v) = -(2⁻¹ • J.toLinearMap v)

The imaginary part of v^(1,0) is -J v / 2.

@[simp]

theorem TauCeti.AlmostComplexStructure.realPart_antiholomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : (realPart V) (J.antiholomorphicPart v) = 2⁻¹ • v

The real part of v^(0,1) is v / 2.

@[simp]

theorem TauCeti.AlmostComplexStructure.imaginaryPart_antiholomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : (imaginaryPart V) (J.antiholomorphicPart v) = 2⁻¹ • J.toLinearMap v

The imaginary part of v^(0,1) is J v / 2.

theorem TauCeti.AlmostComplexStructure.holomorphicPart_injective {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : Function.Injective ⇑J.holomorphicPart

A real vector is determined by its (1,0)-part.

theorem TauCeti.AlmostComplexStructure.antiholomorphicPart_injective {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : Function.Injective ⇑J.antiholomorphicPart

A real vector is determined by its (0,1)-part.

theorem TauCeti.AlmostComplexStructure.range_holomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : J.holomorphicPart.range = Submodule.restrictScalars ℝ (Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I)

The (1,0)-parts of real vectors are exactly the vectors of type (1,0): taking the (1,0)-part is a real-linear isomorphism of V onto the i-eigenspace of the complexified complex structure.

theorem TauCeti.AlmostComplexStructure.range_antiholomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : J.antiholomorphicPart.range = Submodule.restrictScalars ℝ (Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-Complex.I))

The (0,1)-parts of real vectors are exactly the vectors of type (0,1): taking the (0,1)-part is a real-linear isomorphism of V onto the -i-eigenspace of the complexified complex structure.

Conjugation of the (1,0) and (0,1) parts

@[simp]

theorem TauCeti.AlmostComplexStructure.tmulConj_holomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : (tmulConj V) (J.holomorphicPart v) = J.antiholomorphicPart v

Conjugation of the complexification maps the (1,0)-part of a real vector to its (0,1)-part.

@[simp]

theorem TauCeti.AlmostComplexStructure.tmulConj_antiholomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (v : V) : (tmulConj V) (J.antiholomorphicPart v) = J.holomorphicPart v

Conjugation of the complexification maps the (0,1)-part of a real vector to its (1,0)-part.

Bilinear maps anti-commuting with the complex structure

A real bilinear map B : V → V → V with B (J v) w = -J (B v w) and B v (J w) = -J (B v w), such as the Nijenhuis tensor of an almost complex structure, has a complex-bilinear extension to the complexification that sends two vectors of type (0,1) to a vector of type (1,0), two vectors of type (1,0) to a vector of type (0,1), and vanishes on a vector of type (1,0) and one of type (0,1). Here a vector of type (1,0) or (0,1) is one in the i- or -i-eigenspace of the complexified complex structure.

theorem TauCeti.AlmostComplexStructure.bilinMap_baseChange_baseChange_left {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {B : LinearMap.BilinMap ℝ V V} (hl : ∀ (v w : V), (B (J.toLinearMap v)) w = -J.toLinearMap ((B v) w)) (X Y : TensorProduct ℝ ℂ V) : ((LinearMap.BilinMap.baseChange ℂ B) ((LinearMap.baseChange ℂ J.toLinearMap) X)) Y = -(LinearMap.baseChange ℂ J.toLinearMap) (((LinearMap.BilinMap.baseChange ℂ B) X) Y)

The complex-bilinear extension of a bilinear map anti-commuting with J in its first argument anti-commutes with the complexified complex structure in its first argument.

theorem TauCeti.AlmostComplexStructure.bilinMap_baseChange_baseChange_right {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {B : LinearMap.BilinMap ℝ V V} (hr : ∀ (v w : V), (B v) (J.toLinearMap w) = -J.toLinearMap ((B v) w)) (X Y : TensorProduct ℝ ℂ V) : ((LinearMap.BilinMap.baseChange ℂ B) X) ((LinearMap.baseChange ℂ J.toLinearMap) Y) = -(LinearMap.baseChange ℂ J.toLinearMap) (((LinearMap.BilinMap.baseChange ℂ B) X) Y)

The complex-bilinear extension of a bilinear map anti-commuting with J in its second argument anti-commutes with the complexified complex structure in its second argument.

theorem TauCeti.AlmostComplexStructure.bilinMap_baseChange_mem_eigenspace_neg_of_mem_left {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {B : LinearMap.BilinMap ℝ V V} (hl : ∀ (v w : V), (B (J.toLinearMap v)) w = -J.toLinearMap ((B v) w)) {μ : ℂ} {X : TensorProduct ℝ ℂ V} (hX : X ∈ Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) μ) (Y : TensorProduct ℝ ℂ V) : ((LinearMap.BilinMap.baseChange ℂ B) X) Y ∈ Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-μ)

If a bilinear map anti-commutes with J in its first argument, its complex-bilinear extension maps an eigenvector of the complexified complex structure for the eigenvalue μ in its first argument into the eigenspace for -μ.

theorem TauCeti.AlmostComplexStructure.bilinMap_baseChange_mem_eigenspace_neg_of_mem_right {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {B : LinearMap.BilinMap ℝ V V} (hr : ∀ (v w : V), (B v) (J.toLinearMap w) = -J.toLinearMap ((B v) w)) (X : TensorProduct ℝ ℂ V) {μ : ℂ} {Y : TensorProduct ℝ ℂ V} (hY : Y ∈ Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) μ) : ((LinearMap.BilinMap.baseChange ℂ B) X) Y ∈ Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-μ)

If a bilinear map anti-commutes with J in its second argument, its complex-bilinear extension maps an eigenvector of the complexified complex structure for the eigenvalue μ in its second argument into the eigenspace for -μ.

theorem TauCeti.AlmostComplexStructure.bilinMap_baseChange_eq_zero_of_mem_eigenspace_I_of_mem_neg_I {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {B : LinearMap.BilinMap ℝ V V} (hl : ∀ (v w : V), (B (J.toLinearMap v)) w = -J.toLinearMap ((B v) w)) (hr : ∀ (v w : V), (B v) (J.toLinearMap w) = -J.toLinearMap ((B v) w)) {X Y : TensorProduct ℝ ℂ V} (hX : X ∈ Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I) (hY : Y ∈ Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-Complex.I)) : ((LinearMap.BilinMap.baseChange ℂ B) X) Y = 0

The complex-bilinear extension of a bilinear map anti-commuting with J in each argument vanishes on a vector of type (1,0) and a vector of type (0,1).

theorem TauCeti.AlmostComplexStructure.bilinMap_baseChange_eq_zero_of_mem_eigenspace_neg_I_of_mem_I {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {B : LinearMap.BilinMap ℝ V V} (hl : ∀ (v w : V), (B (J.toLinearMap v)) w = -J.toLinearMap ((B v) w)) (hr : ∀ (v w : V), (B v) (J.toLinearMap w) = -J.toLinearMap ((B v) w)) {X Y : TensorProduct ℝ ℂ V} (hX : X ∈ Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-Complex.I)) (hY : Y ∈ Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I) : ((LinearMap.BilinMap.baseChange ℂ B) X) Y = 0

The complex-bilinear extension of a bilinear map anti-commuting with J in each argument vanishes on a vector of type (0,1) and a vector of type (1,0).

theorem TauCeti.AlmostComplexStructure.bilinMap_baseChange_holomorphicPart_antiholomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {B : LinearMap.BilinMap ℝ V V} (hl : ∀ (v w : V), (B (J.toLinearMap v)) w = -J.toLinearMap ((B v) w)) (hr : ∀ (v w : V), (B v) (J.toLinearMap w) = -J.toLinearMap ((B v) w)) (v w : V) : ((LinearMap.BilinMap.baseChange ℂ B) (J.holomorphicPart v)) (J.antiholomorphicPart w) = 0

The complex-bilinear extension of a bilinear map anti-commuting with J in each argument vanishes on the (1,0)-part of v and the (0,1)-part of w.

theorem TauCeti.AlmostComplexStructure.bilinMap_baseChange_antiholomorphicPart_holomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {B : LinearMap.BilinMap ℝ V V} (hl : ∀ (v w : V), (B (J.toLinearMap v)) w = -J.toLinearMap ((B v) w)) (hr : ∀ (v w : V), (B v) (J.toLinearMap w) = -J.toLinearMap ((B v) w)) (v w : V) : ((LinearMap.BilinMap.baseChange ℂ B) (J.antiholomorphicPart v)) (J.holomorphicPart w) = 0

The complex-bilinear extension of a bilinear map anti-commuting with J in each argument vanishes on the (0,1)-part of v and the (1,0)-part of w.

theorem TauCeti.AlmostComplexStructure.bilinMap_baseChange_antiholomorphicPart_antiholomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {B : LinearMap.BilinMap ℝ V V} (hl : ∀ (v w : V), (B (J.toLinearMap v)) w = -J.toLinearMap ((B v) w)) (hr : ∀ (v w : V), (B v) (J.toLinearMap w) = -J.toLinearMap ((B v) w)) (v w : V) : ((LinearMap.BilinMap.baseChange ℂ B) (J.antiholomorphicPart v)) (J.antiholomorphicPart w) = J.holomorphicPart ((B v) w)

The complex-bilinear extension of a bilinear map anti-commuting with J in each argument maps the (0,1)-parts of v and w to the (1,0)-part of B v w.

theorem TauCeti.AlmostComplexStructure.bilinMap_baseChange_holomorphicPart_holomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {B : LinearMap.BilinMap ℝ V V} (hl : ∀ (v w : V), (B (J.toLinearMap v)) w = -J.toLinearMap ((B v) w)) (hr : ∀ (v w : V), (B v) (J.toLinearMap w) = -J.toLinearMap ((B v) w)) (v w : V) : ((LinearMap.BilinMap.baseChange ℂ B) (J.holomorphicPart v)) (J.holomorphicPart w) = J.antiholomorphicPart ((B v) w)

The complex-bilinear extension of a bilinear map anti-commuting with J in each argument maps the (1,0)-parts of v and w to the (0,1)-part of B v w.

Complex-linear extensions of real-linear maps

A real-linear map l : V → N into a complex vector space extends complex-linearly to the complexification by LinearMap.liftBaseChange. The map l is complex-linear for J, l (J v) = i • l v, exactly when its extension vanishes on the vectors of type (0,1), and conjugate-linear, l (J v) = -i • l v, exactly when it vanishes on the vectors of type (1,0).

@[simp]

theorem TauCeti.AlmostComplexStructure.liftBaseChange_holomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {N : Type u_1} [AddCommGroup N] [Module ℂ N] [Module ℝ N] [IsScalarTower ℝ ℂ N] (l : V →ₗ[ℝ] N) (v : V) : (LinearMap.liftBaseChange ℂ l) (J.holomorphicPart v) = 2⁻¹ • (l v - Complex.I • l (J.toLinearMap v))

The complex-linear extension of l on the (1,0)-part of v is (l v - i • l (J v)) / 2.

@[simp]

theorem TauCeti.AlmostComplexStructure.liftBaseChange_antiholomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {N : Type u_1} [AddCommGroup N] [Module ℂ N] [Module ℝ N] [IsScalarTower ℝ ℂ N] (l : V →ₗ[ℝ] N) (v : V) : (LinearMap.liftBaseChange ℂ l) (J.antiholomorphicPart v) = 2⁻¹ • (l v + Complex.I • l (J.toLinearMap v))

The complex-linear extension of l on the (0,1)-part of v is (l v + i • l (J v)) / 2.

theorem TauCeti.AlmostComplexStructure.eigenspace_neg_I_le_ker_liftBaseChange_iff {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {N : Type u_1} [AddCommGroup N] [Module ℂ N] [Module ℝ N] [IsScalarTower ℝ ℂ N] (l : V →ₗ[ℝ] N) : Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-Complex.I) ≤ (LinearMap.liftBaseChange ℂ l).ker ↔ ∀ (v : V), l (J.toLinearMap v) = Complex.I • l v

A real-linear map is complex-linear for J exactly when its complex-linear extension vanishes on the vectors of type (0,1).

theorem TauCeti.AlmostComplexStructure.eigenspace_I_le_ker_liftBaseChange_iff {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {N : Type u_1} [AddCommGroup N] [Module ℂ N] [Module ℝ N] [IsScalarTower ℝ ℂ N] (l : V →ₗ[ℝ] N) : Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I ≤ (LinearMap.liftBaseChange ℂ l).ker ↔ ∀ (v : V), l (J.toLinearMap v) = -Complex.I • l v

A real-linear map is conjugate-linear for J exactly when its complex-linear extension vanishes on the vectors of type (1,0).