The standard compatible triple on V × V

For a real inner product space V, the doubled space V × V carries a canonical compatible triple (ω, J, g): the standard symplectic form ω₀, the product almost complex structure J(x, y) = (-y, x) from TauCeti.AlmostComplexStructure.product, and the componentwise inner product g recovered as ω₀(·, J ·). When V = ℝ^n, this specializes to the standard model ℝ^{2n} = ℝ^n ⊕ ℝ^n; in general it serves as a non-vacuous witness that the pointwise almost-complex/symplectic definitions of AlmostComplex.lean are inhabited and interact as the standard conventions require.

Main declarations

• TauCeti.stdSymplecticForm: the standard symplectic form ω₀((x₁, y₁), (x₂, y₂)) = ⟪x₁, y₂⟫ - ⟪y₁, x₂⟫ on V × V.
• TauCeti.stdSymplecticForm_invariant_product: ω₀ is invariant under the product almost complex structure J.
• TauCeti.stdSymplecticForm_tames_product: ω₀ tames J, with ω₀(v, J v) = ‖v.1‖² + ‖v.2‖².
• TauCeti.stdSymplecticForm_compatible_product: ω₀ is compatible with J.
• TauCeti.stdSymplecticForm_associatedBilinForm_product: the metric g = ω₀(·, J ·) is the sum of the inner products pulled back from the two factors.

The conventions follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.1, where (ℝ^{2n}, ω₀, J₀) is the standard compatible model.

noncomputable def TauCeti.stdSymplecticForm {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : SymplecticForm (V × V)

The standard symplectic form ω₀((x₁, y₁), (x₂, y₂)) = ⟪x₁, y₂⟫ - ⟪y₁, x₂⟫ on V × V.

@[simp]

theorem TauCeti.stdSymplecticForm_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (u w : V × V) : (fun (v w : V × V) => (stdSymplecticForm.toBilinForm v) w) u w = inner ℝ u.1 w.2 - inner ℝ u.2 w.1

The coordinate formula for evaluating the standard symplectic form on two vectors of V × V.

theorem TauCeti.stdSymplecticForm_invariant_product {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : stdSymplecticForm.Invariant (AlmostComplexStructure.product V)

The standard symplectic form is invariant under the product almost complex structure.

theorem TauCeti.stdSymplecticForm_apply_product_self {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (v : V × V) : (fun (v w : V × V) => (stdSymplecticForm.toBilinForm v) w) v ((AlmostComplexStructure.product V).toLinearMap v) = inner ℝ v.1 v.1 + inner ℝ v.2 v.2

ω₀(v, J v) = ‖v.1‖² + ‖v.2‖² for the product almost complex structure J.

theorem TauCeti.stdSymplecticForm_tames_product {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : stdSymplecticForm.Tames (AlmostComplexStructure.product V)

The standard symplectic form tames the product almost complex structure.

theorem TauCeti.stdSymplecticForm_compatible_product {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : stdSymplecticForm.Compatible (AlmostComplexStructure.product V)

The standard symplectic form is compatible with the product almost complex structure.

theorem TauCeti.stdSymplecticForm_associatedBilinForm_product {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : stdSymplecticForm.associatedBilinForm (AlmostComplexStructure.product V) = (innerₗ V).compl₁₂ (LinearMap.fst ℝ V V) (LinearMap.fst ℝ V V) + (innerₗ V).compl₁₂ (LinearMap.snd ℝ V V) (LinearMap.snd ℝ V V)

The metric g = ω₀(·, J ·) associated to the standard compatible triple is the sum of the inner products pulled back along the two coordinate projections. In particular, g(u, w) = ⟪u.1, w.1⟫ + ⟪u.2, w.2⟫.