@[reducible]

def PolyΩ : ℕ → Type

Polynomial $p$-forms on $\mathbb{R}$: real polynomials in degrees $0$ and $1$, trivial otherwise.

@[reducible]

def PolyVF : Type

Polynomial vector fields on $\mathbb{R}$: a single polynomial coefficient $X(t) \partial_t$.

@[implicit_reducible]

noncomputable instance polyΩ_acg (p : ℕ) : AddCommGroup (PolyΩ p)

Each degree of polynomial forms inherits an additive commutative group structure.

@[implicit_reducible]

noncomputable instance polyΩ_mod (p : ℕ) : Module ℝ (PolyΩ p)

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

noncomputable def polyFMul {p : ℕ} : PolyΩ 0 → PolyΩ p → PolyΩ p

Multiplication of a polynomial $0$-form (function) by a $p$-form: pointwise polynomial product.

noncomputable def polyWedge1 {p : ℕ} : PolyΩ 1 → PolyΩ p → PolyΩ (p + 1)

Wedge of a $1$-form with a $p$-form on $\mathbb{R}$: nontrivial only when $p = 0$.

noncomputable def polyD {p : ℕ} : PolyΩ p → PolyΩ (p + 1)

Exterior derivative on polynomial forms: $d f = f'\, dt$ for a $0$-form, zero in higher degree.

noncomputable def polyIota (X : PolyVF) {p : ℕ} : PolyΩ (p + 1) → PolyΩ p

Interior product (contraction) $\iota_X$ of a vector field $X$ with a polynomial form.

noncomputable def polyLie (X : PolyVF) {p : ℕ} : PolyΩ p → PolyΩ p

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

noncomputable def polyAntideriv (g : Polynomial ℝ) : Polynomial ℝ

Formal antiderivative of a real polynomial: $\int (\sum a_n t^n)\, dt = \sum \tfrac{a_n}{n+1} t^{n+1}$.

theorem derivative_antideriv (g : Polynomial ℝ) : Polynomial.derivative (polyAntideriv g) = g

Fundamental theorem of calculus for polynomials: $\frac{d}{dt} \int g(t)\, dt = g(t)$.

@[implicit_reducible]

noncomputable instance polyDFS : DifferentialFormSpace PolyΩ PolyVF

Polynomial forms on $\mathbb{R}$ assemble into a DifferentialFormSpace, providing a testbed scaffolding for de Rham cohomology in dimension $1$.

theorem polyOmega_zero_nontrivial : 0 ≠ 1

The space of polynomial $0$-forms is nontrivial: $0 \ne 1$.

theorem polyOmega_one_nontrivial : 0 ≠ 1

The space of polynomial $1$-forms is nontrivial: $0 \ne 1$.

instance instNontrivialPolyΩOfNatNat : Nontrivial (PolyΩ 0)

Nontriviality instance for polynomial $0$-forms.

instance instNontrivialPolyΩOfNatNat_1 : Nontrivial (PolyΩ 1)

Nontriviality instance for polynomial $1$-forms.