Liouville domains #
A Liouville domain is a compact exact symplectic manifold with boundary whose Liouville vector
field points outwards along the boundary. Here it is a compact domain W with smooth boundary
in the interior of an ambient manifold M, carrying a nondegenerate two-form ω and a primitive
α, dα = ω (TauCeti.IsLiouvilleDomain):
- the smooth vector field
Zwithι_Z ω = α, the Liouville field ofα, exists; W = {f ≤ c}for a continuous functionf, smooth at the points of the levelf⁻¹(c), withdf(Z) > 0along that level.
The last condition says that Z points strictly outwards along f⁻¹(c), and makes c a regular
value of f. So f⁻¹(c) is a smooth hypersurface, and it is the boundary of W: on a manifold
without boundary, the frontier of W is exactly the level
(TauCeti.frontier_setOf_le_eq_of_mvfderiv_pos). The primitive is part of the data, as for
hypersurfaces of contact type, and the ambient form ω is then symplectic
(TauCeti.IsLiouvilleDomain.isSymplectic). Since ω is smooth and closed, the Liouville field
of α is a Liouville vector field of ω, L_Z ω = ω
(TauCeti.IsLiouvilleDomain.isLiouvilleVectorField, from
TauCeti.isLiouvilleVectorField_mextDeriv_of_interior_eq).
The boundary of a Liouville domain, with the atlas of a regular level, is a hypersurface of
restricted contact type with primitive α
(TauCeti.IsLiouvilleDomain.exists_isRestrictedContactType). The basic example is the unit
codisc bundle of a compact Riemannian manifold, with the canonical symplectic form and the
primitive -λ of the cotangent bundle
(TauCeti.CotangentBundle.isLiouvilleDomain_codiscBundle).
Main definitions #
TauCeti.IsLiouvilleDomain: a compact domain whose boundary is crossed outwards by the Liouville field of an explicit primitive of a nondegenerate form.
Main results #
TauCeti.IsLiouvilleDomain.isSymplectic: the ambient form is symplectic.TauCeti.IsLiouvilleDomain.isLiouvilleVectorField: the Liouville field ofαis a Liouville vector field ofω.TauCeti.IsLiouvilleDomain.exists_sublevel_of_interior_eq: every vector fieldZwithι_Z ω = αpoints strictly out of a Liouville domain along its boundary.TauCeti.IsLiouvilleDomain.exists_isRestrictedContactType: the boundary is a regular level of a defining function, and is of restricted contact type.
References #
- K. Cieliebak, Y. Eliashberg, From Stein to Weinstein and Back, AMS Colloquium Publications 59, 2012, Section 11.1 (Liouville domains).
- P. Seidel, A biased view of symplectic cohomology, Current Developments in Mathematics 2006, Section 3 (Liouville domains and their completions).
- J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Floer homology with DG coefficients. Applications to cotangent bundles, arXiv:2404.07953, §1.2.
A subset W of a manifold M is a Liouville domain for the smooth two-form ω, with
primitive α, when ω is nondegenerate, dα = ω, W is compact and lies in the interior of
M, and the Liouville field of α points strictly outwards along the boundary of W: some smooth
vector field Z with ι_Z ω = α and some continuous function f and value c satisfy
W = {f ≤ c}, with f smooth and df(Z) > 0 at every point of the level f⁻¹(c). The
nondegeneracy of ω makes Z unique, and the condition along f⁻¹(c) makes c a regular value
of f, so that W is a compact domain with smooth boundary f⁻¹(c).
- isNondegenerate : ω.IsNondegenerate
The two-form of a Liouville domain is nondegenerate.
The one-form of a Liouville domain is a primitive of its two-form.
- isCompact : IsCompact W
A Liouville domain is compact.
- subset_interior : W ⊆ ModelWithCorners.interior M
A Liouville domain lies in the interior of the ambient manifold.
- exists_liouville_outward : ∃ (Z : (x : M) → TangentSpace I x), (ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) ∧ RoughForm.interior Z ↑ω = ↑α ∧ ∃ (f : M → ℝ) (c : ℝ), Continuous f ∧ W = {x : M | f x ≤ c} ∧ ∀ (x : M), f x = c → ContMDiffAt I (modelWithCornersSelf ℝ ℝ) (↑⊤) f x ∧ 0 < (d% f x) (Z x)
The Liouville field of the primitive points strictly outwards along the boundary, the level
f⁻¹(c)of a continuous functionfwithW = {f ≤ c}that is smooth along the level.
Instances For
The ambient form of a Liouville domain is symplectic: it is nondegenerate by definition, and closed because it is exact.
A Liouville domain is closed, as a sublevel set of a continuous function.
The Liouville field of a Liouville domain is smooth: the vector field Z with
ι_Z ω = α, unique since ω is nondegenerate, is a smooth section of the tangent bundle.
The Liouville field of a Liouville domain is a Liouville vector field of the ambient form,
L_Z ω = ω: the form is exact, ω = dα, and ι_Z dα = α.
The Liouville field points out of a Liouville domain. If ι_Z ω = α, then W = {f ≤ c}
for a continuous function f, smooth along the level f⁻¹(c), with df(Z) > 0 there.
The boundary of a Liouville domain is of restricted contact type. On a finite-dimensional
manifold without boundary, a Liouville domain W is the sublevel set {f ≤ c} of a function f,
C¹ along the level f⁻¹(c), of which c is a regular value; the frontier of W is exactly the
level; and the level, with its atlas TauCeti.regularLevelChartedSpace, is a hypersurface
of restricted contact type for the primitive α.