Transporting almost complex structures along linear equivalences

A real-linear isomorphism e : V ≃ₗ[ℝ] W carries an almost complex structure J on V to one on W by conjugation, w ↦ e (J (e.symm w)). This file records that transport and its functoriality, and packages the statement that e itself is then a complex-linear isomorphism between (V, J) and (W, J.transport e).

This is the pointwise linear algebra behind the corresponding bundle-level and J-holomorphic naturality: an almost complex structure on a vector bundle is given fiberwise, and a change of trivialization acts on each fiber by exactly this conjugation. The capstone isComplexLinearMap_arrowCongr_iff says that complex-linearity of a linear map is preserved and reflected when both source and target are transported.

Main declarations

• TauCeti.AlmostComplexStructure.transport: the almost complex structure e.conj J on W, obtained by conjugating J with e : V ≃ₗ[ℝ] W.
• TauCeti.AlmostComplexStructure.transport_refl / transport_trans: functoriality of transport in the linear equivalence.
• TauCeti.AlmostComplexStructure.isComplexLinearMap_transport: the equivalence e is complex-linear from J to J.transport e.
• TauCeti.IsComplexLinearMap.arrowCongr: complex-linearity transports along a pair of linear equivalences applied to the source and target.
• LinearEquiv.isComplexLinearMap_transport_symm_iff: complex-linearity of e ∘ F is complex-linearity of F for the structure carried back along e.

The conjugation LinearEquiv.conj and LinearEquiv.arrowCongr are reused from Mathlib; the almost complex structure layer is TauCeti.AlmostComplexStructure.

def TauCeti.AlmostComplexStructure.transport {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : AlmostComplexStructure V) (e : V ≃ₗ[ℝ] W) : AlmostComplexStructure W

Transport an almost complex structure along a real-linear equivalence by conjugation.

The transported endomorphism is LinearEquiv.conj e applied to J, equivalently w ↦ e (J (e.symm w)), and it satisfies the almost-complex square condition.

@[simp]

theorem TauCeti.AlmostComplexStructure.transport_toLinearMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : AlmostComplexStructure V) (e : V ≃ₗ[ℝ] W) : (J.transport e).toLinearMap = e.conj J.toLinearMap

@[simp]

theorem TauCeti.AlmostComplexStructure.transport_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : AlmostComplexStructure V) (e : V ≃ₗ[ℝ] W) (w : W) : (J.transport e).toLinearMap w = e (J.toLinearMap (e.symm w))

@[simp]

theorem TauCeti.AlmostComplexStructure.transport_refl {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : J.transport (LinearEquiv.refl ℝ V) = J

Transporting along the identity equivalence does nothing.

@[simp]

theorem TauCeti.AlmostComplexStructure.transport_trans {V : Type u_1} {W : Type u_2} {X : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup X] [Module ℝ X] (J : AlmostComplexStructure V) (e₁ : V ≃ₗ[ℝ] W) (e₂ : W ≃ₗ[ℝ] X) : (J.transport e₁).transport e₂ = J.transport (e₁ ≪≫ₗ e₂)

Transport is functorial: transporting along e₁ then e₂ is transporting along their composite.

theorem TauCeti.AlmostComplexStructure.transport_symm_transport {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : AlmostComplexStructure V) (e : V ≃ₗ[ℝ] W) : (J.transport e).transport e.symm = J

Transporting forward along e and back along e.symm returns the original structure.

theorem TauCeti.AlmostComplexStructure.transport_transport_symm {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : AlmostComplexStructure W) (e : V ≃ₗ[ℝ] W) : (J.transport e.symm).transport e = J

Transporting back along e.symm and forward along e returns the original structure.

@[simp]

theorem TauCeti.AlmostComplexStructure.transport_neg {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : AlmostComplexStructure V) (e : V ≃ₗ[ℝ] W) : (-J).transport e = -J.transport e

Transport commutes with negation of the almost complex structure.

@[simp]

theorem TauCeti.AlmostComplexStructure.isComplexLinearMap_transport {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : AlmostComplexStructure V) (e : V ≃ₗ[ℝ] W) : IsComplexLinearMap J (J.transport e) ↑e

A linear equivalence is complex-linear from J to its transport J.transport e.

@[simp]

theorem TauCeti.AlmostComplexStructure.isComplexLinearMap_symm_transport {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J : AlmostComplexStructure V) (e : V ≃ₗ[ℝ] W) : IsComplexLinearMap (J.transport e) J ↑e.symm

The inverse equivalence is complex-linear from J.transport e back to J.

@[simp]

theorem TauCeti.isComplexLinearMap_arrowCongr_iff {V₁ : Type u_4} {V₂ : Type u_5} {W₁ : Type u_6} {W₂ : Type u_7} [AddCommGroup V₁] [Module ℝ V₁] [AddCommGroup V₂] [Module ℝ V₂] [AddCommGroup W₁] [Module ℝ W₁] [AddCommGroup W₂] [Module ℝ W₂] {J : AlmostComplexStructure V₁} {J' : AlmostComplexStructure W₁} {F : V₁ →ₗ[ℝ] W₁} (eV : V₁ ≃ₗ[ℝ] V₂) (eW : W₁ ≃ₗ[ℝ] W₂) : IsComplexLinearMap (J.transport eV) (J'.transport eW) ((eV.arrowCongr eW) F) ↔ IsComplexLinearMap J J' F

Complex-linearity is preserved and reflected when source, target, and map are transported along linear equivalences.

theorem TauCeti.IsComplexLinearMap.arrowCongr {V₁ : Type u_4} {V₂ : Type u_5} {W₁ : Type u_6} {W₂ : Type u_7} [AddCommGroup V₁] [Module ℝ V₁] [AddCommGroup V₂] [Module ℝ V₂] [AddCommGroup W₁] [Module ℝ W₁] [AddCommGroup W₂] [Module ℝ W₂] {J : AlmostComplexStructure V₁} {J' : AlmostComplexStructure W₁} {F : V₁ →ₗ[ℝ] W₁} (hF : IsComplexLinearMap J J' F) (eV : V₁ ≃ₗ[ℝ] V₂) (eW : W₁ ≃ₗ[ℝ] W₂) : IsComplexLinearMap (J.transport eV) (J'.transport eW) ((eV.arrowCongr eW) F)

Complex-linearity transports along a pair of linear equivalences: if F intertwines J and J', then conjugating F by eV on the source and eW on the target intertwines the transported structures.

theorem LinearEquiv.isComplexLinearMap_transport_symm_iff {V₁ : Type u_1} {W₁ : Type u_2} {W₂ : Type u_3} [AddCommGroup V₁] [Module ℝ V₁] [AddCommGroup W₁] [Module ℝ W₁] [AddCommGroup W₂] [Module ℝ W₂] {J : TauCeti.AlmostComplexStructure V₁} {J' : TauCeti.AlmostComplexStructure W₂} {F : V₁ →ₗ[ℝ] W₁} (e : W₁ ≃ₗ[ℝ] W₂) : TauCeti.IsComplexLinearMap J (J'.transport e.symm) F ↔ TauCeti.IsComplexLinearMap J J' (↑e ∘ₗ F)

A map F is complex-linear for the structure J'.transport e.symm, carried back along a linear equivalence e, exactly when e ∘ F is complex-linear for J'.