Products of smooth symplectic forms #
The product of two manifolds (M, σ) and (N, τ) carrying two-forms carries the product form
pr₁*σ + pr₂*τ (TauCeti.SmoothTwoForm.prod σ τ). On the tangent space at p = (x, y), which
is T_x M × T_y N, it pairs (v, w) with (v', w') to σ(v, v') + τ(w, w'), so its value on
each tangent space is the linear direct-sum form TauCeti.SymplecticForm.prod. Nondegeneracy and
closedness are inherited from the factors, so the product of two symplectic manifolds is a
symplectic manifold. This is the symplectic structure in which products of isotropic,
coisotropic and Lagrangian submanifolds of the factors are again of the same kind
(TauCeti.Geometry.Symplectic.Lagrangian.Prod).
Main declarations #
TauCeti.SmoothTwoForm.prod: the product formpr₁*σ + pr₂*τonM × N.TauCeti.SmoothTwoForm.prod_apply,TauCeti.SmoothTwoForm.eval₂_prod: its evaluation on the components of tangent vectors.TauCeti.SmoothTwoForm.IsNondegenerate.prod,TauCeti.SmoothTwoForm.IsNondegenerate.symplecticFormAt_prod: nondegenerate factors give a nondegenerate product, whose tangent-space forms are the linear direct sums.TauCeti.SmoothTwoForm.isClosed_prod,TauCeti.SmoothTwoForm.IsSymplectic.prod: closed, respectively symplectic, factors give a closed, respectively symplectic, product.
References #
- A. Cannas da Silva, Lectures on Symplectic Geometry, Lecture Notes in Mathematics 1764, Springer, 2001, Section 3.
- D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 3.1.
noncomputable def
TauCeti.SmoothTwoForm.prod
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_4}
{H' : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J (↑⊤) N]
(σ : SmoothTwoForm I M)
(τ : SmoothTwoForm J N)
:
SmoothTwoForm (I.prod J) (M × N)
The product form pr₁*σ + pr₂*τ on M × N of two-forms σ on M and τ on N.
Instances For
theorem
TauCeti.SmoothTwoForm.prod_def
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_4}
{H' : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J (↑⊤) N]
(σ : SmoothTwoForm I M)
(τ : SmoothTwoForm J N)
:
The product form is the sum of the pullbacks from its factors.
@[simp]
theorem
TauCeti.SmoothTwoForm.prod_apply
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_4}
{H' : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J (↑⊤) N]
(σ : SmoothTwoForm I M)
(τ : SmoothTwoForm J N)
(p : M × N)
(v : Fin 2 → TangentSpace (I.prod J) p)
:
(↑(σ.prod τ) p) v = ((↑σ p.1) fun (i : Fin 2) => ((Manifold.tangentSpaceProdEquiv p) (v i)).1) + (↑τ p.2) fun (i : Fin 2) => ((Manifold.tangentSpaceProdEquiv p) (v i)).2
Evaluation of the product form on a family of two tangent vectors.
theorem
TauCeti.SmoothTwoForm.eval₂_prod
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_4}
{H' : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J (↑⊤) N]
(σ : SmoothTwoForm I M)
(τ : SmoothTwoForm J N)
(p : M × N)
(v w : TangentSpace (I.prod J) p)
:
SmoothBundleForm.eval₂ (σ.prod τ) p v w = SmoothBundleForm.eval₂ σ p.1 ((Manifold.tangentSpaceProdEquiv p) v).1 ((Manifold.tangentSpaceProdEquiv p) w).1 + SmoothBundleForm.eval₂ τ p.2 ((Manifold.tangentSpaceProdEquiv p) v).2 ((Manifold.tangentSpaceProdEquiv p) w).2
The product form evaluates on two tangent vectors of M × N as the sum of the factor forms
on their components.
theorem
TauCeti.SmoothTwoForm.IsNondegenerate.prod
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_4}
{H' : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J (↑⊤) N]
{σ : SmoothTwoForm I M}
{τ : SmoothTwoForm J N}
(hσ : σ.IsNondegenerate)
(hτ : τ.IsNondegenerate)
:
(σ.prod τ).IsNondegenerate
Nondegenerate factors give a nondegenerate product form.
@[simp]
theorem
TauCeti.SmoothTwoForm.IsNondegenerate.symplecticFormAt_prod
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_4}
{H' : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J (↑⊤) N]
{σ : SmoothTwoForm I M}
{τ : SmoothTwoForm J N}
(hσ : σ.IsNondegenerate)
(hτ : τ.IsNondegenerate)
(p : M × N)
:
(⋯.symplecticFormAt p).transport ↑(Manifold.tangentSpaceProdEquiv p) = (hσ.symplecticFormAt p.1).prod (hτ.symplecticFormAt p.2)
The tangent-space form of a product of nondegenerate forms is, under the identification
T_(x, y) (M × N) = T_x M × T_y N, the linear direct sum of the tangent-space forms of the
factors.
theorem
TauCeti.SmoothTwoForm.isClosed_prod
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_4}
{H' : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J (↑⊤) N]
{σ : SmoothTwoForm I M}
{τ : SmoothTwoForm J N}
(hσ : SmoothForm.IsClosed σ)
(hτ : SmoothForm.IsClosed τ)
:
SmoothForm.IsClosed (σ.prod τ)
Closed factors give a closed product form.
theorem
TauCeti.SmoothTwoForm.IsSymplectic.prod
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_4}
{H' : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J (↑⊤) N]
{σ : SmoothTwoForm I M}
{τ : SmoothTwoForm J N}
(hσ : σ.IsSymplectic)
(hτ : τ.IsSymplectic)
:
(σ.prod τ).IsSymplectic
The product of symplectic manifolds is symplectic.