The type of smooth k-forms on a manifold M: pointwise alternating multilinear maps
(T_xM)^k → ℝ indexed by x : M.
Instances For
Pointwise addition makes MfdDiffForm k I M into an additive commutative group.
Pointwise scalar multiplication makes MfdDiffForm k I M into a real vector space.
Evaluation of a k-form ω at a point x : M, yielding the alternating map ω_x on T_xM.
Instances For
Pointwise extensionality: two k-forms are equal if they agree at every point.
Exterior derivative d : Ω^k(M) → Ω^{k+1}(M) of a manifold differential form.
Instances For
The exterior derivative is additive: $d(\omega + \eta) = d\omega + d\eta$.
The fundamental identity $d \circ d = 0$ for the exterior derivative on a manifold.
Pullback of a differential form along a map f : M → N: $(f^*\omega)_x = \omega_{f(x)} \circ df_x$.
Instances For
Pullback by the identity map is the identity: $\mathrm{id}^* \omega = \omega$.
Naturality of the exterior derivative: $f^*(d\omega) = d(f^*\omega)$ for smooth f.
A form ω is closed if $d\omega = 0$.
Instances For
A (k+1)-form ω is exact if $\omega = d\eta$ for some k-form η.
Instances For
Every exact form is closed: $\omega = d\eta$ implies $d\omega = d^2\eta = 0$.