@[reducible, inline]

abbrev Poly2 : Type

Real polynomials in two variables $\mathbb{R}[x_0, x_1]$, used as the function ring underlying the polynomial DFS on $\mathbb{R}^2$.

@[reducible]

def Symp2Ω : ℕ → Type

Polynomial $p$-forms on $\mathbb{R}^2$: scalars for $p = 0, 2$, pairs of polynomials for $p = 1$ (the components of $f\, dx + g\, dy$), and trivial in degrees $\ge 3$.

@[reducible]

def Symp2VF : Type

Polynomial vector fields on $\mathbb{R}^2$: pairs $(a, b)$ representing $a\, \partial_x + b\, \partial_y$.

@[implicit_reducible]

noncomputable instance symp2AddCommGroup (p : ℕ) : AddCommGroup (Symp2Ω p)

Each degree of polynomial forms on $\mathbb{R}^2$ inherits an additive commutative group.

@[implicit_reducible]

noncomputable instance symp2Module (p : ℕ) : Module ℝ (Symp2Ω p)

Each degree of polynomial forms on $\mathbb{R}^2$ inherits an $\mathbb{R}$-module structure.

noncomputable def symp2d {p : ℕ} : Symp2Ω p → Symp2Ω (p + 1)

Exterior derivative on polynomial forms on $\mathbb{R}^2$: $df = (\partial_x f, \partial_y f)$ on $0$-forms, $d(f\,dx + g\,dy) = \partial_x g - \partial_y f$ on $1$-forms, and $0$ in higher degree.

noncomputable def symp2Iota : Symp2VF → {p : ℕ} → Symp2Ω (p + 1) → Symp2Ω p

Interior product $\iota_X$ on polynomial forms on $\mathbb{R}^2$ with $X = (a, b)$: on $1$-forms $\iota_X(f, g) = af + bg$, on $2$-forms $\iota_X h = (-hb, ha)$, and $0$ in higher degree.

noncomputable def symp2fMul {p : ℕ} : Symp2Ω 0 → Symp2Ω p → Symp2Ω p

Scaling a polynomial $p$-form on $\mathbb{R}^2$ by a polynomial $0$-form, defined componentwise.

noncomputable def symp2wedge1 {p : ℕ} : Symp2Ω 1 → Symp2Ω p → Symp2Ω (p + 1)

Wedge product of a polynomial $1$-form with a polynomial $p$-form on $\mathbb{R}^2$, yielding a $(p+1)$-form; nontrivial only for $p = 0$ and $p = 1$.

noncomputable def symp2L : Symp2VF → {p : ℕ} → Symp2Ω p → Symp2Ω p

Lie derivative $\mathcal{L}_X$ on polynomial forms on $\mathbb{R}^2$, defined via Cartan's magic formula $\mathcal{L}_X = d \circ \iota_X + \iota_X \circ d$.

theorem pderiv_comm_poly (i j : Fin 2) (f : Poly2) : (MvPolynomial.pderiv i) ((MvPolynomial.pderiv j) f) = (MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) f)

Commutativity of partial derivatives on $\mathbb{R}[x_0, x_1]$: $\partial_i \partial_j f = \partial_j \partial_i f$.

@[implicit_reducible]

noncomputable instance symp2DFS : DifferentialFormSpace Symp2Ω Symp2VF

Polynomial forms on $\mathbb{R}^2$ assemble into a DifferentialFormSpace, giving a two-dimensional scaffolding (DFS) for the local model of a symplectic surface.

noncomputable def symp2Manifold : SymplecticManifold Symp2Ω Symp2VF

The standard symplectic structure on $\mathbb{R}^2$: the constant area form $\omega = 1 \in \Omega^2$, which is closed and nondegenerate.

noncomputable def symp2HodgeStar {p : ℕ} : Symp2Ω p → Symp2Ω p

Hodge star operator on polynomial forms on $\mathbb{R}^2$: $\star f = f$ on $0$- and $2$-forms, and $\star(f\, dx + g\, dy) = -g\, dx + f\, dy$ on $1$-forms.