Nondegenerate, tame, and compatible two-forms on manifolds #
This file supplies the fiberwise part of a symplectic structure on a smooth manifold. A smooth
two-form is nondegenerate when its value on every tangent space is a nondegenerate alternating
bilinear form. Such a value is therefore a TauCeti.SymplecticForm, so the pointwise linear theory
can be reused without restating it.
Tameness and compatibility with a smooth almost complex structure are kept as unbundled
predicates. They are pointwise exactly SymplecticForm.Tames and SymplecticForm.Compatible.
In particular, tameness already forces fiberwise nondegeneracy. The constant construction shows
that every finite-dimensional symplectic vector space, and especially the standard doubled model,
gives a non-vacuous manifold-level example.
Closedness is the separate predicate TauCeti.SmoothForm.IsClosed of
TauCeti/Geometry/Manifold/DifferentialForm/Closed.lean, defined through the exterior derivative
of the coordinate expressions of the form. A symplectic form on a manifold is a smooth two-form
which
is both closed and fiberwise nondegenerate; TauCeti.SmoothTwoForm.IsSymplectic bundles the two
conditions, and a constant symplectic form on a finite-dimensional vector space is the basic
example.
Main declarations #
TauCeti.SmoothTwoForm.IsNondegenerate: fiberwise nondegeneracy of a smooth two-form.TauCeti.SmoothTwoForm.IsSymplectic: a closed, fiberwise nondegenerate smooth two-form.TauCeti.SmoothTwoForm.IsNondegenerate.symplecticFormAt: the symplectic form on a tangent fiber.TauCeti.SmoothTwoForm.inChartAt_extChartAt_self_nondegenerate: nondegeneracy at a point passes to the coordinate expression in the preferred chart at that point.TauCeti.SmoothTwoForm.IsNondegenerate.symplecticFormAt_transport: transport of tangent-fiber symplectic forms by the differential of a symplectomorphism.TauCeti.SmoothTwoForm.IsNondegenerate.isNondegenerate_mpullback_of_isLocalDiffeomorph: a local diffeomorphism pulls a nondegenerate form back to a nondegenerate form.IsLocalDiffeomorph.isNondegenerate_mpullback_iff: for a surjective local diffeomorphism the converse holds as well.IsLocalDiffeomorph.isSymplectic_mpullback_iff: a surjective local diffeomorphism pulls a two-form back to a symplectic form exactly when the form is symplectic.TauCeti.SmoothTwoForm.isNondegenerate_iff_forall_ker_bilinFormAt_mpullback: nondegeneracy characterized by pullback kernels along a surjective smooth map with surjective derivatives.TauCeti.SmoothTwoForm.isSymplectic_iff_of_mpullback_eq: a form on the base of such a map is symplectic exactly when its pullback is closed and has kernel equal to the derivative’s kernel.TauCeti.SmoothTwoForm.TamesandTauCeti.SmoothTwoForm.Compatible: the unbundled pointwise relations to a smooth almost complex structure.TauCeti.SmoothTwoForm.IsNondegenerate.tames_iff,invariant_iff, andcompatible_iff: these relations characterized fiber by fiber through the linear theory.TauCeti.SymplecticForm.constSmooth: a symplectic form as a constant smooth two-form, which is symplectic (TauCeti.SymplecticForm.isSymplectic_constSmooth), together with itsmvfderivand partial-diffeomorphism pullback characterizations (TauCeti.SymplecticForm.eval₂_constSmooth_mfderiv_eq,TauCeti.SmoothTwoForm.mpullback_constSmooth_eq_mpullback_subtype_val_iff).
The definitions follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.2.
A smooth two-form is fiberwise nondegenerate when its algebraic bilinear form on every tangent space is nondegenerate. Closedness is a separate condition.
Instances For
Fiberwise nondegeneracy in terms of vectors annihilating every vector on the right. For an alternating form this one-sided condition implies the corresponding condition on the other side.
Fiberwise nondegeneracy says that the null space {v | ∀ w, form x v w = 0} of the form is
zero at every point.
On a manifold of positive dimension, a fiberwise nondegenerate smooth two-form vanishes nowhere.
The negative of a fiberwise nondegenerate smooth two-form is fiberwise nondegenerate.
A smooth two-form is symplectic when it is closed and fiberwise nondegenerate. This is the manifold-level notion of a symplectic form; a symplectic manifold is a manifold carrying one.
- isClosed : SmoothForm.IsClosed form
A symplectic form is closed.
- isNondegenerate : form.IsNondegenerate
A symplectic form is fiberwise nondegenerate.
Instances For
A fiberwise nondegenerate smooth two-form gives a symplectic form on each tangent space.
Instances For
The tangent-space symplectic form evaluates as the original smooth two-form.
A fiberwise nondegenerate two-form is nondegenerate on the tangent space at each point.
A two-form nondegenerate at x has a nondegenerate coordinate expression in the preferred
chart at x, at the chart point of x.
The bilinear form underlying the tangent-space symplectic form is the value of the two-form.
At every point, the differential of a diffeomorphism pulling σ₂ back to σ transports the
tangent-space symplectic form of σ to that of σ₂.
A local diffeomorphism, such as a diffeomorphism, pulls a nondegenerate form back to a nondegenerate form.
A surjective local diffeomorphism, such as the projection of a covering space, pulls a two-form back to a nondegenerate form exactly when the form is nondegenerate.
A surjective local diffeomorphism, such as the projection of a covering space, pulls a two-form back to a symplectic form exactly when the form is symplectic.
For a surjective p with surjective derivatives, η is nondegenerate exactly when, at every
point z, the null space of the pullback p^* η is the kernel of the derivative of p.
Symplectic forms through a smooth surjection. If p is a surjective smooth map with
surjective derivatives and p^* η = σ, then η is symplectic exactly when σ is closed and its
null space at every point is the kernel of the derivative of p.
A smooth two-form tames a smooth almost complex structure when
form_x(v, J_x v) > 0 for every nonzero tangent vector.
Instances For
Tameness is positivity on each nonzero tangent vector and its complex rotation.
Manifold-level tameness is the pointwise linear tameness condition once nondegeneracy has
identified each tangent-space form as a SymplecticForm.
A tame smooth two-form is fiberwise nondegenerate.
A smooth two-form is invariant under a smooth almost complex structure when applying the structure in both tangent arguments leaves the form unchanged.
Instances For
Invariance is preservation of the form on each tangent fibre.
Apply invariance at a point and two tangent vectors.
Manifold-level invariance is the pointwise linear invariance condition once nondegeneracy has
identified each tangent-space form as a SymplecticForm.
Compatibility is the conjunction of invariance and tameness. Neither relation is stored in the smooth two-form or almost complex structure.
- invariant : form.Invariant J
Applying the almost complex structure in both entries preserves the two-form.
- tames : form.Tames J
The two-form is positive on every complex line.
Instances For
Compatibility implies fiberwise nondegeneracy.
Manifold-level compatibility is compatibility of the induced linear pair on every tangent space.
Manifold-level compatibility gives the existing compatible-pair structure on each tangent space.
A symplectic form on a finite-dimensional normed vector space, regarded as a constant smooth two-form on the corresponding model manifold.
Instances For
A constant smooth symplectic form evaluates as its defining algebraic form.
Under the canonical identification of a self-model tangent fiber with the model space, evaluating a constant smooth symplectic form is evaluating its defining bilinear form.
Evaluating the constant smooth two-form omegaForm.constSmooth on mfderiv of a model-valued
map agrees with evaluating omegaForm directly on mvfderiv.
A constant smooth symplectic form is fiberwise nondegenerate.
On every tangent fiber, the symplectic form of a constant smooth symplectic form is the defining algebraic form.
A constant smooth symplectic form is closed.
A symplectic vector space is a symplectic manifold: a constant smooth symplectic form is symplectic.
Tameness of a pair of constant smooth structures is exactly tameness of the underlying linear pair.
Invariance of a pair of constant smooth structures is exactly invariance of the underlying linear pair.
Compatibility of a pair of constant smooth structures is exactly compatibility of the underlying linear pair.
A partial diffeomorphism chart : M → F pulls the constant smooth form form₀.constSmooth
back to the restriction of form on the open submanifold chart.source if and only if form
agrees pointwise on chart.source with form₀ pulled back by mvfderiv I chart.