Smooth differential two-forms on manifolds

The generic smooth differential-form carrier already records the alternating map in each tangent fibre. This module supplies the degree-two view used by the symplectic API: SmoothTwoForm is the scalar degree-two specialization, and its bilinear, evaluation, and constant-form operations are derived from SmoothForm.

The degree-two specialization supplies the bilinear view used by the symplectic modules while retaining the generic form's alternating-map and smooth-section structure.

@[reducible, inline]

abbrev TauCeti.SmoothTwoForm {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] : Type (max u_4 u_1)

A smooth real differential two-form is the generic smooth scalar form in degree two.

noncomputable def TauCeti.SmoothTwoForm.const {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] (B : V →L[ℝ] V →L[ℝ] ℝ) : SmoothTwoForm (modelWithCornersSelf ℝ V) V

A continuous bilinear form defines a constant smooth two-form by antisymmetrization: const B evaluates to (B v w - B w v) / 2; when B is alternating, this agrees with B.

theorem TauCeti.SmoothTwoForm.const_eq {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] (B : V →L[ℝ] V →L[ℝ] ℝ) : const B = SmoothForm.const (2⁻¹ • (ContinuousAlternatingMap.alternatizeBilinCLM ℝ V ℝ) B)

The degree-two constructor is the generic constant form in alternating-map coordinates.

theorem TauCeti.SmoothTwoForm.const_apply {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : ∀ (v : V), (B v) v = 0) (x : V) (v w : TangentSpace (modelWithCornersSelf ℝ V) x) : SmoothBundleForm.eval₂ (const B) x v w = (B ((NormedSpace.fromTangentSpace x) v)) ((NormedSpace.fromTangentSpace x) w)

The tangent-space evaluation of a constant smooth two-form.

theorem TauCeti.SmoothTwoForm.const_model_apply {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : ∀ (v : V), (B v) v = 0) (x v w : V) : SmoothBundleForm.eval₂ (const B) x ((NormedSpace.fromTangentSpace x).symm v) ((NormedSpace.fromTangentSpace x).symm w) = (B v) w

The model-space evaluation of a constant smooth two-form.

theorem TauCeti.SmoothTwoForm.eval₂_smul_add_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] [IsManifold I (↑⊤) M] (form : SmoothTwoForm I M) (x : M) (v w : TangentSpace I x) (a b c d : ℝ) : SmoothBundleForm.eval₂ form x (a • v + b • w) (c • v + d • w) = (a * d - b * c) * SmoothBundleForm.eval₂ form x v w

The bilinear expansion of a two-form on a pair of combinations of two tangent vectors: the coefficient is the determinant a d - b c of the coefficient matrix.

theorem TauCeti.SmoothTwoForm.eval₂_smul_add_smul_det {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] [IsManifold I (↑⊤) M] (form : SmoothTwoForm I M) (x : M) (B : ℝ × ℝ →ₗ[ℝ] ℝ × ℝ) (v w : TangentSpace I x) : SmoothBundleForm.eval₂ form x ((B (1, 0)).1 • v + (B (1, 0)).2 • w) ((B (0, 1)).1 • v + (B (0, 1)).2 • w) = LinearMap.det B * SmoothBundleForm.eval₂ form x v w

SmoothTwoForm.eval₂_smul_add_smul with coefficients the images of the coordinate directions under an endomorphism B of ℝ × ℝ: the coefficient is det B.