Twisted products of smooth symplectic forms #
The form on M × N used for Lagrangian correspondences is pr₁*σ - pr₂*τ.
It is the product form TauCeti.SmoothTwoForm.prod of σ and -τ
(TauCeti.SmoothTwoForm.twistedProd_eq_prod_neg), so nondegeneracy and closedness are
inherited from the two factors through the product form. Its value on each tangent
space is the existing linear twisted product. These comparisons let the linear theory
of Lagrangian graphs apply to graphs of maps between manifolds.
Two sign laws govern the operations on correspondences. Exchanging the factors pulls
pr₁*τ - pr₂*σ on N × M back to -(pr₁*σ - pr₂*τ) on M × N
(TauCeti.SmoothTwoForm.mpullback_prodComm_twistedProd), so transposing a relation negates
its form. Regrouping (M × N) × (M' × N') as (M × M') × (N × N') pulls the twisted product
of the product forms back to the product of the twisted products
(TauCeti.SmoothTwoForm.mpullback_prodProdProdComm_twistedProd_prod).
References #
- A. Cannas da Silva, Lectures on Symplectic Geometry, Sections 3 and 5.
- D. McDuff, D. Salamon, Introduction to Symplectic Topology, Section 3.4.
noncomputable def
TauCeti.SmoothTwoForm.twistedProd
{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 twisted product pr₁*σ - pr₂*τ on M × N.
Instances For
theorem
TauCeti.SmoothTwoForm.twistedProd_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 twisted product is the difference of the pullbacks from its factors.
@[simp]
theorem
TauCeti.SmoothTwoForm.twistedProd_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)
:
(↑(σ.twistedProd τ) 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 twisted product on a family of two tangent vectors.
theorem
TauCeti.SmoothTwoForm.twistedProd_eq_prod_neg
{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 twisted product pr₁*σ - pr₂*τ is the product form of σ and -τ.
theorem
TauCeti.SmoothTwoForm.eval₂_twistedProd
{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₂ (σ.twistedProd τ) 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
Evaluation of the twisted product on two product tangent vectors.
theorem
TauCeti.SmoothTwoForm.IsNondegenerate.twistedProd
{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)
:
(σ.twistedProd τ).IsNondegenerate
Nondegenerate factors give a nondegenerate twisted product.
@[simp]
theorem
TauCeti.SmoothTwoForm.IsNondegenerate.symplecticFormAt_twistedProd
{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).twistedProd (hτ.symplecticFormAt p.2)
The tangent-fibre form of a twisted product is the linear twisted product.
theorem
TauCeti.SmoothTwoForm.isClosed_twistedProd
{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 τ)
:
Closed factors give a closed twisted product.
theorem
TauCeti.SmoothTwoForm.IsSymplectic.twistedProd
{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)
:
(σ.twistedProd τ).IsSymplectic
The twisted product of symplectic forms is symplectic.
theorem
TauCeti.SmoothTwoForm.mpullback_prodComm_twistedProd
{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)
:
Exchanging the factors turns the twisted product pr₁*τ - pr₂*σ on N × M into the
negative of the twisted product pr₁*σ - pr₂*τ on M × N.
theorem
TauCeti.SmoothTwoForm.mpullback_prodProdProdComm_twistedProd_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]
{E' : Type u_7}
{H'' : Type u_8}
{M' : Type u_9}
{F' : Type u_10}
{H''' : Type u_11}
{N' : Type u_12}
[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' M')
(τ' : SmoothTwoForm J' N')
:
(SmoothForm.mpullback ⇑(Diffeomorph.prodProdProdComm I J I' J' M N M' N' ↑⊤) ⋯) ((σ.prod σ').twistedProd (τ.prod τ')) = (σ.twistedProd τ).prod (σ'.twistedProd τ')
Regrouping (M × N) × (M' × N') as (M × M') × (N × N') pulls the twisted product of the
product forms back to the product of the twisted products.