Differential $p$-forms on a smooth manifold $M$ (modeled on $E$ via I), realized
concretely as functions $M \to \Lambda^p E^*$ from points of $M$ to alternating $p$-forms
on the model space $E$.
Instances For
Vector fields on $M$ (modeled on $E$), realized concretely as functions $M \to E$ assigning to each point an element of the model space.
Instances For
Pointwise addition gives the space of differential $p$-forms an abelian group structure.
Pointwise scalar multiplication gives differential $p$-forms an $\mathbb{R}$-module structure.
Convert a continuous alternating $1$-form $w \in \Lambda^1 E^*$ to a continuous linear functional $E \to \mathbb{R}$, using the canonical identification of singleton-indexed alternating maps with linear maps.
Instances For
Pointwise wedge product of a $1$-form $w$ with a $p$-form $a$, producing a $(p+1)$-form $w \wedge a$ via antisymmetrization of $(v_0, v_1, \dots, v_p) \mapsto w(v_0) \cdot a(v_1, \dots, v_p)$.
Instances For
Evaluating oneFormToCL w at a vector $v$ is the same as evaluating the original
$1$-form on the one-element tuple $[v]$.
Currying-on-the-left commutes with antisymmetrization in the following sense: $$\iota_v (L \wedge \beta) = (Lv) \cdot \beta - L \wedge (\iota_v \beta),$$ the basic Leibniz identity for $\iota_v$ acting on a wedge product $L \wedge \beta$.
Multiplication of a $p$-form $\alpha$ by a scalar function $f \in \Omega^0$: $(f \cdot \alpha)_x = f(x) \cdot \alpha_x$.
Instances For
Interior product $\iota_X \alpha$: contracts a vector field $X$ into the first slot of a $(p+1)$-form $\alpha$, producing a $p$-form.
Instances For
The exterior derivative $d : \Omega^p(M) \to \Omega^{p+1}(M)$. On a function $f$, $df$ is the differential. On a $(p+1)$-form $\alpha$, $d\alpha$ is given by the invariant formula involving $\sum_i (-1)^i \, \partial_{v_i}(\alpha(\hat v_i))$.
Instances For
Wedge product of a $1$-form $w$ with a $p$-form $\alpha$, producing a $(p+1)$-form $w \wedge \alpha$ defined pointwise.
Instances For
The Lie derivative $\mathcal{L}_X \alpha$ along a vector field $X$, defined via Cartan's magic formula $\mathcal{L}_X = \iota_X \circ d + d \circ \iota_X$ (with the $p = 0$ case reducing to $\mathcal{L}_X f = \iota_X df$).
Instances For
The exterior derivative is additive: $d(\alpha + \beta) = d\alpha + d\beta$.
The exterior derivative is $\mathbb{R}$-linear: $d(r \cdot \alpha) = r \cdot d\alpha$.
$d^2 = 0$: the exterior derivative squares to zero, $d \circ d = 0$.
Interior product against the zero form vanishes: $\iota_X 0 = 0$.
The interior product is additive in the form argument: $\iota_X(\alpha + \beta) = \iota_X \alpha + \iota_X \beta$.
The interior product is $\mathbb{R}$-linear: $\iota_X(r \cdot \alpha) = r \cdot \iota_X \alpha$.
Leibniz rule for $d$ multiplied by a function: $d(f \cdot \alpha) = df \wedge \alpha + f \cdot d\alpha$.
$\iota_X$ commutes with multiplication by a scalar function: $\iota_X(f \cdot \alpha) = f \cdot \iota_X \alpha$.
Graded Leibniz rule for $\iota_X$ on a wedge $w \wedge \alpha$ with $w$ a $1$-form: $$\iota_X(w \wedge \alpha) = (\iota_X w) \cdot \alpha - w \wedge \iota_X \alpha.$$
Degenerate case of $\iota_X$ on $w \wedge g$ when $g \in \Omega^0$: the second correction term vanishes, yielding $\iota_X(w \wedge g) = (\iota_X w) \cdot g$.
Multiplication by a function distributes over form addition: $f \cdot (\alpha + \beta) = f \cdot \alpha + f \cdot \beta$.
The Lie derivative is additive in the form: $\mathcal{L}_X(\alpha + \beta) = \mathcal{L}_X \alpha + \mathcal{L}_X \beta$.
The Lie derivative is $\mathbb{R}$-linear in the form: $\mathcal{L}_X(r \cdot \alpha) = r \cdot \mathcal{L}_X \alpha$.
The Lie derivative commutes with the exterior derivative: $\mathcal{L}_X \, d\alpha = d \, \mathcal{L}_X \alpha$, a consequence of Cartan's formula and $d^2 = 0$.
Leibniz rule for the Lie derivative: $\mathcal{L}_X(f \cdot \alpha) = (\mathcal{L}_X f) \cdot \alpha + f \cdot \mathcal{L}_X \alpha$.
Rearranged Leibniz rule: $f \cdot d\alpha = d(f \cdot \alpha) - df \wedge \alpha$.
Auxiliary scalar function: fix the slot $i$ and the remaining vectors Fin.removeNth i vs,
viewing $\alpha$ as a function of the base point $y$ that evaluates to a real number. Useful
for differentiating $\alpha$ in the base variable.
Instances For
The differential-form-space (DFS) structure on a smooth manifold $M$. This bundles the exterior derivative $d$, the interior product $\iota_X$, multiplication by functions, wedge with $1$-forms, and the Lie derivative $\mathcal{L}_X$, together with all their algebraic identities ($d^2 = 0$, Leibniz, Cartan, nondegeneracy of $\iota$).
Instances For
Typeclass version of manifoldDFS: every smooth manifold $M$ automatically carries the
differential-form-space structure on $\Omega^\bullet(M)$ and vector fields.
The Lie bracket of two constant vector fields is zero: $[V, W] = 0$ when $V, W$ are constant functions on $E$, since their derivatives vanish.
The "Lie-bracket term" appearing in the invariant Cartan formula for $d\alpha$:
$$\sum_{i < j} (-1)^{i+j} \, \alpha([V_i, V_j], V_0, \dots, \hat V_i, \dots, \hat V_j, \dots).$$
For constant vector fields this term vanishes by lieBracket_constVF.