Rough differential forms #
A rough bundle-valued differential form assigns a continuous alternating map to each
tangent fiber, with values in an arbitrary family of real modules equipped with arbitrary
topologies. No regularity in the base point, global trivialization, connection, or fiber norm
is required.
Fixed-coefficient forms are the specialization to the trivial value bundle, and a function
f : M → F is the fixed-coefficient 0-form RoughForm.ofFunction I f, and a real one-form α
has the kernel distribution RoughForm.ker α, x ↦ ker α_x.
This is the unbundled section description of differential forms from Lee,
Introduction to Smooth Manifolds, second edition, Chapter 14, using Mathlib's
ContinuousAlternatingMap carrier.
A rough degree-k form with values in the family V of real modules equipped with arbitrary
topologies.
Instances For
A rough form with fixed coefficients, the trivial-value-bundle specialization.
Instances For
The 0-form of a function: at each point, the alternating map of degree zero with value
f x.
Instances For
Evaluation of the 0-form of a function on the empty tuple of tangent vectors.
The 0-form of a function at a point is the constant alternating map of degree zero with
value f x.
The 0-form of a scalar multiple of a function is the scalar multiple of its 0-form.
Every 0-form is the 0-form of its values on the empty tuple of tangent vectors.
The linear functional v ↦ α_x (v) of a one-form α at a point x.
Instances For
The kernel distribution of a one-form α: at each point x, the subspace of tangent vectors
v with α_x (v) = 0.
Instances For
The kernel of a one-form at x is the kernel of its linear functional at x.
The kernel of a one-form at x is the whole tangent space exactly when the form vanishes
at x.
A one-form which does not vanish at x takes a nonzero value on some tangent vector at x.
Rescaling a one-form by a function that does not vanish at x does not change its kernel
at x.