Products of isotropic, coisotropic and Lagrangian maps and of symplectic tangent images #
Let σ₁ and σ₂ be nondegenerate two-forms on M₁ and M₂, and give M₁ × M₂ the product form
pr₁*σ₁ + pr₂*σ₂ (TauCeti.SmoothTwoForm.prod). For maps f₁ : N₁ → M₁ and f₂ : N₂ → M₂, the
tangent image of the product map f₁ × f₂ at (x₁, x₂) is the product of the tangent images of
f₁ at x₁ and of f₂ at x₂, and the tangent-space form of the product is the direct sum of
those of the factors. The linear product formulas of
TauCeti.Geometry.Symplectic.Lagrangian.Constructions then show that f₁ × f₂ is isotropic,
coisotropic or Lagrangian, or has symplectic tangent images, exactly when both factors do. This
needs the factors to be differentiable, since the tangent image of a map is taken with mfderiv,
and the sources to be nonempty for the converse: a product with an empty source has empty source
and satisfies every predicate vacuously. In particular a product of Lagrangian immersions is a
Lagrangian immersion.
Main results #
TauCeti.SmoothTwoForm.IsNondegenerate.isIsotropicMap_prodMap_iff,isCoisotropicMap_prodMap_iff,isLagrangianMap_prodMap_iff: a product of differentiable maps from nonempty manifolds is isotropic, coisotropic or Lagrangian exactly when both factors are.TauCeti.SmoothTwoForm.IsNondegenerate.hasSymplecticTangentImages_prodMap_iff: likewise for symplectic tangent images.TauCeti.SmoothTwoForm.IsNondegenerate.IsIsotropicMap.prodMap,IsCoisotropicMap.prodMap,IsLagrangianMap.prodMap,HasSymplecticTangentImages.prodMap: the forward directions, which need no nonempty sources.TauCeti.SmoothTwoForm.IsNondegenerate.IsLagrangianImmersion.prodMap: a product of Lagrangian immersions is a Lagrangian immersion.
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.4.
Tangent images of a product map #
Products of isotropic, coisotropic and Lagrangian maps and of symplectic tangent images #
theorem
TauCeti.SmoothTwoForm.IsNondegenerate.isIsotropicMap_prodMap_iff
{E₁ : Type u_1}
{H₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace ℝ E₁]
[TopologicalSpace H₁]
{I₁ : ModelWithCorners ℝ E₁ H₁}
{M₁ : Type u_3}
[TopologicalSpace M₁]
[ChartedSpace H₁ M₁]
[IsManifold I₁ (↑⊤) M₁]
{E₂ : Type u_4}
{H₂ : Type u_5}
[NormedAddCommGroup E₂]
[NormedSpace ℝ E₂]
[TopologicalSpace H₂]
{I₂ : ModelWithCorners ℝ E₂ H₂}
{M₂ : Type u_6}
[TopologicalSpace M₂]
[ChartedSpace H₂ M₂]
[IsManifold I₂ (↑⊤) M₂]
{F₁ : Type u_7}
{G₁ : Type u_8}
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[TopologicalSpace G₁]
{J₁ : ModelWithCorners ℝ F₁ G₁}
{N₁ : Type u_9}
[TopologicalSpace N₁]
[ChartedSpace G₁ N₁]
{F₂ : Type u_10}
{G₂ : Type u_11}
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[TopologicalSpace G₂]
{J₂ : ModelWithCorners ℝ F₂ G₂}
{N₂ : Type u_12}
[TopologicalSpace N₂]
[ChartedSpace G₂ N₂]
{σ₁ : SmoothTwoForm I₁ M₁}
{σ₂ : SmoothTwoForm I₂ M₂}
{hσ₁ : σ₁.IsNondegenerate}
{hσ₂ : σ₂.IsNondegenerate}
{f₁ : N₁ → M₁}
{f₂ : N₂ → M₂}
[Nonempty N₁]
[Nonempty N₂]
(hf₁ : MDiff f₁)
(hf₂ : MDiff f₂)
:
IsIsotropicMap (J₁.prod J₂) ⋯ (Prod.map f₁ f₂) ↔ IsIsotropicMap J₁ hσ₁ f₁ ∧ IsIsotropicMap J₂ hσ₂ f₂
A product of differentiable maps from nonempty manifolds is isotropic for the product form exactly when both factors are isotropic.
theorem
TauCeti.SmoothTwoForm.IsNondegenerate.isCoisotropicMap_prodMap_iff
{E₁ : Type u_1}
{H₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace ℝ E₁]
[TopologicalSpace H₁]
{I₁ : ModelWithCorners ℝ E₁ H₁}
{M₁ : Type u_3}
[TopologicalSpace M₁]
[ChartedSpace H₁ M₁]
[IsManifold I₁ (↑⊤) M₁]
{E₂ : Type u_4}
{H₂ : Type u_5}
[NormedAddCommGroup E₂]
[NormedSpace ℝ E₂]
[TopologicalSpace H₂]
{I₂ : ModelWithCorners ℝ E₂ H₂}
{M₂ : Type u_6}
[TopologicalSpace M₂]
[ChartedSpace H₂ M₂]
[IsManifold I₂ (↑⊤) M₂]
{F₁ : Type u_7}
{G₁ : Type u_8}
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[TopologicalSpace G₁]
{J₁ : ModelWithCorners ℝ F₁ G₁}
{N₁ : Type u_9}
[TopologicalSpace N₁]
[ChartedSpace G₁ N₁]
{F₂ : Type u_10}
{G₂ : Type u_11}
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[TopologicalSpace G₂]
{J₂ : ModelWithCorners ℝ F₂ G₂}
{N₂ : Type u_12}
[TopologicalSpace N₂]
[ChartedSpace G₂ N₂]
{σ₁ : SmoothTwoForm I₁ M₁}
{σ₂ : SmoothTwoForm I₂ M₂}
{hσ₁ : σ₁.IsNondegenerate}
{hσ₂ : σ₂.IsNondegenerate}
{f₁ : N₁ → M₁}
{f₂ : N₂ → M₂}
[Nonempty N₁]
[Nonempty N₂]
(hf₁ : MDiff f₁)
(hf₂ : MDiff f₂)
:
IsCoisotropicMap (J₁.prod J₂) ⋯ (Prod.map f₁ f₂) ↔ IsCoisotropicMap J₁ hσ₁ f₁ ∧ IsCoisotropicMap J₂ hσ₂ f₂
A product of differentiable maps from nonempty manifolds is coisotropic for the product form exactly when both factors are coisotropic.
theorem
TauCeti.SmoothTwoForm.IsNondegenerate.isLagrangianMap_prodMap_iff
{E₁ : Type u_1}
{H₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace ℝ E₁]
[TopologicalSpace H₁]
{I₁ : ModelWithCorners ℝ E₁ H₁}
{M₁ : Type u_3}
[TopologicalSpace M₁]
[ChartedSpace H₁ M₁]
[IsManifold I₁ (↑⊤) M₁]
{E₂ : Type u_4}
{H₂ : Type u_5}
[NormedAddCommGroup E₂]
[NormedSpace ℝ E₂]
[TopologicalSpace H₂]
{I₂ : ModelWithCorners ℝ E₂ H₂}
{M₂ : Type u_6}
[TopologicalSpace M₂]
[ChartedSpace H₂ M₂]
[IsManifold I₂ (↑⊤) M₂]
{F₁ : Type u_7}
{G₁ : Type u_8}
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[TopologicalSpace G₁]
{J₁ : ModelWithCorners ℝ F₁ G₁}
{N₁ : Type u_9}
[TopologicalSpace N₁]
[ChartedSpace G₁ N₁]
{F₂ : Type u_10}
{G₂ : Type u_11}
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[TopologicalSpace G₂]
{J₂ : ModelWithCorners ℝ F₂ G₂}
{N₂ : Type u_12}
[TopologicalSpace N₂]
[ChartedSpace G₂ N₂]
{σ₁ : SmoothTwoForm I₁ M₁}
{σ₂ : SmoothTwoForm I₂ M₂}
{hσ₁ : σ₁.IsNondegenerate}
{hσ₂ : σ₂.IsNondegenerate}
{f₁ : N₁ → M₁}
{f₂ : N₂ → M₂}
[Nonempty N₁]
[Nonempty N₂]
(hf₁ : MDiff f₁)
(hf₂ : MDiff f₂)
:
IsLagrangianMap (J₁.prod J₂) ⋯ (Prod.map f₁ f₂) ↔ IsLagrangianMap J₁ hσ₁ f₁ ∧ IsLagrangianMap J₂ hσ₂ f₂
A product of differentiable maps from nonempty manifolds is Lagrangian for the product form exactly when both factors are Lagrangian.
theorem
TauCeti.SmoothTwoForm.IsNondegenerate.hasSymplecticTangentImages_prodMap_iff
{E₁ : Type u_1}
{H₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace ℝ E₁]
[TopologicalSpace H₁]
{I₁ : ModelWithCorners ℝ E₁ H₁}
{M₁ : Type u_3}
[TopologicalSpace M₁]
[ChartedSpace H₁ M₁]
[IsManifold I₁ (↑⊤) M₁]
{E₂ : Type u_4}
{H₂ : Type u_5}
[NormedAddCommGroup E₂]
[NormedSpace ℝ E₂]
[TopologicalSpace H₂]
{I₂ : ModelWithCorners ℝ E₂ H₂}
{M₂ : Type u_6}
[TopologicalSpace M₂]
[ChartedSpace H₂ M₂]
[IsManifold I₂ (↑⊤) M₂]
{F₁ : Type u_7}
{G₁ : Type u_8}
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[TopologicalSpace G₁]
{J₁ : ModelWithCorners ℝ F₁ G₁}
{N₁ : Type u_9}
[TopologicalSpace N₁]
[ChartedSpace G₁ N₁]
{F₂ : Type u_10}
{G₂ : Type u_11}
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[TopologicalSpace G₂]
{J₂ : ModelWithCorners ℝ F₂ G₂}
{N₂ : Type u_12}
[TopologicalSpace N₂]
[ChartedSpace G₂ N₂]
{σ₁ : SmoothTwoForm I₁ M₁}
{σ₂ : SmoothTwoForm I₂ M₂}
{hσ₁ : σ₁.IsNondegenerate}
{hσ₂ : σ₂.IsNondegenerate}
{f₁ : N₁ → M₁}
{f₂ : N₂ → M₂}
[Nonempty N₁]
[Nonempty N₂]
(hf₁ : MDiff f₁)
(hf₂ : MDiff f₂)
:
HasSymplecticTangentImages (J₁.prod J₂) ⋯ (Prod.map f₁ f₂) ↔ HasSymplecticTangentImages J₁ hσ₁ f₁ ∧ HasSymplecticTangentImages J₂ hσ₂ f₂
A product of differentiable maps from nonempty manifolds has symplectic tangent images for the product form exactly when both factors have symplectic tangent images.
theorem
TauCeti.SmoothTwoForm.IsNondegenerate.IsIsotropicMap.prodMap
{E₁ : Type u_1}
{H₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace ℝ E₁]
[TopologicalSpace H₁]
{I₁ : ModelWithCorners ℝ E₁ H₁}
{M₁ : Type u_3}
[TopologicalSpace M₁]
[ChartedSpace H₁ M₁]
[IsManifold I₁ (↑⊤) M₁]
{E₂ : Type u_4}
{H₂ : Type u_5}
[NormedAddCommGroup E₂]
[NormedSpace ℝ E₂]
[TopologicalSpace H₂]
{I₂ : ModelWithCorners ℝ E₂ H₂}
{M₂ : Type u_6}
[TopologicalSpace M₂]
[ChartedSpace H₂ M₂]
[IsManifold I₂ (↑⊤) M₂]
{F₁ : Type u_7}
{G₁ : Type u_8}
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[TopologicalSpace G₁]
{J₁ : ModelWithCorners ℝ F₁ G₁}
{N₁ : Type u_9}
[TopologicalSpace N₁]
[ChartedSpace G₁ N₁]
{F₂ : Type u_10}
{G₂ : Type u_11}
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[TopologicalSpace G₂]
{J₂ : ModelWithCorners ℝ F₂ G₂}
{N₂ : Type u_12}
[TopologicalSpace N₂]
[ChartedSpace G₂ N₂]
{σ₁ : SmoothTwoForm I₁ M₁}
{σ₂ : SmoothTwoForm I₂ M₂}
{hσ₁ : σ₁.IsNondegenerate}
{hσ₂ : σ₂.IsNondegenerate}
{f₁ : N₁ → M₁}
{f₂ : N₂ → M₂}
(h₁ : IsIsotropicMap J₁ hσ₁ f₁)
(h₂ : IsIsotropicMap J₂ hσ₂ f₂)
(hf₁ : MDiff f₁)
(hf₂ : MDiff f₂)
:
IsIsotropicMap (J₁.prod J₂) ⋯ (Prod.map f₁ f₂)
A product of differentiable isotropic maps is isotropic for the product form.
theorem
TauCeti.SmoothTwoForm.IsNondegenerate.IsCoisotropicMap.prodMap
{E₁ : Type u_1}
{H₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace ℝ E₁]
[TopologicalSpace H₁]
{I₁ : ModelWithCorners ℝ E₁ H₁}
{M₁ : Type u_3}
[TopologicalSpace M₁]
[ChartedSpace H₁ M₁]
[IsManifold I₁ (↑⊤) M₁]
{E₂ : Type u_4}
{H₂ : Type u_5}
[NormedAddCommGroup E₂]
[NormedSpace ℝ E₂]
[TopologicalSpace H₂]
{I₂ : ModelWithCorners ℝ E₂ H₂}
{M₂ : Type u_6}
[TopologicalSpace M₂]
[ChartedSpace H₂ M₂]
[IsManifold I₂ (↑⊤) M₂]
{F₁ : Type u_7}
{G₁ : Type u_8}
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[TopologicalSpace G₁]
{J₁ : ModelWithCorners ℝ F₁ G₁}
{N₁ : Type u_9}
[TopologicalSpace N₁]
[ChartedSpace G₁ N₁]
{F₂ : Type u_10}
{G₂ : Type u_11}
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[TopologicalSpace G₂]
{J₂ : ModelWithCorners ℝ F₂ G₂}
{N₂ : Type u_12}
[TopologicalSpace N₂]
[ChartedSpace G₂ N₂]
{σ₁ : SmoothTwoForm I₁ M₁}
{σ₂ : SmoothTwoForm I₂ M₂}
{hσ₁ : σ₁.IsNondegenerate}
{hσ₂ : σ₂.IsNondegenerate}
{f₁ : N₁ → M₁}
{f₂ : N₂ → M₂}
(h₁ : IsCoisotropicMap J₁ hσ₁ f₁)
(h₂ : IsCoisotropicMap J₂ hσ₂ f₂)
(hf₁ : MDiff f₁)
(hf₂ : MDiff f₂)
:
IsCoisotropicMap (J₁.prod J₂) ⋯ (Prod.map f₁ f₂)
A product of differentiable coisotropic maps is coisotropic for the product form.
theorem
TauCeti.SmoothTwoForm.IsNondegenerate.IsLagrangianMap.prodMap
{E₁ : Type u_1}
{H₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace ℝ E₁]
[TopologicalSpace H₁]
{I₁ : ModelWithCorners ℝ E₁ H₁}
{M₁ : Type u_3}
[TopologicalSpace M₁]
[ChartedSpace H₁ M₁]
[IsManifold I₁ (↑⊤) M₁]
{E₂ : Type u_4}
{H₂ : Type u_5}
[NormedAddCommGroup E₂]
[NormedSpace ℝ E₂]
[TopologicalSpace H₂]
{I₂ : ModelWithCorners ℝ E₂ H₂}
{M₂ : Type u_6}
[TopologicalSpace M₂]
[ChartedSpace H₂ M₂]
[IsManifold I₂ (↑⊤) M₂]
{F₁ : Type u_7}
{G₁ : Type u_8}
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[TopologicalSpace G₁]
{J₁ : ModelWithCorners ℝ F₁ G₁}
{N₁ : Type u_9}
[TopologicalSpace N₁]
[ChartedSpace G₁ N₁]
{F₂ : Type u_10}
{G₂ : Type u_11}
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[TopologicalSpace G₂]
{J₂ : ModelWithCorners ℝ F₂ G₂}
{N₂ : Type u_12}
[TopologicalSpace N₂]
[ChartedSpace G₂ N₂]
{σ₁ : SmoothTwoForm I₁ M₁}
{σ₂ : SmoothTwoForm I₂ M₂}
{hσ₁ : σ₁.IsNondegenerate}
{hσ₂ : σ₂.IsNondegenerate}
{f₁ : N₁ → M₁}
{f₂ : N₂ → M₂}
(h₁ : IsLagrangianMap J₁ hσ₁ f₁)
(h₂ : IsLagrangianMap J₂ hσ₂ f₂)
(hf₁ : MDiff f₁)
(hf₂ : MDiff f₂)
:
IsLagrangianMap (J₁.prod J₂) ⋯ (Prod.map f₁ f₂)
A product of differentiable Lagrangian maps is Lagrangian for the product form.
theorem
TauCeti.SmoothTwoForm.IsNondegenerate.HasSymplecticTangentImages.prodMap
{E₁ : Type u_1}
{H₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace ℝ E₁]
[TopologicalSpace H₁]
{I₁ : ModelWithCorners ℝ E₁ H₁}
{M₁ : Type u_3}
[TopologicalSpace M₁]
[ChartedSpace H₁ M₁]
[IsManifold I₁ (↑⊤) M₁]
{E₂ : Type u_4}
{H₂ : Type u_5}
[NormedAddCommGroup E₂]
[NormedSpace ℝ E₂]
[TopologicalSpace H₂]
{I₂ : ModelWithCorners ℝ E₂ H₂}
{M₂ : Type u_6}
[TopologicalSpace M₂]
[ChartedSpace H₂ M₂]
[IsManifold I₂ (↑⊤) M₂]
{F₁ : Type u_7}
{G₁ : Type u_8}
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[TopologicalSpace G₁]
{J₁ : ModelWithCorners ℝ F₁ G₁}
{N₁ : Type u_9}
[TopologicalSpace N₁]
[ChartedSpace G₁ N₁]
{F₂ : Type u_10}
{G₂ : Type u_11}
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[TopologicalSpace G₂]
{J₂ : ModelWithCorners ℝ F₂ G₂}
{N₂ : Type u_12}
[TopologicalSpace N₂]
[ChartedSpace G₂ N₂]
{σ₁ : SmoothTwoForm I₁ M₁}
{σ₂ : SmoothTwoForm I₂ M₂}
{hσ₁ : σ₁.IsNondegenerate}
{hσ₂ : σ₂.IsNondegenerate}
{f₁ : N₁ → M₁}
{f₂ : N₂ → M₂}
(h₁ : HasSymplecticTangentImages J₁ hσ₁ f₁)
(h₂ : HasSymplecticTangentImages J₂ hσ₂ f₂)
(hf₁ : MDiff f₁)
(hf₂ : MDiff f₂)
:
HasSymplecticTangentImages (J₁.prod J₂) ⋯ (Prod.map f₁ f₂)
A product of differentiable maps with symplectic tangent images has symplectic tangent images for the product form.
theorem
TauCeti.SmoothTwoForm.IsNondegenerate.IsLagrangianImmersion.prodMap
{E₁ : Type u_1}
{H₁ : Type u_2}
[NormedAddCommGroup E₁]
[NormedSpace ℝ E₁]
[TopologicalSpace H₁]
{I₁ : ModelWithCorners ℝ E₁ H₁}
{M₁ : Type u_3}
[TopologicalSpace M₁]
[ChartedSpace H₁ M₁]
[IsManifold I₁ (↑⊤) M₁]
{E₂ : Type u_4}
{H₂ : Type u_5}
[NormedAddCommGroup E₂]
[NormedSpace ℝ E₂]
[TopologicalSpace H₂]
{I₂ : ModelWithCorners ℝ E₂ H₂}
{M₂ : Type u_6}
[TopologicalSpace M₂]
[ChartedSpace H₂ M₂]
[IsManifold I₂ (↑⊤) M₂]
{F₁ : Type u_7}
{G₁ : Type u_8}
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[TopologicalSpace G₁]
{J₁ : ModelWithCorners ℝ F₁ G₁}
{N₁ : Type u_9}
[TopologicalSpace N₁]
[ChartedSpace G₁ N₁]
{F₂ : Type u_10}
{G₂ : Type u_11}
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[TopologicalSpace G₂]
{J₂ : ModelWithCorners ℝ F₂ G₂}
{N₂ : Type u_12}
[TopologicalSpace N₂]
[ChartedSpace G₂ N₂]
{σ₁ : SmoothTwoForm I₁ M₁}
{σ₂ : SmoothTwoForm I₂ M₂}
{hσ₁ : σ₁.IsNondegenerate}
{hσ₂ : σ₂.IsNondegenerate}
{f₁ : N₁ → M₁}
{f₂ : N₂ → M₂}
[FiniteDimensional ℝ E₁]
[FiniteDimensional ℝ E₂]
[FiniteDimensional ℝ F₁]
[FiniteDimensional ℝ F₂]
[IsManifold J₁ (↑⊤) N₁]
[IsManifold J₂ (↑⊤) N₂]
(h₁ : IsLagrangianImmersion J₁ hσ₁ f₁)
(h₂ : IsLagrangianImmersion J₂ hσ₂ f₂)
:
IsLagrangianImmersion (J₁.prod J₂) ⋯ (Prod.map f₁ f₂)
A product of Lagrangian immersions is a Lagrangian immersion for the product form.