Maps with symplectic tangent images

Let σ be a fiberwise nondegenerate smooth two-form on M, so that every tangent space T_y M carries the linear symplectic form hσ.symplecticFormAt y. A map f : N → M has symplectic tangent images when, at every point x of N, its tangent image df_x(T_x N), the range of the differential, is a symplectic subspace of T_(f x) M in the sense of TauCeti.SymplecticForm.IsSymplectic: it meets its symplectic complement only in zero, equivalently σ restricts to it nondegenerately. This is the fourth of the tangent-image predicates, beside the isotropic, coisotropic and Lagrangian maps of TauCeti.Geometry.Symplectic.Lagrangian.Manifold. It is not called a symplectic map, a term which conventionally means a map pulling one symplectic form back to another.

As for the other three predicates, the differential is mfderiv, which is 0 where f is not differentiable, the source is an arbitrary charted space, and f need not be injective, so the predicate applies to embedded and immersed submanifolds alike, through any parametrization.

• Pointwise, f has symplectic tangent images exactly when a tangent vector df_x v pairing to zero with every df_x w is itself zero (TauCeti.SmoothTwoForm.IsNondegenerate.hasSymplecticTangentImages_iff).
• A smooth map pulls σ back to a nondegenerate form exactly when its differentials are injective and its tangent images are symplectic (isNondegenerate_mpullback_iff). So an immersion with symplectic tangent images pulls a symplectic form back to a symplectic form; for embeddings this is the condition defining symplectic submanifolds.
• The predicate depends only on the tangent images, hence not on the parametrization, and it is transported by symplectomorphisms of the target.
• A symplectic tangent image has even dimension, so a map with symplectic tangent images and an injective differential at some point comes from an even-dimensional manifold. In a finite-dimensional target each tangent image splits off together with its symplectic complement, T_(f x) M = df_x(T_x N) ⊕ df_x(T_x N)^σ; for an embedding these complements are the fibres of the symplectic normal bundle.
• A map with surjective differentials, such as a local diffeomorphism, has symplectic tangent images. In a finite-dimensional symplectic vector space with its constant form, a continuous linear map has symplectic tangent images exactly when its range is a symplectic subspace; for instance the inclusion of the first factor of a direct sum of symplectic vector spaces does.

Main declarations

• TauCeti.SmoothTwoForm.IsNondegenerate.HasSymplecticTangentImages: the predicate.
• TauCeti.SmoothTwoForm.IsNondegenerate.isNondegenerate_mpullback_iff: a smooth map pulls σ back to a nondegenerate form exactly when its differentials are injective and its tangent images are symplectic.
• TauCeti.SmoothTwoForm.IsNondegenerate.HasSymplecticTangentImages.isSymplectic_mpullback: such a map pulls a symplectic form back to a symplectic form.
• TauCeti.SmoothTwoForm.IsNondegenerate.hasSymplecticTangentImages_comp_diffeomorph_iff and hasSymplecticTangentImages_diffeomorph_comp_iff: reparametrization and transport.
• TauCeti.SmoothTwoForm.IsNondegenerate.HasSymplecticTangentImages.even_finrank: the source dimension is even.
• TauCeti.SmoothTwoForm.IsNondegenerate.HasSymplecticTangentImages.isCompl: the splitting of the ambient tangent space.

References

• D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 2.1 (symplectic subspaces and complements).
• A. Cannas da Silva, Lectures on Symplectic Geometry, Lecture Notes in Mathematics 1764, Springer, 2001, Chapters 1 and 3.

def TauCeti.SmoothTwoForm.IsNondegenerate.HasSymplecticTangentImages {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'] (J : ModelWithCorners ℝ E' H') {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} (hσ : σ.IsNondegenerate) (f : N → M) : Prop

A map f : N → M has symplectic tangent images for a nondegenerate two-form σ when every tangent image df_x(T_x N) is a symplectic subspace of (T_(f x) M, σ_(f x)): it meets its symplectic complement only in zero, equivalently σ_(f x) restricts to it nondegenerately.

The tangent image is taken with mfderiv, which is 0 at points where f is not differentiable; the zero subspace is symplectic, so there the condition holds trivially.

theorem TauCeti.SmoothTwoForm.IsNondegenerate.hasSymplecticTangentImages_iff_forall {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'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {f : N → M} : HasSymplecticTangentImages J hσ f ↔ ∀ (x : N), (hσ.symplecticFormAt (f x)).IsSymplectic (↑(mfderiv% f x)).range

Having symplectic tangent images is the pointwise condition on the tangent images.

theorem TauCeti.SmoothTwoForm.IsNondegenerate.hasSymplecticTangentImages_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'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {f : N → M} : HasSymplecticTangentImages J hσ f ↔ ∀ (x : N) (v : TangentSpace J x), (∀ (w : TangentSpace J x), SmoothBundleForm.eval₂ σ (f x) ((mfderiv% f x) v) ((mfderiv% f x) w) = 0) → (mfderiv% f x) v = 0

A map has symplectic tangent images exactly when, at every point, a pushed-forward tangent vector on which σ pairs to zero with every pushed-forward tangent vector is itself zero.

theorem TauCeti.SmoothTwoForm.IsNondegenerate.isNondegenerate_mpullback_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'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {f : N → M} [IsManifold J (↑⊤) N] (hf : ContMDiff J I (↑⊤) f) : IsNondegenerate ((SmoothForm.mpullback f hf) σ) ↔ HasSymplecticTangentImages J hσ f ∧ ∀ (x : N), Function.Injective ⇑(mfderiv% f x)

Symplectic tangent images and the pulled-back form. A smooth map pulls σ back to a nondegenerate form exactly when its differentials are injective and its tangent images are symplectic. In particular an immersion has symplectic tangent images exactly when the pulled-back form is nondegenerate.

theorem TauCeti.SmoothTwoForm.IsNondegenerate.HasSymplecticTangentImages.isSymplectic_mpullback {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'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {f : N → M} [IsManifold J (↑⊤) N] (h : HasSymplecticTangentImages J hσ f) (hσs : σ.IsSymplectic) (hf : ContMDiff J I (↑⊤) f) (hinj : ∀ (x : N), Function.Injective ⇑(mfderiv% f x)) : IsSymplectic ((SmoothForm.mpullback f hf) σ)

A smooth map with injective differentials and symplectic tangent images pulls a symplectic form back to a symplectic form.

theorem TauCeti.SmoothTwoForm.IsNondegenerate.hasSymplecticTangentImages_of_surjective {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'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {f : N → M} (hf : ∀ (x : N), Function.Surjective ⇑(mfderiv% f x)) : HasSymplecticTangentImages J hσ f

A map whose differentials are all surjective, such as a local diffeomorphism, has symplectic tangent images.

Reparametrization and transport

theorem TauCeti.SmoothTwoForm.IsNondegenerate.hasSymplecticTangentImages_comp_diffeomorph_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'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {f : N → M} {E'' : Type u_7} {H'' : Type u_8} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] {K : ModelWithCorners ℝ E'' H''} {P : Type u_9} [TopologicalSpace P] [ChartedSpace H'' P] {n : WithTop ℕ∞} (φ : Diffeomorph K J P N n) (hn : n ≠ 0) : HasSymplecticTangentImages K hσ (f ∘ ⇑φ) ↔ HasSymplecticTangentImages J hσ f

Independence of the parametrization. Precomposing with a diffeomorphism of the source does not change whether a map has symplectic tangent images.

theorem TauCeti.SmoothTwoForm.IsNondegenerate.hasSymplecticTangentImages_diffeomorph_comp_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'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {f : N → M} {E₂ : Type u_7} {H₂ : Type u_8} [NormedAddCommGroup E₂] [NormedSpace ℝ E₂] [TopologicalSpace H₂] {I₂ : ModelWithCorners ℝ E₂ H₂} {M₂ : Type u_9} [TopologicalSpace M₂] [ChartedSpace H₂ M₂] [IsManifold I₂ (↑⊤) M₂] {σ₂ : SmoothTwoForm I₂ M₂} {hσ₂ : σ₂.IsNondegenerate} (ψ : Diffeomorph I I₂ M M₂ ↑⊤) (hψ : (SmoothForm.mpullback ⇑ψ ⋯) σ₂ = σ) : HasSymplecticTangentImages J hσ₂ (⇑ψ ∘ f) ↔ HasSymplecticTangentImages J hσ f

Transport by symplectomorphisms. If ψ pulls σ₂ back to σ, then ψ ∘ f has symplectic tangent images for σ₂ exactly when f has symplectic tangent images for σ.

Dimension and the symplectic complement

theorem TauCeti.SmoothTwoForm.IsNondegenerate.HasSymplecticTangentImages.even_finrank_range {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'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {f : N → M} [FiniteDimensional ℝ E'] (h : HasSymplecticTangentImages J hσ f) (x : N) : Even (Module.finrank ℝ ↥(↑(mfderiv% f x)).range)

A symplectic tangent image of a map from a finite-dimensional manifold has even dimension.

theorem TauCeti.SmoothTwoForm.IsNondegenerate.HasSymplecticTangentImages.even_finrank {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'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {f : N → M} [FiniteDimensional ℝ E'] (h : HasSymplecticTangentImages J hσ f) {x : N} (hx : Function.Injective ⇑(mfderiv% f x)) : Even (Module.finrank ℝ E')

A map with symplectic tangent images and an injective differential at some point comes from an even-dimensional manifold.

theorem TauCeti.SmoothTwoForm.IsNondegenerate.HasSymplecticTangentImages.isCompl {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'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {σ : SmoothTwoForm I M} {hσ : σ.IsNondegenerate} {f : N → M} [FiniteDimensional ℝ E] (h : HasSymplecticTangentImages J hσ f) (x : N) : IsCompl (↑(mfderiv% f x)).range ((hσ.symplecticFormAt (f x)).orthogonal (↑(mfderiv% f x)).range)

In a finite-dimensional manifold, each symplectic tangent image splits the ambient tangent space together with its symplectic complement, T_(f x) M = df_x(T_x N) ⊕ df_x(T_x N)^σ.

Linear maps of symplectic vector spaces

theorem TauCeti.SymplecticForm.hasSymplecticTangentImages_continuousLinearMap_iff {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W] (σ₀ : SymplecticForm W) (L : V →L[ℝ] W) : SmoothTwoForm.IsNondegenerate.HasSymplecticTangentImages (modelWithCornersSelf ℝ V) ⋯ ⇑L ↔ σ₀.IsSymplectic (↑L).range

In a finite-dimensional symplectic vector space with its constant symplectic form, a continuous linear map has symplectic tangent images exactly when its range is a symplectic subspace.

theorem TauCeti.SymplecticForm.hasSymplecticTangentImages_inl {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W] [FiniteDimensional ℝ V] (ω₁ : SymplecticForm V) (ω₂ : SymplecticForm W) : SmoothTwoForm.IsNondegenerate.HasSymplecticTangentImages (modelWithCornersSelf ℝ V) ⋯ ⇑(ContinuousLinearMap.inl ℝ V W)

The inclusion v ↦ (v, 0) of the first factor of a direct sum of finite-dimensional symplectic vector spaces has symplectic tangent images for the constant direct-sum form.