noncomputable def symp2StdJ : Symp2VF → Symp2VF

The standard almost-complex structure $J$ on the $2$-dimensional symplectic model: $J(a, b) = (-b, a)$, modeling multiplication by $i$.

theorem symp2StdJ_sq (X : Symp2VF) : symp2StdJ (symp2StdJ X) = (-X.1, -X.2)

$J^2 = -\mathrm{Id}$: applying the standard $J$ twice negates both components.

theorem symp2_iota_neg_components (a b : Poly2) (α : Symp2Ω 1) : symp2Iota (-a, -b) α = -symp2Iota (a, b) α

The interior product $\iota$ on the $2$D symplectic model is linear under negation of its vector-field components: $\iota_{(-a, -b)} \alpha = -\iota_{(a, b)} \alpha$.

theorem symp2_lift_sq_neg (X : Symp2VF) (α : Symp2Ω 1) : DifferentialFormSpace.ι (symp2StdJ (symp2StdJ X)) α = -DifferentialFormSpace.ι X α

The lifted $J$ on the differential-form-space level satisfies $\iota_{J^2 X} = -\iota_X$, i.e. the action of $J^2$ on $1$-forms is multiplication by $-1$.

theorem symp2_lift_preserves (u v : Symp2VF) (ω : Symp2Ω 2) : DifferentialFormSpace.ι (symp2StdJ u) (DifferentialFormSpace.ι (symp2StdJ v) ω) = DifferentialFormSpace.ι u (DifferentialFormSpace.ι v ω)

$J$ preserves the symplectic form: $\omega(JX, JY) = \omega(X, Y)$ in the $2$-dimensional model, expressed via the lifted interior product.

theorem symp2_lift_taming (S : SymplecticManifold Symp2Ω Symp2VF) : Function.Injective fun (v : Symp2VF) => DifferentialFormSpace.ι (symp2StdJ v) S.ω

Taming: the map $v \mapsto \iota_{Jv} \omega$ is injective, equivalently the bilinear form $g(X, Y) = \omega(X, JY)$ is nondegenerate. This is the analytic content of $J$ taming the symplectic form.

@[implicit_reducible]

noncomputable instance symp2HasTangentSpaces : HasTangentSpaces Symp2Ω Symp2VF

The $2$-dimensional symplectic model carries a HasTangentSpaces instance: the model manifold is taken to be Empty (it serves only as a tangent-space scaffolding), while the linear-algebra data (standard $J$, $J^2 = -1$, $J$ preserving $\omega$, taming) is provided by the lemmas above.