Complex-linear and complex-antilinear parts of a real-linear map

Fix real vector spaces (or modules) V and W equipped with almost complex structures, that is, real-linear endomorphisms J : V →ₗ[ℝ] V and J' : W →ₗ[ℝ] W with J ∘ J = -1 and J' ∘ J' = -1. A real-linear map F : V →ₗ[ℝ] W is complex linear (with respect to the pair (J, J')) when it commutes with the structures, F ∘ J = J' ∘ F, and complex antilinear when it anticommutes, F ∘ J = -(J' ∘ F).

Every real-linear map splits canonically as the sum of a complex-linear and a complex-antilinear map,

F = complexLinearPart J J' F + complexAntilinearPart J J' F,

with complexLinearPart J J' F = ½ (F - J' ∘ F ∘ J) and complexAntilinearPart J J' F = ½ (F + J' ∘ F ∘ J). This is the pointwise linearization at the heart of the holomorphic theory: a smooth map between almost complex manifolds is J-holomorphic exactly when its differential is complex linear, equivalently when its complex-antilinear part ∂̄ vanishes. This file develops the linear-algebra layer of that statement, before any smoothness or bundle structure is introduced.

Main definitions

• TauCeti.IsComplexLinear J J' F: the commutation condition F ∘ J = J' ∘ F.
• TauCeti.IsComplexAntilinear J J' F: the anticommutation condition F ∘ J = -(J' ∘ F).
• TauCeti.complexLinearPart J J' F: the complex-linear part ½ (F - J' ∘ F ∘ J) (the ∂ operator).
• TauCeti.complexAntilinearPart J J' F: the complex-antilinear part ½ (F + J' ∘ F ∘ J) (the ∂̄ operator).
• TauCeti.complexLinearPartLinearMap J J' / TauCeti.complexAntilinearPartLinearMap J J': the corresponding real-linear operators on V →ₗ[ℝ] W (these become genuine projections only under J ∘ J = -1 and J' ∘ J' = -1).
• TauCeti.complexLinearMaps J J' / TauCeti.complexAntilinearMaps J J': the real subspaces of complex-linear and complex-antilinear maps.

Main results

• TauCeti.complexLinearPart_add_complexAntilinearPart: the decomposition ∂ + ∂̄ = id.
• TauCeti.complexLinearPart_isComplexLinear / TauCeti.complexAntilinearPart_isComplexAntilinear: the two parts land in their named classes.
• TauCeti.isComplexLinear_iff_complexAntilinearPart_eq_zero: F is complex linear iff its complex-antilinear part vanishes (the ∂̄ F = 0 characterization).
• TauCeti.isCompl_complexLinearMaps: the complex-linear and complex-antilinear maps are complementary subspaces of all real-linear maps.
• TauCeti.isComplexLinear_arrowCongr_iff: complex-linearity is preserved and reflected by conjugating source, target, and map along real-linear equivalences.

The sign conventions follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Section 2.2, specialized to the pointwise real-linear setting.

def TauCeti.IsComplexLinear {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (F : V →ₗ[ℝ] W) : Prop

A real-linear map F : V →ₗ[ℝ] W is complex linear for the pair of almost complex structures (J, J') when it intertwines them: F ∘ J = J' ∘ F.

Equations

• TauCeti.IsComplexLinear J J' F = (F ∘ₗ J = J' ∘ₗ F)

def TauCeti.IsComplexAntilinear {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (F : V →ₗ[ℝ] W) : Prop

A real-linear map F : V →ₗ[ℝ] W is complex antilinear for the pair of almost complex structures (J, J') when it anti-intertwines them: F ∘ J = -(J' ∘ F).

Equations

• TauCeti.IsComplexAntilinear J J' F = (F ∘ₗ J = -J' ∘ₗ F)

@[simp]

theorem TauCeti.isComplexLinear_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} : IsComplexLinear J J' F ↔ F ∘ₗ J = J' ∘ₗ F

Complex linearity restated as its defining commutation equation F ∘ J = J' ∘ F.

@[simp]

theorem TauCeti.isComplexAntilinear_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} : IsComplexAntilinear J J' F ↔ F ∘ₗ J = -J' ∘ₗ F

Complex antilinearity restated as its defining anticommutation equation F ∘ J = -(J' ∘ F).

theorem TauCeti.IsComplexLinear.apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} (h : IsComplexLinear J J' F) (v : V) : F (J v) = J' (F v)

The pointwise form of complex linearity: F (J v) = J' (F v).

theorem TauCeti.isComplexLinear_of_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} (h : ∀ (v : V), F (J v) = J' (F v)) : IsComplexLinear J J' F

A real-linear map intertwining J and J' pointwise is complex linear.

@[simp]

theorem TauCeti.isComplexLinear_arrowCongr_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {V₂ : Type u_4} {W₂ : Type u_5} [AddCommGroup V₂] [Module ℝ V₂] [AddCommGroup W₂] [Module ℝ W₂] {F : V →ₗ[ℝ] W} (eV : V ≃ₗ[ℝ] V₂) (eW : W ≃ₗ[ℝ] W₂) : IsComplexLinear (eV.conj J) (eW.conj J') ((eV.arrowCongr eW) F) ↔ IsComplexLinear J J' F

Raw complex-linearity is preserved and reflected by conjugating source and target along linear equivalences.

theorem TauCeti.IsComplexAntilinear.apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} (h : IsComplexAntilinear J J' F) (v : V) : F (J v) = -J' (F v)

The pointwise form of complex antilinearity: F (J v) = -(J' (F v)).

theorem TauCeti.isComplexAntilinear_of_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} (h : ∀ (v : V), F (J v) = -J' (F v)) : IsComplexAntilinear J J' F

A real-linear map anti-intertwining J and J' pointwise is complex antilinear.

theorem TauCeti.isComplexLinear_id {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : V →ₗ[ℝ] V} : IsComplexLinear J J LinearMap.id

The identity map is complex linear.

theorem TauCeti.isComplexLinear_zero {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} : IsComplexLinear J J' 0

The zero map is complex linear.

theorem TauCeti.isComplexAntilinear_zero {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} : IsComplexAntilinear J J' 0

The zero map is complex antilinear.

theorem TauCeti.IsComplexLinear.neg {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} (h : IsComplexLinear J J' F) : IsComplexLinear J J' (-F)

The negation of a complex-linear map is complex linear.

theorem TauCeti.IsComplexLinear.neg_neg {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} (h : IsComplexLinear J J' F) : IsComplexLinear (-J) (-J') F

Complex-linearity is unchanged after negating both source and target endomorphisms.

theorem TauCeti.IsComplexLinear.of_neg_neg {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} (h : IsComplexLinear (-J) (-J') F) : IsComplexLinear J J' F

If a map is complex-linear after negating both endomorphisms, then it was complex-linear before the sign change.

theorem TauCeti.IsComplexAntilinear.neg {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} (h : IsComplexAntilinear J J' F) : IsComplexAntilinear J J' (-F)

The negation of a complex-antilinear map is complex antilinear.

theorem TauCeti.IsComplexAntilinear.neg_neg {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} (h : IsComplexAntilinear J J' F) : IsComplexAntilinear (-J) (-J') F

Complex-antilinearity is unchanged after negating both source and target endomorphisms.

theorem TauCeti.IsComplexAntilinear.of_neg_neg {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} (h : IsComplexAntilinear (-J) (-J') F) : IsComplexAntilinear J J' F

If a map is complex-antilinear after negating both endomorphisms, then it was complex-antilinear before the sign change.

theorem TauCeti.IsComplexLinear.comp {V : Type u_1} {W : Type u_2} {U : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup U] [Module ℝ U] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {J'' : U →ₗ[ℝ] U} {F : V →ₗ[ℝ] W} {G : W →ₗ[ℝ] U} (hG : IsComplexLinear J' J'' G) (hF : IsComplexLinear J J' F) : IsComplexLinear J J'' (G ∘ₗ F)

The composite of two complex-linear maps is complex linear.

theorem TauCeti.IsComplexAntilinear.comp {V : Type u_1} {W : Type u_2} {U : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup U] [Module ℝ U] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {J'' : U →ₗ[ℝ] U} {F : V →ₗ[ℝ] W} {G : W →ₗ[ℝ] U} (hG : IsComplexAntilinear J' J'' G) (hF : IsComplexAntilinear J J' F) : IsComplexLinear J J'' (G ∘ₗ F)

The composite of two complex-antilinear maps is complex linear.

theorem TauCeti.IsComplexLinear.comp_antilinear {V : Type u_1} {W : Type u_2} {U : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup U] [Module ℝ U] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {J'' : U →ₗ[ℝ] U} {F : V →ₗ[ℝ] W} {G : W →ₗ[ℝ] U} (hG : IsComplexLinear J' J'' G) (hF : IsComplexAntilinear J J' F) : IsComplexAntilinear J J'' (G ∘ₗ F)

A complex-linear map after a complex-antilinear map is complex antilinear.

theorem TauCeti.IsComplexAntilinear.comp_linear {V : Type u_1} {W : Type u_2} {U : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup U] [Module ℝ U] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {J'' : U →ₗ[ℝ] U} {F : V →ₗ[ℝ] W} {G : W →ₗ[ℝ] U} (hG : IsComplexAntilinear J' J'' G) (hF : IsComplexLinear J J' F) : IsComplexAntilinear J J'' (G ∘ₗ F)

A complex-antilinear map after a complex-linear map is complex antilinear.

noncomputable def TauCeti.complexLinearPartLinearMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) : (V →ₗ[ℝ] W) →ₗ[ℝ] V →ₗ[ℝ] W

The complex-linear-part operator F ↦ ∂F as a real-linear map on V →ₗ[ℝ] W.

Equations

• TauCeti.complexLinearPartLinearMap J J' = { toFun := fun (F : V →ₗ[ℝ] W) => 2⁻¹ • (F - J' ∘ₗ F ∘ₗ J), map_add' := ⋯, map_smul' := ⋯ }

noncomputable def TauCeti.complexAntilinearPartLinearMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) : (V →ₗ[ℝ] W) →ₗ[ℝ] V →ₗ[ℝ] W

The complex-antilinear-part operator F ↦ ∂̄F as a real-linear map on V →ₗ[ℝ] W.

Equations

• TauCeti.complexAntilinearPartLinearMap J J' = { toFun := fun (F : V →ₗ[ℝ] W) => 2⁻¹ • (F + J' ∘ₗ F ∘ₗ J), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.complexLinearPartLinearMap_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (F : V →ₗ[ℝ] W) : (complexLinearPartLinearMap J J') F = 2⁻¹ • (F - J' ∘ₗ F ∘ₗ J)

The defining formula for complexLinearPartLinearMap J J' on an input map.

@[simp]

theorem TauCeti.complexAntilinearPartLinearMap_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (F : V →ₗ[ℝ] W) : (complexAntilinearPartLinearMap J J') F = 2⁻¹ • (F + J' ∘ₗ F ∘ₗ J)

The defining formula for complexAntilinearPartLinearMap J J' on an input map.

noncomputable def TauCeti.complexLinearPart {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (F : V →ₗ[ℝ] W) : V →ₗ[ℝ] W

The complex-linear part ∂F = ½ (F - J' ∘ F ∘ J) of a real-linear map.

Equations

• TauCeti.complexLinearPart J J' F = (TauCeti.complexLinearPartLinearMap J J') F

noncomputable def TauCeti.complexAntilinearPart {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (F : V →ₗ[ℝ] W) : V →ₗ[ℝ] W

The complex-antilinear part ∂̄F = ½ (F + J' ∘ F ∘ J) of a real-linear map.

Equations

• TauCeti.complexAntilinearPart J J' F = (TauCeti.complexAntilinearPartLinearMap J J') F

theorem TauCeti.complexLinearPart_def {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (F : V →ₗ[ℝ] W) : complexLinearPart J J' F = 2⁻¹ • (F - J' ∘ₗ F ∘ₗ J)

The defining formula for the complex-linear part as a linear-map equality.

theorem TauCeti.complexAntilinearPart_def {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (F : V →ₗ[ℝ] W) : complexAntilinearPart J J' F = 2⁻¹ • (F + J' ∘ₗ F ∘ₗ J)

The defining formula for the complex-antilinear part as a linear-map equality.

@[simp]

theorem TauCeti.complexLinearPart_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (F : V →ₗ[ℝ] W) (v : V) : (complexLinearPart J J' F) v = 2⁻¹ • (F v - J' (F (J v)))

The pointwise formula for the complex-linear part: ∂F v = 1/2 • (F v - J' (F (J v))).

@[simp]

theorem TauCeti.complexAntilinearPart_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (F : V →ₗ[ℝ] W) (v : V) : (complexAntilinearPart J J' F) v = 2⁻¹ • (F v + J' (F (J v)))

The pointwise formula for the complex-antilinear part: ∂̄F v = 1/2 • (F v + J' (F (J v))).

@[simp]

theorem TauCeti.complexLinearPart_add_complexAntilinearPart {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (F : V →ₗ[ℝ] W) : complexLinearPart J J' F + complexAntilinearPart J J' F = F

The canonical decomposition ∂F + ∂̄F = F.

@[simp]

theorem TauCeti.complexLinearPartLinearMap_add_complexAntilinearPartLinearMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) : complexLinearPartLinearMap J J' + complexAntilinearPartLinearMap J J' = LinearMap.id

The complex-linear-part and complex-antilinear-part operators add to the identity.

@[simp]

theorem TauCeti.complexLinearPart_add {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (F G : V →ₗ[ℝ] W) : complexLinearPart J J' (F + G) = complexLinearPart J J' F + complexLinearPart J J' G

The complex-linear part is additive in F.

@[simp]

theorem TauCeti.complexAntilinearPart_add {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (F G : V →ₗ[ℝ] W) : complexAntilinearPart J J' (F + G) = complexAntilinearPart J J' F + complexAntilinearPart J J' G

The complex-antilinear part is additive in F.

@[simp]

theorem TauCeti.complexLinearPart_smul {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (c : ℝ) (F : V →ₗ[ℝ] W) : complexLinearPart J J' (c • F) = c • complexLinearPart J J' F

The complex-linear part commutes with real scalar multiplication in F.

@[simp]

theorem TauCeti.complexAntilinearPart_smul {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (c : ℝ) (F : V →ₗ[ℝ] W) : complexAntilinearPart J J' (c • F) = c • complexAntilinearPart J J' F

The complex-antilinear part commutes with real scalar multiplication in F.

@[simp]

theorem TauCeti.complexLinearPart_zero {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) : complexLinearPart J J' 0 = 0

The complex-linear part of the zero map is zero.

@[simp]

theorem TauCeti.complexAntilinearPart_zero {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) : complexAntilinearPart J J' 0 = 0

The complex-antilinear part of the zero map is zero.

@[simp]

theorem TauCeti.complexLinearPart_neg {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (F : V →ₗ[ℝ] W) : complexLinearPart J J' (-F) = -complexLinearPart J J' F

The complex-linear part commutes with negation in F.

@[simp]

theorem TauCeti.complexAntilinearPart_neg {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) (F : V →ₗ[ℝ] W) : complexAntilinearPart J J' (-F) = -complexAntilinearPart J J' F

The complex-antilinear part commutes with negation in F.

theorem TauCeti.complexLinearPart_isComplexLinear {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} (hJ : J ∘ₗ J = -LinearMap.id) (hJ' : J' ∘ₗ J' = -LinearMap.id) (F : V →ₗ[ℝ] W) : IsComplexLinear J J' (complexLinearPart J J' F)

The complex-linear part really is complex linear.

theorem TauCeti.complexAntilinearPart_isComplexAntilinear {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} (hJ : J ∘ₗ J = -LinearMap.id) (hJ' : J' ∘ₗ J' = -LinearMap.id) (F : V →ₗ[ℝ] W) : IsComplexAntilinear J J' (complexAntilinearPart J J' F)

The complex-antilinear part really is complex antilinear.

theorem TauCeti.isComplexLinear_iff_complexAntilinearPart_eq_zero {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} (hJ' : J' ∘ₗ J' = -LinearMap.id) (F : V →ₗ[ℝ] W) : IsComplexLinear J J' F ↔ complexAntilinearPart J J' F = 0

A real-linear map is complex linear exactly when its complex-antilinear part vanishes: the linear-algebra shadow of "F is J-holomorphic iff ∂̄F = 0".

theorem TauCeti.isComplexAntilinear_iff_complexLinearPart_eq_zero {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} (hJ' : J' ∘ₗ J' = -LinearMap.id) (F : V →ₗ[ℝ] W) : IsComplexAntilinear J J' F ↔ complexLinearPart J J' F = 0

A real-linear map is complex antilinear exactly when its complex-linear part vanishes.

theorem TauCeti.IsComplexLinear.complexLinearPart_eq {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} (h : IsComplexLinear J J' F) (hJ' : J' ∘ₗ J' = -LinearMap.id) : complexLinearPart J J' F = F

A complex-linear map equals its own complex-linear part.

theorem TauCeti.IsComplexLinear.complexAntilinearPart_eq_zero {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} (h : IsComplexLinear J J' F) (hJ' : J' ∘ₗ J' = -LinearMap.id) : complexAntilinearPart J J' F = 0

The complex-antilinear part of a complex-linear map vanishes.

theorem TauCeti.IsComplexAntilinear.complexAntilinearPart_eq {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} (h : IsComplexAntilinear J J' F) (hJ' : J' ∘ₗ J' = -LinearMap.id) : complexAntilinearPart J J' F = F

A complex-antilinear map equals its own complex-antilinear part.

theorem TauCeti.IsComplexAntilinear.complexLinearPart_eq_zero {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} (h : IsComplexAntilinear J J' F) (hJ' : J' ∘ₗ J' = -LinearMap.id) : complexLinearPart J J' F = 0

The complex-linear part of a complex-antilinear map vanishes.

theorem TauCeti.complexLinearPart_eq_and_complexAntilinearPart_eq_of_decomp {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} (hJ' : J' ∘ₗ J' = -LinearMap.id) {F A B : V →ₗ[ℝ] W} (hA : IsComplexLinear J J' A) (hB : IsComplexAntilinear J J' B) (hF : F = A + B) : A = complexLinearPart J J' F ∧ B = complexAntilinearPart J J' F

Uniqueness of the complex-linear/antilinear decomposition: if F = A + B with A complex linear and B complex antilinear, then A and B are the canonical parts of F.

def TauCeti.complexLinearMaps {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) : Submodule ℝ (V →ₗ[ℝ] W)

The real subspace of complex-linear maps V →ₗ[ℝ] W for the pair (J, J').

Equations

• TauCeti.complexLinearMaps J J' = { carrier := {F : V →ₗ[ℝ] W | TauCeti.IsComplexLinear J J' F}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def TauCeti.complexAntilinearMaps {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : V →ₗ[ℝ] V) (J' : W →ₗ[ℝ] W) : Submodule ℝ (V →ₗ[ℝ] W)

The real subspace of complex-antilinear maps V →ₗ[ℝ] W for the pair (J, J').

Equations

• TauCeti.complexAntilinearMaps J J' = { carrier := {F : V →ₗ[ℝ] W | TauCeti.IsComplexAntilinear J J' F}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.mem_complexLinearMaps {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} : F ∈ complexLinearMaps J J' ↔ IsComplexLinear J J' F

@[simp]

theorem TauCeti.mem_complexAntilinearMaps {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} {F : V →ₗ[ℝ] W} : F ∈ complexAntilinearMaps J J' ↔ IsComplexAntilinear J J' F

theorem TauCeti.isCompl_complexLinearMaps {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J : V →ₗ[ℝ] V} {J' : W →ₗ[ℝ] W} (hJ : J ∘ₗ J = -LinearMap.id) (hJ' : J' ∘ₗ J' = -LinearMap.id) : IsCompl (complexLinearMaps J J') (complexAntilinearMaps J J')

For genuine almost complex structures, every real-linear map splits uniquely as a complex-linear plus a complex-antilinear map: the two subspaces are complementary.