Smooth bundle-valued differential forms

This file packages smooth sections of the bundle of alternating maps on tangent fibres. The underlying rough form remains an unbundled dependent function, while IsSmoothBundleForm records that its graph is a smooth section of the alternating bundle. The corresponding Submodule provides the bundled carrier SmoothBundleForm; fixed coefficients are the SmoothForm specialization. These carriers are the input for smooth wedge products and pullbacks.

The degree-two evaluation API below evaluates forms on ordered pairs and exposes real-valued fibres as alternating bilinear forms.

In the trivialization at any point, the fiber coordinate of a form at y is the form pulled back along the inverse tangent trivialization at y (FiberBundle.trivializationAt_continuousAlternatingMap_apply_snd), with no chart-domain hypothesis. Hence a form is C^n exactly when its values on the frames of these trivializations are (TauCeti.isSmoothForm_iff_forall_contMDiffAt_trivializationAt_apply).

Smoothness is expressed through the total-space charts of the topological alternating bundle. The module operations use Mathlib's smooth-section API, so this carrier does not require a chosen trivialization or a global smooth alternating-bundle instance.

The fixed-coefficient section and degree-two evaluation adapters generalize the corresponding declarations in TauCeti.Geometry.Manifold.TwoForm.Basic.

For degree two, use the ordered-pair evaluation to obtain the value in the fibre over a point. The accompanying API provides alternation, extensionality, and C^n smoothness after applying the form to C^n tangent fields; the fixed-coefficient section exposes the same operations in a trivial bundle. On a Hausdorff manifold, two smooth forms agreeing on a dense set are equal (TauCeti.SmoothBundleForm.eq_of_forall_mem_dense).

def TauCeti.IsSmoothBundleForm {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} (I : ModelWithCorners ℝ E H) (F : Type u_6) [NormedAddCommGroup F] [NormedSpace ℝ F] (V : M → Type u_7) [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [IsManifold I 1 M] (n : WithTop ℕ∞) (φ : RoughBundleForm I M V k) : Prop

A rough bundle-valued form has C^n regularity when its graph is a C^n section of the alternating bundle with fibres TangentSpace I x [⋀^Fin k]→L[ℝ] V x; n = ∞ gives smoothness.

theorem TauCeti.isSmoothBundleForm_def {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} [IsManifold I 1 M] (n : WithTop ℕ∞) (φ : RoughBundleForm I M V k) : IsSmoothBundleForm I F V n φ ↔ ContMDiff I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F))) n fun (x : M) => ⟨x, φ x⟩

The defining characterization of IsSmoothBundleForm.

def TauCeti.smoothBundleForms {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) [IsManifold I 1 M] (F : Type u_6) [NormedAddCommGroup F] [NormedSpace ℝ F] (V : M → Type u_7) [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] (k : ℕ) : Submodule ℝ (RoughBundleForm I M V k)

The submodule of smooth V-valued rough k-forms.

@[simp]

theorem TauCeti.mem_smoothBundleForms {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} [IsManifold I 1 M] {φ : RoughBundleForm I M V k} : φ ∈ smoothBundleForms I F V k ↔ IsSmoothBundleForm I F V (↑⊤) φ

Membership in smoothBundleForms is exactly smoothness of the corresponding section.

@[reducible, inline]

abbrev TauCeti.SmoothBundleForm {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) (F : Type u_6) [NormedAddCommGroup F] [NormedSpace ℝ F] (V : M → Type u_7) [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [IsManifold I 1 M] (k : ℕ) : Type (max (max u_1 u_3) u_7)

A smooth bundle-valued differential k-form.

theorem TauCeti.SmoothBundleForm.ext {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {φ ψ : SmoothBundleForm I F V k} (h : ∀ (x : M) (v : Fin k → TangentSpace I x), (↑φ x) v = (↑ψ x) v) : φ = ψ

Two smooth bundle-valued forms are equal when they agree on every tangent tuple.

theorem TauCeti.SmoothBundleForm.ext_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {φ ψ : SmoothBundleForm I F V k} : φ = ψ ↔ ∀ (x : M) (v : Fin k → TangentSpace I x), (↑φ x) v = (↑ψ x) v

theorem TauCeti.SmoothBundleForm.eq_of_forall_mem_dense {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] [T2Space M] {s : Set M} (hs : Dense s) {φ ψ : SmoothBundleForm I F V k} (h : ∀ x ∈ s, ↑φ x = ↑ψ x) : φ = ψ

Two smooth bundle-valued forms on a Hausdorff manifold that agree on a dense set are equal: their sections are continuous maps into the total space of the alternating bundle, which is Hausdorff.

def TauCeti.SmoothBundleForm.toContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothBundleForm I F V k) : ContMDiffSection I (E [⋀^Fin k]→L[ℝ] F) ↑⊤ fun (x : M) => TangentSpace I x [⋀^Fin k]→L[ℝ] V x

The smooth section underlying a smooth bundle-valued differential form.

def TauCeti.SmoothBundleForm.ofContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (s : ContMDiffSection I (E [⋀^Fin k]→L[ℝ] F) ↑⊤ fun (x : M) => TangentSpace I x [⋀^Fin k]→L[ℝ] V x) : SmoothBundleForm I F V k

Reconstruct a smooth bundle-valued form from its smooth section.

@[simp]

theorem TauCeti.SmoothBundleForm.toContMDiffSection_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothBundleForm I F V k) (x : M) : φ.toContMDiffSection x = ↑φ x

@[simp]

theorem TauCeti.SmoothBundleForm.ofContMDiffSection_toContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothBundleForm I F V k) : ofContMDiffSection φ.toContMDiffSection = φ

The section view and reconstruction are mutual inverses on forms.

@[simp]

theorem TauCeti.SmoothBundleForm.toContMDiffSection_ofContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (s : ContMDiffSection I (E [⋀^Fin k]→L[ℝ] F) ↑⊤ fun (x : M) => TangentSpace I x [⋀^Fin k]→L[ℝ] V x) : (ofContMDiffSection s).toContMDiffSection = s

The section view and reconstruction are mutual inverses on sections.

theorem TauCeti.SmoothBundleForm.toContMDiffSection_injective {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] : Function.Injective toContMDiffSection

The section view determines a smooth bundle-valued form uniquely.

@[simp]

theorem TauCeti.SmoothBundleForm.zero_toContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] : toContMDiffSection 0 = 0

@[simp]

theorem TauCeti.SmoothBundleForm.add_toContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ ψ : SmoothBundleForm I F V k) : (φ + ψ).toContMDiffSection = φ.toContMDiffSection + ψ.toContMDiffSection

@[simp]

theorem TauCeti.SmoothBundleForm.smul_toContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (c : ℝ) (φ : SmoothBundleForm I F V k) : (c • φ).toContMDiffSection = c • φ.toContMDiffSection

@[simp]

theorem TauCeti.SmoothBundleForm.neg_toContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothBundleForm I F V k) : (-φ).toContMDiffSection = -φ.toContMDiffSection

@[simp]

theorem TauCeti.SmoothBundleForm.sub_toContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ ψ : SmoothBundleForm I F V k) : (φ - ψ).toContMDiffSection = φ.toContMDiffSection - ψ.toContMDiffSection

def TauCeti.SmoothBundleForm.eval₂ {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothBundleForm I F V 2) (x : M) (v w : TangentSpace I x) : V x

Evaluation of a smooth bundle-valued two-form on an ordered pair of tangent vectors returns the value in the fibre over the base point.

@[simp]

theorem TauCeti.SmoothBundleForm.eval₂_self {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothBundleForm I F V 2) (x : M) (v : TangentSpace I x) : φ.eval₂ x v v = 0

Evaluation on two equal tangent vectors vanishes by alternation.

theorem TauCeti.SmoothBundleForm.eval₂_swap {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothBundleForm I F V 2) (x : M) (v w : TangentSpace I x) : φ.eval₂ x v w = -φ.eval₂ x w v

Swapping the inputs of a bundle-valued two-form negates its value.

@[simp]

theorem TauCeti.SmoothBundleForm.eval₂_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothBundleForm I F V 2) (x : M) (v w : TangentSpace I x) : φ.eval₂ x v w = (↑φ x) ![v, w]

theorem TauCeti.SmoothBundleForm.eval₂_add {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ ψ : SmoothBundleForm I F V 2) (x : M) (v w : TangentSpace I x) : (φ + ψ).eval₂ x v w = φ.eval₂ x v w + ψ.eval₂ x v w

Evaluation of a sum of degree-two forms is the sum of the evaluations.

theorem TauCeti.SmoothBundleForm.eval₂_neg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothBundleForm I F V 2) (x : M) (v w : TangentSpace I x) : (-φ).eval₂ x v w = -φ.eval₂ x v w

Evaluation of the negative of a degree-two form is the negative of the evaluation.

theorem TauCeti.SmoothBundleForm.eval₂_add_left {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothBundleForm I F V 2) (x : M) (v v' w : TangentSpace I x) : φ.eval₂ x (v + v') w = φ.eval₂ x v w + φ.eval₂ x v' w

Ordered-pair evaluation is additive in its first tangent argument.

theorem TauCeti.SmoothBundleForm.eval₂_add_right {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothBundleForm I F V 2) (x : M) (v w w' : TangentSpace I x) : φ.eval₂ x v (w + w') = φ.eval₂ x v w + φ.eval₂ x v w'

Ordered-pair evaluation is additive in its second tangent argument.

theorem TauCeti.SmoothBundleForm.eval₂_smul_left {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothBundleForm I F V 2) (x : M) (c : ℝ) (v w : TangentSpace I x) : φ.eval₂ x (c • v) w = c • φ.eval₂ x v w

Real scalar multiplication in the first tangent argument scales the fibre value.

theorem TauCeti.SmoothBundleForm.eval₂_smul_right {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothBundleForm I F V 2) (x : M) (c : ℝ) (v w : TangentSpace I x) : φ.eval₂ x v (c • w) = c • φ.eval₂ x v w

Real scalar multiplication in the second tangent argument scales the fibre value.

theorem TauCeti.SmoothBundleForm.eval₂_neg_left {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothBundleForm I F V 2) (x : M) (v w : TangentSpace I x) : φ.eval₂ x (-v) w = -φ.eval₂ x v w

Negating the first tangent vector negates the evaluation of a degree-two form.

theorem TauCeti.SmoothBundleForm.eval₂_neg_right {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothBundleForm I F V 2) (x : M) (v w : TangentSpace I x) : φ.eval₂ x v (-w) = -φ.eval₂ x v w

Negating the second tangent vector negates the evaluation of a degree-two form.

theorem TauCeti.SmoothBundleForm.apply_eq_of_eval₂_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {φ ψ : SmoothBundleForm I F V 2} {x : M} (h : ∀ (v w : TangentSpace I x), φ.eval₂ x v w = ψ.eval₂ x v w) : ↑φ x = ↑ψ x

Two smooth bundle-valued two-forms have the same value at a point when their ordered-pair evaluations there agree.

theorem TauCeti.SmoothBundleForm.ext_eval₂ {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {φ ψ : SmoothBundleForm I F V 2} (h : ∀ (x : M) (v w : TangentSpace I x), φ.eval₂ x v w = ψ.eval₂ x v w) : φ = ψ

Two smooth bundle-valued two-forms are equal when their ordered-pair evaluations agree.

theorem TauCeti.SmoothBundleForm.ext_eval₂_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {φ ψ : SmoothBundleForm I F V 2} : φ = ψ ↔ ∀ (x : M) (v w : TangentSpace I x), φ.eval₂ x v w = ψ.eval₂ x v w

Two smooth bundle-valued two-forms are equal exactly when all ordered-pair evaluations agree.

theorem TauCeti.SmoothBundleForm.contMDiff_eval₂ {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {E' : Type u_6} {H' : Type u_7} {N : Type u_8} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} [ENat.LEInfty n] (φ : SmoothBundleForm I F V 2) {b : N → M} {U W : (y : N) → TangentSpace I (b y)} (hU : ContMDiff I' I.tangent n fun (y : N) => ⟨b y, U y⟩) (hW : ContMDiff I' I.tangent n fun (y : N) => ⟨b y, W y⟩) : ContMDiff I' (I.prod (modelWithCornersSelf ℝ F)) n fun (y : N) => ⟨b y, φ.eval₂ (b y) (U y) (W y)⟩

Evaluating a smooth bundle-valued two-form on two C^n tangent fields along a C^n map is C^n.

def TauCeti.IsSmoothForm {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} (I : ModelWithCorners ℝ E H) [IsManifold I 1 M] (n : WithTop ℕ∞) (φ : RoughForm I M F k) : Prop

A fixed-coefficient rough form is C^n when it is a C^n section of the existing alternating tangent bundle. Degree and coefficient space are inferred from the form.

theorem TauCeti.isSmoothForm_def {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] (n : WithTop ℕ∞) (φ : RoughForm I M F k) : IsSmoothForm I n φ ↔ ContMDiff I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F))) n fun (x : M) => ⟨x, φ x⟩

The fixed-coefficient regularity predicate is the existing section regularity predicate.

theorem TauCeti.IsSmoothForm.contMDiff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] {n : WithTop ℕ∞} {φ : RoughForm I M F k} (hφ : IsSmoothForm I n φ) : ContMDiff I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F))) n fun (x : M) => ⟨x, φ x⟩

A regular fixed-coefficient form is a regular section of the alternating bundle.

theorem TauCeti.IsSmoothForm.add {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] {n : WithTop ℕ∞} {φ ψ : RoughForm I M F k} (hφ : IsSmoothForm I n φ) (hψ : IsSmoothForm I n ψ) : IsSmoothForm I n (φ + ψ)

Addition preserves regularity of the actual fixed-coefficient bundle sections.

theorem TauCeti.IsSmoothForm.zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] (n : WithTop ℕ∞) : IsSmoothForm I n 0

The zero differential form has every section regularity.

theorem TauCeti.IsSmoothForm.sum {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] {n : WithTop ℕ∞} {ι : Type u_6} (φ : ι → RoughForm I M F k) (s : Finset ι) (hφ : ∀ i ∈ s, IsSmoothForm I n (φ i)) : IsSmoothForm I n (∑ i ∈ s, φ i)

Finite sums preserve section regularity of differential forms.

theorem TauCeti.IsSmoothForm.neg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] {n : WithTop ℕ∞} {φ : RoughForm I M F k} (hφ : IsSmoothForm I n φ) : IsSmoothForm I n (-φ)

Negation preserves regularity of the actual fixed-coefficient bundle section.

theorem TauCeti.IsSmoothForm.smul {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] {n : WithTop ℕ∞} {φ : RoughForm I M F k} (hφ : IsSmoothForm I n φ) (c : ℝ) : IsSmoothForm I n (c • φ)

Constant scalar multiplication preserves regularity of the actual bundle section.

theorem TauCeti.IsSmoothForm.fun_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] {n : WithTop ℕ∞} {φ : RoughForm I M F k} (hφ : IsSmoothForm I n φ) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f) : IsSmoothForm I n fun (x : M) => f x • φ x

Multiplication by a scalar C^n function preserves the regularity of a rough form.

theorem TauCeti.IsSmoothForm.of_le {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] {m n : WithTop ℕ∞} {φ : RoughForm I M F k} (hφ : IsSmoothForm I n φ) (hmn : m ≤ n) : IsSmoothForm I m φ

A C^n form is C^m for every m ≤ n.

theorem TauCeti.isSmoothForm_iff_forall_contMDiffAt_trivializationAt_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} {φ : RoughForm I M F k} : IsSmoothForm I n φ ↔ ∀ (x : M) (v : Fin k → E), ContMDiffAt I (modelWithCornersSelf ℝ F) n (fun (y : M) => (φ y) (⇑(Bundle.Trivialization.symmL ℝ (trivializationAt E (TangentSpace I) x) y) ∘ v)) x

Smoothness of a form read in tangent trivializations: for a finite-dimensional model space, a form is C^n exactly when, near each point x, its values on the frame e.symmL y ∘ v of the tangent trivialization e at x, for each fixed tuple v of model vectors, are C^n at x.

theorem TauCeti.IsSmoothForm.mem_smoothBundleForms {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] {φ : RoughForm I M F k} (hφ : IsSmoothForm I (↑⊤) φ) : φ ∈ smoothBundleForms I F (Bundle.Trivial M F) k

A smooth fixed-coefficient rough form lies in the smooth bundle-form submodule.

@[reducible, inline]

abbrev TauCeti.SmoothForm {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (F : Type u_7) [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) : Type (max (max u_7 u_6) u_1)

A smooth fixed-coefficient differential k-form.

theorem TauCeti.SmoothForm.isSmoothBundleForm {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothForm I M F k) : IsSmoothBundleForm I F (Bundle.Trivial M F) ↑⊤ ↑φ

The underlying rough form of a smooth form is a smooth bundle section.

theorem TauCeti.SmoothForm.contMDiff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothForm I M F k) : ContMDiff I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F))) ↑⊤ fun (x : M) => ⟨x, ↑φ x⟩

The section underlying a smooth form is smooth.

theorem TauCeti.SmoothForm.isSmoothForm {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothForm I M F k) : IsSmoothForm I ↑⊤ ↑φ

The underlying rough form of a smooth form is a smooth fixed-coefficient form.

theorem TauCeti.SmoothForm.cast_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] {n m : ℕ} (h : n = m) (α : SmoothForm I M F n) (x : M) (v : Fin m → TangentSpace I x) : (↑((LinearEquiv.cast h) α) x) v = (↑α x) (v ∘ Fin.cast h)

Evaluating a smooth form after transporting its degree across an equality.

theorem TauCeti.SmoothForm.coe_cast {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] {n m : ℕ} (h : n = m) (α : SmoothForm I M F n) (x : M) : ⇑(↑((LinearEquiv.cast h) α) x) = fun (v : Fin m → TangentSpace I x) => (↑α x) (v ∘ Fin.cast h)

Evaluating the underlying rough form of a degree transport evaluates transported vectors.

theorem TauCeti.SmoothForm.cast_cast {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] {n m o : ℕ} (h : n = m) (h' : m = o) (α : SmoothForm I M F n) : (LinearEquiv.cast h') ((LinearEquiv.cast h) α) = (LinearEquiv.cast ⋯) α

Successive degree transports collapse to the transport along their composite equality.

@[simp]

theorem TauCeti.SmoothForm.cast_symm {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] {n m : ℕ} (h : n = m) : (LinearEquiv.cast h).symm = LinearEquiv.cast ⋯

Inverting a degree transport gives the transport along the inverse equality.

theorem TauCeti.SmoothForm.mdifferentiable {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothForm I M F k) : MDiff fun (x : M) => ⟨x, ↑φ x⟩

The section underlying a smooth form is differentiable.

theorem TauCeti.SmoothForm.mdifferentiableAt {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothForm I M F k) (x : M) : (MDiffAt fun (x : M) => ⟨x, ↑φ x⟩) x

The section underlying a smooth form is differentiable at every point.

theorem TauCeti.SmoothForm.mdifferentiableAt_apply_vectorField {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothForm I M F k) {V : Fin k → (y : M) → TangentSpace I y} {x : M} (hV : ∀ (i : Fin k), (MDiffAt fun (y : M) => ⟨y, V i y⟩) x) : (MDiffAt fun (y : M) => (↑φ y) fun (x : Fin k) => V x y) x

Evaluating a smooth form on vector fields differentiable at a point gives a function differentiable at that point.

def TauCeti.SmoothForm.toContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (φ : SmoothForm I M F k) : ContMDiffSection I (E [⋀^Fin k]→L[ℝ] F) ↑⊤ fun (x : M) => TangentSpace I x [⋀^Fin k]→L[ℝ] F

The smooth section underlying a fixed-coefficient smooth form.

def TauCeti.SmoothForm.ofContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (s : ContMDiffSection I (E [⋀^Fin k]→L[ℝ] F) ↑⊤ fun (x : M) => TangentSpace I x [⋀^Fin k]→L[ℝ] F) : SmoothForm I M F k

Reconstruct a fixed-coefficient smooth form from its smooth section.

@[simp]

theorem TauCeti.SmoothForm.toContMDiffSection_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (φ : SmoothForm I M F k) (x : M) : φ.toContMDiffSection x = ↑φ x

@[simp]

theorem TauCeti.SmoothForm.ofContMDiffSection_toContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (φ : SmoothForm I M F k) : ofContMDiffSection φ.toContMDiffSection = φ

The section view and reconstruction are mutual inverses on forms.

@[simp]

theorem TauCeti.SmoothForm.toContMDiffSection_ofContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (s : ContMDiffSection I (E [⋀^Fin k]→L[ℝ] F) ↑⊤ fun (x : M) => TangentSpace I x [⋀^Fin k]→L[ℝ] F) : (ofContMDiffSection s).toContMDiffSection = s

The section view and reconstruction are mutual inverses on sections.

theorem TauCeti.SmoothForm.toContMDiffSection_injective {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} : Function.Injective toContMDiffSection

The section view determines a smooth fixed-coefficient form uniquely.

@[simp]

theorem TauCeti.SmoothForm.zero_toContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} : toContMDiffSection 0 = 0

@[simp]

theorem TauCeti.SmoothForm.add_toContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (φ ψ : SmoothForm I M F k) : (φ + ψ).toContMDiffSection = φ.toContMDiffSection + ψ.toContMDiffSection

@[simp]

theorem TauCeti.SmoothForm.smul_toContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (c : ℝ) (φ : SmoothForm I M F k) : (c • φ).toContMDiffSection = c • φ.toContMDiffSection

@[simp]

theorem TauCeti.SmoothForm.neg_toContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (φ : SmoothForm I M F k) : (-φ).toContMDiffSection = -φ.toContMDiffSection

@[simp]

theorem TauCeti.SmoothForm.sub_toContMDiffSection {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (φ ψ : SmoothForm I M F k) : (φ - ψ).toContMDiffSection = φ.toContMDiffSection - ψ.toContMDiffSection

theorem TauCeti.SmoothForm.add_toRoughForm {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (φ ψ : SmoothForm I M F k) : ↑(φ + ψ) = ↑φ + ↑ψ

The rough form underlying a sum of smooth forms is the sum of their rough forms.

theorem TauCeti.SmoothForm.neg_toRoughForm {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (φ : SmoothForm I M F k) : ↑(-φ) = -↑φ

The rough form underlying the negation of a smooth form is the negation of its rough form.

noncomputable def TauCeti.SmoothForm.funSMulₗ {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (g : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) : SmoothForm I M F k →ₗ[ℝ] SmoothForm I M F k

Multiplication of smooth forms by a smooth real function, as a real-linear map.

@[simp]

theorem TauCeti.SmoothForm.coe_funSMulₗ {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (g : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) (φ : SmoothForm I M F k) : ↑((funSMulₗ g) φ) = fun (x : M) => g x • ↑φ x

The rough form underlying the product of a smooth form with a smooth function is the pointwise product.

theorem TauCeti.SmoothForm.eq_zero_of_finrank_lt {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] [FiniteDimensional ℝ E] (h : Module.finrank ℝ E < k) (φ : SmoothForm I M F k) : φ = 0

A smooth form whose degree exceeds the dimension of the model space vanishes.

noncomputable def TauCeti.SmoothForm.const {V : Type u_6} {F : Type u_7} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} (A : V [⋀^Fin k]→L[ℝ] F) : SmoothForm (modelWithCornersSelf ℝ V) V F k

The constant smooth form whose value is the alternating map A in model-space coordinates.

theorem TauCeti.SmoothForm.const_toRoughForm {V : Type u_6} {F : Type u_7} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} (A : V [⋀^Fin k]→L[ℝ] F) : ↑(const A) = fun (y : V) => A.compContinuousLinearMap ↑(NormedSpace.fromTangentSpace y)

The underlying rough form of const A is A transported to each tangent fibre.

@[simp]

theorem TauCeti.SmoothForm.const_apply {V : Type u_6} {F : Type u_7} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} (A : V [⋀^Fin k]→L[ℝ] F) (x : V) (v : Fin k → TangentSpace (modelWithCornersSelf ℝ V) x) : (↑(const A) x) v = A fun (i : Fin k) => (NormedSpace.fromTangentSpace x) (v i)

Evaluating a constant smooth form transports its arguments back to the model space.

noncomputable def TauCeti.SmoothForm.realLineCoordForm : SmoothForm (modelWithCornersSelf ℝ ℝ) ℝ ℝ 1

The coordinate one-form dz of the real line.

@[simp]

theorem TauCeti.SmoothForm.realLineCoordForm_apply (z : ℝ) (v : Fin 1 → TangentSpace (modelWithCornersSelf ℝ ℝ) z) : (↑realLineCoordForm z) v = v 0

The coordinate one-form dz of the real line sends a tangent vector to itself.

theorem TauCeti.SmoothForm.contMDiff_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {E' : Type u_6} {H' : Type u_7} {N : Type u_8} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} [ENat.LEInfty n] (form : SmoothForm I M F 2) {b : N → M} {V W : (y : N) → TangentSpace I (b y)} (hV : ContMDiff I' I.tangent n fun (y : N) => ⟨b y, V y⟩) (hW : ContMDiff I' I.tangent n fun (y : N) => ⟨b y, W y⟩) : ContMDiff I' (modelWithCornersSelf ℝ F) n fun (y : N) => SmoothBundleForm.eval₂ form (b y) (V y) (W y)

Evaluating a smooth degree-two form on two C^n tangent fields along a C^n map is C^n.

This is the trivial-bundle specialization of SmoothBundleForm.contMDiff_eval₂.

noncomputable def TauCeti.SmoothForm.bilinFormAt {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothForm I M ℝ 2) (x : M) : LinearMap.BilinForm ℝ (TangentSpace I x)

The algebraic bilinear form represented by the value of a real degree-two smooth form.

This generalizes SmoothTwoForm.bilinFormAt from TauCeti.Geometry.Manifold.TwoForm.Basic. The view interoperates with APIs phrased in terms of LinearMap.BilinForm, including the symplectic constructions.

@[simp]

theorem TauCeti.SmoothForm.bilinFormAt_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothForm I M ℝ 2) (x : M) (v w : TangentSpace I x) : ((φ.bilinFormAt x) v) w = SmoothBundleForm.eval₂ φ x v w

theorem TauCeti.SmoothForm.isAlt_bilinFormAt {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothForm I M ℝ 2) (x : M) : (φ.bilinFormAt x).IsAlt

The bilinear form represented by a degree-two smooth form is alternating.

@[simp]

theorem TauCeti.SmoothForm.bilinFormAt_eq_zero_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothForm I M ℝ 2) (x : M) : φ.bilinFormAt x = 0 ↔ ↑φ x = 0

The bilinear form represented by a degree-two smooth form at a point vanishes exactly when the form vanishes there.

def TauCeti.SmoothForm.altAt {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (φ : SmoothForm I M F k) (x : M) : E [⋀^Fin k]→L[ℝ] F

The value of a smooth form as a continuous alternating map on the model fibre.

@[simp]

theorem TauCeti.SmoothForm.altAt_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] {k : ℕ} (φ : SmoothForm I M F k) (x : M) (v : Fin k → E) : (φ.altAt x) v = (↑φ x) v

theorem TauCeti.SmoothForm.altAt_apply_eval₂ {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {I : ModelWithCorners ℝ E H} [IsManifold I 1 M] (φ : SmoothForm I M F 2) (x : M) (v : Fin 2 → E) : (φ.altAt x) v = SmoothBundleForm.eval₂ φ x (v 0) (v 1)

The degree-two alternating-map view evaluated on a tuple agrees with ordered-pair evaluation.