Coordinate continuity of regular differential forms

The coordinate expression of a differential form is the fiber coordinate of its section in the existing alternating tangent-bundle trivialization. Consequently even C⁰ section regularity implies coordinate continuity on the extended chart target, including boundary and corner points. The zero set of a regular form is closed, as can be checked in local bundle trivializations.

theorem TauCeti.RoughForm.inChartAt_eq_trivializationAt {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} (φ : RoughForm I M F k) (α : M) {z : E} (hz : z ∈ (extChartAt I α).target) : φ.inChartAt α z = (↑(trivializationAt (E [⋀^Fin k]→L[ℝ] F) (fun (x : M) => TangentSpace I x [⋀^Fin k]→L[ℝ] F) α) ⟨↑(extChartAt I α).symm z, φ (↑(extChartAt I α).symm z)⟩).2

On an extended chart target, the form's coordinate expression is exactly its section's fiber coordinate in the preferred alternating-bundle trivialization.

theorem TauCeti.RoughForm.trivializationAt_snd_eventuallyEq_inChartAt {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} (φ : RoughForm I M F k) (α : M) : (fun (z : E) => (↑(trivializationAt (E [⋀^Fin k]→L[ℝ] F) (fun (x : M) => TangentSpace I x [⋀^Fin k]→L[ℝ] F) α) ⟨↑(extChartAt I α).symm z, φ (↑(extChartAt I α).symm z)⟩).2) =ᶠ[nhdsWithin (↑(extChartAt I α) α) (Set.range ↑I)] φ.inChartAt α

Within the model range near the image of the chart centre, the section's fiber coordinate in the preferred alternating-bundle trivialization is the form's coordinate expression.

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

Every regular fixed-coefficient form, including a C⁰ form, has continuous coordinate coefficients on each preferred extended chart target.

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

The zero set of a regular differential form is closed, including for a continuous form. Neither closedness of the form nor a Hausdorff base is needed.