Direct sums of almost complex structures and symplectic forms

Given almost complex structures J₁ on V and J₂ on W, the product V × W carries the direct-sum almost complex structure acting componentwise, (v, w) ↦ (J₁ v, J₂ w). Likewise two symplectic forms ω₁, ω₂ assemble into the direct-sum symplectic form (ω₁ ⊕ ω₂)((v₁, w₁), (v₂, w₂)) = ω₁(v₁, v₂) + ω₂(w₁, w₂). This file builds both, records their basic API, and proves the payoff: a direct sum of tame (respectively compatible) pairs is again tame (respectively compatible).

This is the pointwise linear algebra of product symplectic manifolds: the standard model and every fiberwise compatibility argument decomposes over a direct sum. It complements the doubling structure TauCeti.AlmostComplexStructure.product on V × V (which mixes the two coordinates, (x, y) ↦ (-y, x)); the construction here is the componentwise direct sum instead, following Mathlib's LinearMap.prodMap naming convention.

Main declarations

• TauCeti.AlmostComplexStructure.prod: the direct-sum almost complex structure (v, w) ↦ (J₁ v, J₂ w) on V × W.
• TauCeti.AlmostComplexStructure.isComplexLinearMap_inl / isComplexLinearMap_inr / isComplexLinearMap_fst / isComplexLinearMap_snd: the structural maps of the product are complex-linear for the direct-sum structure.
• TauCeti.AlmostComplexStructure.transport_prod: transport distributes over the direct sum.
• TauCeti.IsComplexLinearMap.prod and TauCeti.IsComplexLinearMap.prodMap: complex-linearity is preserved by pairing maps with a common source and by product maps into the direct sum.
• TauCeti.SymplecticForm.prod: the direct-sum symplectic form on V × W.
• TauCeti.SymplecticForm.twistedProd: the twisted product form ω₁ ⊖ ω₂ on V × W, the direct sum with the second factor negated.
• TauCeti.SymplecticForm.prod_invariant, prod_tames, prod_compatible: a direct sum of invariant / tame / compatible pairs is invariant / tame / compatible.

The conventions follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.1, where products of compatible triples model split symplectic vector spaces.

def TauCeti.AlmostComplexStructure.prod {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J₁ : AlmostComplexStructure V) (J₂ : AlmostComplexStructure W) : AlmostComplexStructure (V × W)

The direct-sum almost complex structure on V × W, acting componentwise by (v, w) ↦ (J₁ v, J₂ w).

This is the componentwise direct sum, distinct from the doubling structure AlmostComplexStructure.product on V × V.

@[simp]

theorem TauCeti.AlmostComplexStructure.prod_toLinearMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J₁ : AlmostComplexStructure V) (J₂ : AlmostComplexStructure W) : (J₁.prod J₂).toLinearMap = J₁.toLinearMap.prodMap J₂.toLinearMap

@[simp]

theorem TauCeti.AlmostComplexStructure.prod_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J₁ : AlmostComplexStructure V) (J₂ : AlmostComplexStructure W) (p : V × W) : (J₁.prod J₂).toLinearMap p = (J₁.toLinearMap p.1, J₂.toLinearMap p.2)

@[simp]

theorem TauCeti.AlmostComplexStructure.neg_prod_neg {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J₁ : AlmostComplexStructure V) (J₂ : AlmostComplexStructure W) : (-J₁).prod (-J₂) = -J₁.prod J₂

The direct sum of negations is the negation of the direct sum.

@[simp]

theorem TauCeti.AlmostComplexStructure.isComplexLinearMap_inl {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J₁ : AlmostComplexStructure V) (J₂ : AlmostComplexStructure W) : IsComplexLinearMap J₁ (J₁.prod J₂) (LinearMap.inl ℝ V W)

The inclusion of the first factor is complex-linear into the direct sum.

@[simp]

theorem TauCeti.AlmostComplexStructure.isComplexLinearMap_inr {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J₁ : AlmostComplexStructure V) (J₂ : AlmostComplexStructure W) : IsComplexLinearMap J₂ (J₁.prod J₂) (LinearMap.inr ℝ V W)

The inclusion of the second factor is complex-linear into the direct sum.

@[simp]

theorem TauCeti.AlmostComplexStructure.isComplexLinearMap_fst {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J₁ : AlmostComplexStructure V) (J₂ : AlmostComplexStructure W) : IsComplexLinearMap (J₁.prod J₂) J₁ (LinearMap.fst ℝ V W)

The first projection is complex-linear out of the direct sum.

@[simp]

theorem TauCeti.AlmostComplexStructure.isComplexLinearMap_snd {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (J₁ : AlmostComplexStructure V) (J₂ : AlmostComplexStructure W) : IsComplexLinearMap (J₁.prod J₂) J₂ (LinearMap.snd ℝ V W)

The second projection is complex-linear out of the direct sum.

@[simp]

theorem TauCeti.AlmostComplexStructure.transport_prod {V : Type u_1} {W : Type u_2} {V' : Type u_3} {W' : Type u_4} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup V'] [Module ℝ V'] [AddCommGroup W'] [Module ℝ W'] (J₁ : AlmostComplexStructure V) (J₂ : AlmostComplexStructure W) (e₁ : V ≃ₗ[ℝ] V') (e₂ : W ≃ₗ[ℝ] W') : (J₁.prod J₂).transport (e₁.prodCongr e₂) = (J₁.transport e₁).prod (J₂.transport e₂)

Transport distributes over the direct sum: conjugating a direct sum by a product of equivalences is the direct sum of the conjugates.

theorem TauCeti.IsComplexLinearMap.prod {V : Type u_1} {W : Type u_2} {V' : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup V'] [Module ℝ V'] {J : AlmostComplexStructure V} {J₁ : AlmostComplexStructure W} {J₂ : AlmostComplexStructure V'} {F : V →ₗ[ℝ] W} {G : V →ₗ[ℝ] V'} (hF : IsComplexLinearMap J J₁ F) (hG : IsComplexLinearMap J J₂ G) : IsComplexLinearMap J (J₁.prod J₂) (F.prod G)

A pair of complex-linear maps with the same source is complex-linear into the direct-sum almost complex structure.

theorem TauCeti.IsComplexLinearMap.prodMap {V : Type u_1} {W : Type u_2} {V' : Type u_3} {W' : Type u_4} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup V'] [Module ℝ V'] [AddCommGroup W'] [Module ℝ W'] {J₁ : AlmostComplexStructure V} {J₂ : AlmostComplexStructure W} {K₁ : AlmostComplexStructure V'} {K₂ : AlmostComplexStructure W'} {F : V →ₗ[ℝ] V'} {G : W →ₗ[ℝ] W'} (hF : IsComplexLinearMap J₁ K₁ F) (hG : IsComplexLinearMap J₂ K₂ G) : IsComplexLinearMap (J₁.prod J₂) (K₁.prod K₂) (F.prodMap G)

A product map of complex-linear maps is complex-linear for the direct-sum almost complex structures.

def TauCeti.SymplecticForm.prodBilin {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω₁ : SymplecticForm V) (ω₂ : SymplecticForm W) : LinearMap.BilinForm ℝ (V × W)

The underlying bilinear form of the direct-sum symplectic form.

theorem TauCeti.SymplecticForm.prodBilin_isAlt {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω₁ : SymplecticForm V) (ω₂ : SymplecticForm W) : (ω₁.prodBilin ω₂).IsAlt

theorem TauCeti.SymplecticForm.prodBilin_nondegenerate {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω₁ : SymplecticForm V) (ω₂ : SymplecticForm W) : (ω₁.prodBilin ω₂).Nondegenerate

def TauCeti.SymplecticForm.prod {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω₁ : SymplecticForm V) (ω₂ : SymplecticForm W) : SymplecticForm (V × W)

The direct-sum symplectic form on V × W, given by (ω₁ ⊕ ω₂)((v₁, w₁), (v₂, w₂)) = ω₁(v₁, v₂) + ω₂(w₁, w₂).

@[simp]

theorem TauCeti.SymplecticForm.prod_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω₁ : SymplecticForm V) (ω₂ : SymplecticForm W) (p q : V × W) : (fun (v w : V × W) => ((ω₁.prod ω₂).toBilinForm v) w) p q = (fun (v w : V) => (ω₁.toBilinForm v) w) p.1 q.1 + (fun (v w : W) => (ω₂.toBilinForm v) w) p.2 q.2

noncomputable def TauCeti.SymplecticForm.twistedProd {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω₁ : SymplecticForm V) (ω₂ : SymplecticForm W) : SymplecticForm (V × W)

The twisted product symplectic form ω₁ ⊖ ω₂ on V × W, given by (ω₁ ⊖ ω₂)((v₁, w₁), (v₂, w₂)) = ω₁(v₁, v₂) - ω₂(w₁, w₂).

It is the direct sum prod of ω₁ with the negation ω₂.rescale (-1) of ω₂; the body is @[no_expose], so downstream code uses it through twistedProd_apply rather than by unfolding.

@[simp]

theorem TauCeti.SymplecticForm.twistedProd_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (ω₁ : SymplecticForm V) (ω₂ : SymplecticForm W) (p q : V × W) : (fun (v w : V × W) => ((ω₁.twistedProd ω₂).toBilinForm v) w) p q = (fun (v w : V) => (ω₁.toBilinForm v) w) p.1 q.1 - (fun (v w : W) => (ω₂.toBilinForm v) w) p.2 q.2

@[simp]

theorem TauCeti.SymplecticForm.prod_associatedBilinForm_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J₁ : AlmostComplexStructure V} {J₂ : AlmostComplexStructure W} (ω₁ : SymplecticForm V) (ω₂ : SymplecticForm W) (p q : V × W) : (((ω₁.prod ω₂).associatedBilinForm (J₁.prod J₂)) p) q = ((ω₁.associatedBilinForm J₁) p.1) q.1 + ((ω₂.associatedBilinForm J₂) p.2) q.2

The bilinear form (ω₁ ⊕ ω₂)(·, (J₁ ⊕ J₂) ·) is the direct sum of the factorwise associated forms.

theorem TauCeti.SymplecticForm.prod_apply_prod_self {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J₁ : AlmostComplexStructure V} {J₂ : AlmostComplexStructure W} (ω₁ : SymplecticForm V) (ω₂ : SymplecticForm W) (p : V × W) : (fun (v w : V × W) => ((ω₁.prod ω₂).toBilinForm v) w) p ((J₁.prod J₂).toLinearMap p) = (fun (v w : V) => (ω₁.toBilinForm v) w) p.1 (J₁.toLinearMap p.1) + (fun (v w : W) => (ω₂.toBilinForm v) w) p.2 (J₂.toLinearMap p.2)

(ω₁ ⊕ ω₂)(p, (J₁ ⊕ J₂) p) = ω₁(p.1, J₁ p.1) + ω₂(p.2, J₂ p.2).

theorem TauCeti.SymplecticForm.prod_invariant {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J₁ : AlmostComplexStructure V} {J₂ : AlmostComplexStructure W} {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} (h₁ : ω₁.Invariant J₁) (h₂ : ω₂.Invariant J₂) : (ω₁.prod ω₂).Invariant (J₁.prod J₂)

A direct sum of invariant pairs is invariant.

theorem TauCeti.SymplecticForm.prod_tames {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J₁ : AlmostComplexStructure V} {J₂ : AlmostComplexStructure W} {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} (h₁ : ω₁.Tames J₁) (h₂ : ω₂.Tames J₂) : (ω₁.prod ω₂).Tames (J₁.prod J₂)

A direct sum of tame pairs is tame.

theorem TauCeti.SymplecticForm.prod_compatible {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {J₁ : AlmostComplexStructure V} {J₂ : AlmostComplexStructure W} {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} (h₁ : ω₁.Compatible J₁) (h₂ : ω₂.Compatible J₂) : (ω₁.prod ω₂).Compatible (J₁.prod J₂)

A direct sum of compatible pairs is compatible.