theorem pullback_neg {Ω₁ : ℕ → Type u_1} {VF₁ : Type u_2} {Ω₂ : ℕ → Type u_3} {VF₂ : Type u_4} [inst₁ : DifferentialFormSpace Ω₁ VF₁] [inst₂ : DifferentialFormSpace Ω₂ VF₂] (φ : DFSMorphism Ω₁ VF₁ Ω₂ VF₂) {p : ℕ} (α : Ω₂ p) : φ.pullback (-α) = -φ.pullback α

Pullback commutes with negation: $\varphi^*(-\alpha) = -\varphi^*\alpha$.

theorem pullback_sub {Ω₁ : ℕ → Type u_1} {VF₁ : Type u_2} {Ω₂ : ℕ → Type u_3} {VF₂ : Type u_4} [inst₁ : DifferentialFormSpace Ω₁ VF₁] [inst₂ : DifferentialFormSpace Ω₂ VF₂] (φ : DFSMorphism Ω₁ VF₁ Ω₂ VF₂) {p : ℕ} (α β : Ω₂ p) : φ.pullback (α - β) = φ.pullback α - φ.pullback β

Pullback is additive on differences: $\varphi^*(\alpha - \beta) = \varphi^*\alpha - \varphi^*\beta$.

structure SymplecticManifold (Ω : ℕ → Type u_1) (VF : Type u_2) [inst : DifferentialFormSpace Ω VF] : Type u_1

A symplectic manifold (Definition 7): a $2$-form $\omega \in \Omega^2(M)$ that is closed ($d\omega = 0$) and non-degenerate (the contraction map $X \mapsto \iota_X \omega$ is injective).

• ω : Ω 2
• closed : DifferentialFormSpace.d VF self.ω = 0
• nondegenerate : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X self.ω

class SymplecticManifoldDim (Ω : ℕ → Type u_1) (VF : Type u_2) [DifferentialFormSpace Ω VF] : Type

Records that a differential form space carries a positive half-dimension $n > 0$, so the ambient symplectic manifold has total dimension $2n$.

• n : ℕ
• n_pos : 0 < n Ω VF

class IsCompactSymplectic (Ω : ℕ → Type u_1) (VF : Type u_2) [inst : DifferentialFormSpace Ω VF] extends SymplecticManifoldDim Ω VF : Type u_1

Marks a $2n$-dimensional symplectic differential form space as compact symplectic: the symplectic form $\omega$ is not exact and there is a top-degree volume form $\omega^n$ which is also not exact. This abstracts the cohomological obstructions that hold on compact symplectic manifolds.

• n : ℕ
• n_pos : 0 < n Ω VF
• symplectic_not_exact (S : SymplecticManifold Ω VF) : ¬DifferentialFormSpace.IsExact' VF S.ω
• vol (S : SymplecticManifold Ω VF) : Ω (2 * SymplecticManifoldDim.n Ω VF - 1 + 1)
• volume_not_exact (S : SymplecticManifold Ω VF) : ¬∃ (β : Ω (2 * SymplecticManifoldDim.n Ω VF - 1)), DifferentialFormSpace.d VF β = vol S

structure Symplectomorphism {Ω₁ : ℕ → Type u_1} {VF₁ : Type u_2} {Ω₂ : ℕ → Type u_3} {VF₂ : Type u_4} [inst₁ : DifferentialFormSpace Ω₁ VF₁] [inst₂ : DifferentialFormSpace Ω₂ VF₂] (S₁ : SymplecticManifold Ω₁ VF₁) (S₂ : SymplecticManifold Ω₂ VF₂) : Type (max u_1 u_3)

A symplectomorphism (Definition 8): an invertible morphism of differential form spaces $\varphi : (M_1, \omega_1) \to (M_2, \omega_2)$ satisfying $\varphi^* \omega_2 = \omega_1$. Encoded with explicit two-sided inverse data at the level of pullbacks.

• toMorphism : DFSMorphism Ω₁ VF₁ Ω₂ VF₂
• invMorphism : DFSMorphism Ω₂ VF₂ Ω₁ VF₁
• left_inv {p : ℕ} (β : Ω₂ p) : self.invMorphism.pullback (self.toMorphism.pullback β) = β
• right_inv {p : ℕ} (α : Ω₁ p) : self.toMorphism.pullback (self.invMorphism.pullback α) = α
• pullback_symplectic : self.toMorphism.pullback S₂.ω = S₁.ω

structure IsSymplecticSubmanifold {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} {Ω_W : ℕ → Type u_3} {VF_W : Type u_4} [inst_M : DifferentialFormSpace Ω_M VF_M] [inst_W : DifferentialFormSpace Ω_W VF_W] (S : SymplecticManifold Ω_M VF_M) (i : DFSMorphism Ω_W VF_W Ω_M VF_M) : Prop

A submanifold $W \hookrightarrow M$ is symplectic when the pullback $i^*\omega$ remains non-degenerate on $W$, i.e. $X \mapsto \iota_X (i^*\omega)$ is injective on $\mathfrak{X}(W)$.

• restriction_nondegenerate : Function.Injective fun (X : VF_W) => DifferentialFormSpace.ι X (i.pullback S.ω)

structure IsLagrangianSubmanifold {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} {Ω_L : ℕ → Type u_3} {VF_L : Type u_4} [inst_M : DifferentialFormSpace Ω_M VF_M] [inst_L : DifferentialFormSpace Ω_L VF_L] (S : SymplecticManifold Ω_M VF_M) (i : DFSMorphism Ω_L VF_L Ω_M VF_M) (dimM dimL : ℕ) : Prop

A submanifold $L \hookrightarrow M$ is Lagrangian when $i^*\omega = 0$ and $\dim L = \tfrac{1}{2}\dim M$, i.e. $L$ is isotropic of maximal dimension.

• restriction_zero : i.pullback S.ω = 0
• half_dim : 2 * dimL = dimM

class CotangentBundleDFS (Ω_X : ℕ → Type u_1) (VF_X : Type u_2) (Ω_TX : ℕ → Type u_3) (VF_TX : Type u_4) [inst_X : DifferentialFormSpace Ω_X VF_X] [inst_TX : DifferentialFormSpace Ω_TX VF_TX] : Type (max u_1 u_3)

Axiomatic interface for the cotangent bundle $T^*X$ of a manifold $X$: equips $T^*X$ with the tautological Liouville 1-form $\theta$, the canonical symplectic form $\omega = d\theta$, and a zero section $X \hookrightarrow T^*X$ along which $\theta$ pulls back to $0$.

• dimX : ℕ
• dimX_pos : 0 < dimX Ω_X VF_X Ω_TX VF_TX
• liouville : Ω_TX 1
• canonical_symplectic : SymplecticManifold Ω_TX VF_TX
• symplectic_eq_d_liouville : (canonical_symplectic Ω_X VF_X).ω = DifferentialFormSpace.d VF_TX (liouville Ω_X VF_X VF_TX)
• zeroSection : DFSMorphism Ω_X VF_X Ω_TX VF_TX
• liouville_zero_section : zeroSection.pullback (liouville Ω_X VF_X VF_TX) = 0

structure GraphSetup (Ω₁ : ℕ → Type u_1) (VF₁ : Type u_2) (Ω₂ : ℕ → Type u_3) (VF₂ : Type u_4) (Ω_P : ℕ → Type u_5) (VF_P : Type u_6) [inst₁ : DifferentialFormSpace Ω₁ VF₁] [inst₂ : DifferentialFormSpace Ω₂ VF₂] [inst_P : DifferentialFormSpace Ω_P VF_P] (S₁ : SymplecticManifold Ω₁ VF₁) (S₂ : SymplecticManifold Ω₂ VF₂) : Type (max (max u_1 u_3) u_5)

Auxiliary setup for the graph $\Gamma_\varphi \subset M_1 \times M_2$ of a map $\varphi : M_1 \to M_2$ between symplectic manifolds: projections $\pi_1, \pi_2$, an embedding $\gamma : M_1 \to \Gamma_\varphi$, and the compatibility $\gamma^*\pi_1^* = \mathrm{id}$, $\gamma^*\pi_2^* = \varphi^*$.

• π₁ : DFSMorphism Ω_P VF_P Ω₁ VF₁
• π₂ : DFSMorphism Ω_P VF_P Ω₂ VF₂
• φ : DFSMorphism Ω₁ VF₁ Ω₂ VF₂
• γ : DFSMorphism Ω₁ VF₁ Ω_P VF_P
• dimM₁ : ℕ
• dimM₂ : ℕ
• dim_eq : self.dimM₁ = self.dimM₂
• γ_π₁ {p : ℕ} (α : Ω₁ p) : self.γ.pullback (self.π₁.pullback α) = α
• γ_π₂ {p : ℕ} (β : Ω₂ p) : self.γ.pullback (self.π₂.pullback β) = self.φ.pullback β

theorem graph_lagrangian_of_symplectomorphism {Ω₁ : ℕ → Type u_1} {VF₁ : Type u_2} {Ω₂ : ℕ → Type u_3} {VF₂ : Type u_4} {Ω_P : ℕ → Type u_5} {VF_P : Type u_6} [inst₁ : DifferentialFormSpace Ω₁ VF₁] [inst₂ : DifferentialFormSpace Ω₂ VF₂] [inst_P : DifferentialFormSpace Ω_P VF_P] {S₁ : SymplecticManifold Ω₁ VF₁} {S₂ : SymplecticManifold Ω₂ VF₂} (G : GraphSetup Ω₁ VF₁ Ω₂ VF₂ Ω_P VF_P S₁ S₂) (hφ : G.φ.pullback S₂.ω = S₁.ω) : G.γ.pullback (G.π₁.pullback S₁.ω - G.π₂.pullback S₂.ω) = 0

If $\varphi^* \omega_2 = \omega_1$ (i.e. $\varphi$ is a symplectomorphism), then the graph $\Gamma_\varphi$ is isotropic for $\pi_1^*\omega_1 - \pi_2^*\omega_2$: the pullback of this difference along $\gamma$ vanishes.

theorem symplectomorphism_of_graph_lagrangian {Ω₁ : ℕ → Type u_1} {VF₁ : Type u_2} {Ω₂ : ℕ → Type u_3} {VF₂ : Type u_4} {Ω_P : ℕ → Type u_5} {VF_P : Type u_6} [inst₁ : DifferentialFormSpace Ω₁ VF₁] [inst₂ : DifferentialFormSpace Ω₂ VF₂] [inst_P : DifferentialFormSpace Ω_P VF_P] {S₁ : SymplecticManifold Ω₁ VF₁} {S₂ : SymplecticManifold Ω₂ VF₂} (G : GraphSetup Ω₁ VF₁ Ω₂ VF₂ Ω_P VF_P S₁ S₂) (hLag : G.γ.pullback (G.π₁.pullback S₁.ω - G.π₂.pullback S₂.ω) = 0) : G.φ.pullback S₂.ω = S₁.ω

Converse: if $\gamma^*(\pi_1^*\omega_1 - \pi_2^*\omega_2) = 0$ on the graph, then $\varphi^*\omega_2 = \omega_1$, so $\varphi$ is a symplectomorphism.