Constant rescaling of smooth symplectic forms

Multiplication by a nonzero real constant preserves nondegeneracy and symplecticity of a smooth two-form. Its tangent-space symplectic forms are the rescalings of the original tangent-space forms. Consequently symplectic complements and all four linear subspace predicates are unchanged. This comparison allows the linear rescaling API to apply directly to tangent images of immersed or embedded submanifolds, including when the scale is negative.

Primitives scale by the same constant, with the convention σ = -dθ.

The conventions follow McDuff--Salamon, Introduction to Symplectic Topology, Section 3.4.

@[simp]

theorem TauCeti.SmoothTwoForm.isNondegenerate_smul_iff {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] {σ : SmoothTwoForm I M} (c : ℝ) (hc : c ≠ 0) : (c • σ).IsNondegenerate ↔ σ.IsNondegenerate

Nonzero constant rescaling preserves and reflects fiberwise nondegeneracy.

theorem TauCeti.SmoothTwoForm.IsNondegenerate.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] {σ : SmoothTwoForm I M} (hσ : σ.IsNondegenerate) (c : ℝ) (hc : c ≠ 0) : (c • σ).IsNondegenerate

A nonzero multiple of a nondegenerate smooth two-form is nondegenerate.

@[simp]

theorem TauCeti.SmoothTwoForm.isNondegenerate_neg_iff {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] {σ : SmoothTwoForm I M} : (-σ).IsNondegenerate ↔ σ.IsNondegenerate

Negation preserves and reflects fiberwise nondegeneracy.

theorem TauCeti.SmoothTwoForm.IsSymplectic.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] {σ : SmoothTwoForm I M} (hσ : σ.IsSymplectic) (c : ℝ) (hc : c ≠ 0) : (c • σ).IsSymplectic

A nonzero multiple of a symplectic form is symplectic.

@[simp]

theorem TauCeti.SmoothTwoForm.isSymplectic_smul_iff {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] {σ : SmoothTwoForm I M} (c : ℝ) (hc : c ≠ 0) : (c • σ).IsSymplectic ↔ σ.IsSymplectic

Nonzero constant rescaling preserves and reflects symplecticity.

@[simp]

theorem TauCeti.SmoothTwoForm.isSymplectic_neg_iff {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] {σ : SmoothTwoForm I M} : (-σ).IsSymplectic ↔ σ.IsSymplectic

Negation preserves and reflects symplecticity.

@[simp]

theorem TauCeti.SmoothTwoForm.IsNondegenerate.symplecticFormAt_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] {σ : SmoothTwoForm I M} (hσ : σ.IsNondegenerate) (c : ℝ) (hc : c ≠ 0) (x : M) : ⋯.symplecticFormAt x = (hσ.symplecticFormAt x).rescale c hc

The tangent-space symplectic form of a constant multiple is the corresponding linear rescaling.

theorem TauCeti.SmoothTwoForm.smul_eq_neg_mextDerivₗ {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] {σ : SmoothTwoForm I M} (θ : SmoothForm I M ℝ 1) (hθ : σ = -(mextDerivₗ I 1) θ) (c : ℝ) : c • σ = -(mextDerivₗ I 1) (c • θ)

Constant rescaling preserves the convention relating a symplectic form and its chosen primitive, including negative scale factors.