Collar charts on a manifold with boundary #
Boundary.Collar.Basic identifies the model half-space EuclideanHalfSpace (n + 1) with the
product EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1 of its boundary model and an inward normal
coordinate. That is a statement about the model; this file transports it to an arbitrary
manifold M modeled on that half-space, by composing an ambient chart of M with the
identification.
The resulting collar chart reads a point of M as a pair: a tangential coordinate in the
boundary model, and a normal coordinate in [0, ∞). Two facts make it deserve the name.
- The boundary is the zero slice. For an atlas chart
eand a point ofe.source, lying onI.boundary Mbecomes the vanishing of one product factor — the normal coordinate — of the collar chart ofe. - The tangential coordinate is the boundary chart. On boundary points the first component of
the collar chart induced by the preferred ambient chart is the preferred chart of the boundary
manifold built in
Boundary.Charts. The two files therefore describe one coordinate system, not two.
The chart is built from collarDiffeomorph at the top regularity ⊤. Since ⊤ is the top of
WithTop ℕ∞, ContMDiff.of_le le_top downcasts its smoothness to whatever exponent a caller
needs, so one chart serves every regularity.
Those coordinates are smooth, not merely continuous: contMDiffOn_collarChart and
contMDiffOn_collarChart_symm make a collar chart a C^k diffeomorphism between its source and
its target, for a chart in IsManifold.maximalAtlas. Read with
mem_boundary_iff_collarChart_snd_apply_zero_eq_zero, they give smooth local product
coordinates whose normal component cuts out the boundary. They do not give a collar: the target
of a collar chart is ⇑collarDiffeomorph ⁻¹' e.target, an open subset of the product model, and
shrinking it to a product neighbourhood V × [0, 1) is not proved here.
This serves the collar-neighbourhood target in Layer 1 of the GeometricTopology roadmap
(TauCetiRoadmap/GeometricTopology/README.md), after Boundary.Collar.Basic's standard-model
calculation. Boundary.Collar.Manifold uses the two smoothness lemmas above to prove that these
charts have C^k transitions. The remaining global statement is that a whole neighbourhood of
I.boundary M is diffeomorphic to
I.boundary M × [0, 1). The two textbook routes differ in what they need. Lee Thm 9.25 goes
through the Boundary Flowout Theorem, gluing an inward-pointing vector field and flowing it,
which needs flows from boundary points; Mathlib's integral curves are still restricted to
interior points, so that route waits on them. Hirsch Thm 6.1 instead glues local retractions
with a bump function and pairs the resulting retraction r with a g vanishing on the boundary
and regular there, taking h = (r, g); that route needs no flows. (Hirsch §5.2 gives the
differential-equations proof as an alternative.)
Main definitions #
TauCeti.collarChart: the collar chart induced by an ambient chart.TauCeti.collarChartedSpace:Mas a charted space over the product, composingEuclideanHalfSpace.collarModelChartedSpacewith the ambient atlas ofM. It is adef, not aninstance:Malready carries aChartedSpaceover the half-space, and the two must not compete in instance search.
Main results #
TauCeti.mem_boundary_iff_collarChart_snd_apply_zero_eq_zero: the boundary is the zero slice of the normal coordinate.TauCeti.collarChart_fst_eq_boundaryChartedSpace_chartAt_apply: on the boundary, the tangential coordinate is the preferred boundary chart ofBoundary.Charts.TauCeti.collarChart_apply,_targetand_symm_apply: the value, target and inverse of a collar chart, so it never has to be unfolded.TauCeti.collarChartedSpace_chartAtandTauCeti.collarChartedSpace_atlas: its preferred charts and its atlas.TauCeti.contMDiffOn_collarChartandTauCeti.contMDiffOn_collarChart_symm: a collar chart and its inverse areC^k, so the local product coordinates are smooth.
References #
- M. Hirsch, Differential Topology, Springer GTM 33 (1976), Theorem 6.1 (the collaring theorem).
- J. Lee, Introduction to Smooth Manifolds, Springer GTM 218, 2nd ed. (2013), Theorem 9.25 (the collar neighbourhood theorem).
The collar chart attached to an ambient chart e of M: read a point through e, then split
the model half-space into its boundary model and the inward normal coordinate.
collarDiffeomorph is taken at the top regularity ⊤ because ContMDiff.of_le le_top downcasts
its smoothness to any k, so this one chart serves every regularity. Its underlying map does not
depend on the exponent either, so the topological lemmas below are equally unaffected.
No body here or below is exposed: the lemmas in this section name the value, source, target and inverse of a collar chart, so downstream code rewrites with those instead of unfolding.
Instances For
Reading a point through a collar chart is reading it through the ambient chart and then applying the inverse collar identification.
Not @[simp]: it would rewrite the collar phrasing of the two main results back into ambient
coordinates via Boundary.Collar.Basic's simp lemmas, which is the normal-form clash the collar
statements exist to avoid. Use it explicitly, as collarChart_fst and collarChart_snd_apply_zero
do.
A collar chart sees exactly what the ambient chart it comes from sees.
A collar chart lands where the collar identification carries the ambient chart's target.
The inverse of a collar chart reassembles the pair and reads it back through the ambient chart.
The tangential coordinate of a collar chart deletes the zeroth ambient coordinate.
Not @[simp]: the collar phrasing is the user-facing normal form here, so this must not rewrite
collarChart_fst_eq_boundaryChartedSpace_chartAt_apply's left-hand side away.
The normal coordinate of a collar chart is the zeroth ambient coordinate.
Not @[simp], for the reason given at collarChart_fst.
A collar chart is C^k on its source. The collar identification is a diffeomorphism, so
splitting an ambient chart into a tangential and a normal coordinate costs no regularity.
The inverse of a collar chart is C^k on its target. With contMDiffOn_collarChart,
a collar chart of a maximalAtlas member is a C^k diffeomorphism between its source and its
target, so on that source M carries smooth tangential and normal coordinates. The target is an
open subset of the product model, not a product neighbourhood.
In collar coordinates the boundary is the zero slice of the normal coordinate. For an
atlas chart e and a point of e.source, the collar chart isolates the coordinate that
Boundary.Charts tests as a product factor, so the boundary condition is one equation in it.
On the boundary, the tangential coordinate of a collar chart is the boundary chart. The
collar coordinates of Boundary.Collar.Basic and the boundary manifold structure of
Boundary.Charts are the same coordinate system: the boundary chart is the restriction of the
collar chart's first component.
The collar charts present M as a charted space over the product of the boundary model and
the one-dimensional half-space.
It is ChartedSpace.comp applied to EuclideanHalfSpace.collarModelChartedSpace, rather than an
atlas written out by hand, so that chartAt_comp, the extChartAt composition lemmas and
HasGroupoid.comp all apply to it. Its C^k manifold structure is proved in
Boundary.Collar.Manifold.
n and M are explicit so that letI := collarChartedSpace n M determines both; there is no
expected type at a letI to solve them from.
Deliberately not an instance: M already carries a ChartedSpace over
EuclideanHalfSpace (n + 1), and letting a second one be found by instance search would make
every statement about charts of M ambiguous.
Instances For
The preferred chart of collarChartedSpace is the collar chart of the preferred ambient
chart. Consumers should rewrite with this rather than unfold the definition.
The atlas of collarChartedSpace is the collar chart of every ambient chart.