The closed unit ball as an analytic manifold with boundary #
The closed unit ball Dⁿ = closedBall (0 : E) 1 of an n-dimensional real inner product space
E is an analytic manifold with boundary, modelled on the half-space EuclideanHalfSpace n, and
its manifold boundary is the unit sphere. This is the disc that handles Dᵏ × Dⁿ⁻ᵏ are built
from, that ball embeddings and connected sums use, and whose diffeomorphisms fixing the boundary
form the group Diff(Dⁿ, ∂).
Charts #
Write e₀ for the first standard basis vector of EuclideanSpace ℝ (Fin n). The inversion in
the sphere of radius √2 centred at -e₀ passes the unit sphere through its centre, so it maps
the unit sphere minus -e₀ onto the hyperplane {y | y 0 = 0} and the closed unit ball minus
-e₀ onto the closed half-space {y | 0 ≤ y 0}. Precomposing with a linear isometry
φ : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) gives the chart TauCeti.closedBallChart φ, defined
on the ball minus φ.symm (-e₀), whose target is the whole half-space. The atlas consists of
these charts for all φ. Every transition map is a composite of two inversions and a linear
isometry, hence analytic, so the ball is an analytic manifold.
Main declarations #
TauCeti.closedBallChart φ: the chart attached to a linear isometryφ.TauCeti.instChartedSpaceClosedBall,TauCeti.instIsManifoldClosedBall: the closed unit ball of ann-dimensional real inner product space is an analytic manifold modelled onEuclideanHalfSpace n.TauCeti.boundary_closedBall: its manifold boundary is the unit sphere.TauCeti.isInteriorPoint_closedBall_iff: its interior points are those of norm less than1.TauCeti.isOrientedAtlas_closedBall: in dimension at least two, the charts attached to the isometriesφof one orientation class forming an oriented atlas.TauCeti.contMDiff_subtypeVal_closedBall: the inclusion intoEis analytic.TauCeti.contMDiffWithinAt_iff_comp_subtypeVal_closedBalland its pointwise, setwise and global versions: a map into the ball isC^kexactly when it isC^kas a map intoE.LinearIsometry.isSmoothEmbedding_unitClosedBallMap: a linear isometryF →ₗᵢ[ℝ] Erestricts to a smooth embedding of closed unit balls, in the sense of manifolds with boundary. In chartsclosedBallChart φandclosedBallChart ψwithψ ∘ ι ∘ φ⁻¹fixinge₀, the inversions cancel and the map reads as that linear isometry of the model spaces, which is the inclusion of a factor of a product decomposition (LinearIsometry.prodOrthogonalRangeEquiv). This is the flat discD² ⊆ D⁴bounded by a great circle, the slice disc of the unknot.LinearIsometryEquiv.unitClosedBallDiffeomorph: a linear isometry equivalence restricts to a diffeomorphism of closed unit balls.Diffeomorph.restrictUnitClosedBall: a diffeomorphism ofEmapping the closed unit ball onto itself restricts to a diffeomorphism of the closed unit ball.
References #
- M. W. Hirsch, Differential Topology, Graduate Texts in Mathematics 33, Springer, 1976, Chapter 1, §4 (manifolds with boundary).
The inversion onto the half-space #
The charts #
The chart of the closed unit ball attached to a linear isometry
φ : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n): transport along φ, then invert in the sphere of radius
√2 centred at -e₀. It is defined on the ball minus φ.symm (-e₀), maps the unit sphere into
the boundary hyperplane {y | y 0 = 0}, and its target is the whole half-space.
Instances For
The chart attached to φ is defined away from φ.symm (-e₀).
The chart attached to φ maps onto the whole half-space.
The chart attached to φ inverts the image of a point under φ and reads the result in the
half-space; off the source the result is clamped into the half-space by the model.
On its source, the chart reads a point as the inversion of its image under φ.
The inverse of the chart attached to φ inverts a point of the half-space and transports it
back along φ.
The manifold structure #
The closed unit ball of an n-dimensional real inner product space is a charted space
modelled on EuclideanHalfSpace n, with the charts closedBallChart φ for all linear isometries
φ : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n). Use atlas_closedBall and
exists_chartAt_closedBall_eq to reason about the charts.
The atlas of the closed ball consists of the charts closedBallChart φ.
The preferred chart of the closed ball at x is closedBallChart φ for an isometry φ not
sending x to -e₀.
The closed unit ball of an n-dimensional real inner product space is an analytic manifold
with boundary.
The boundary is the unit sphere #
A point of the closed unit ball is a boundary point exactly when it has norm 1.
A point of the closed unit ball is an interior point exactly when it has norm less than 1.
The manifold boundary of the closed unit ball is the unit sphere.
Smooth maps to and from the closed ball #
The inclusion of the closed unit ball into E is analytic.
Orientability #
In dimension at least two, the closed-ball charts in a fixed orientation class form an oriented atlas. Their transitions are two inversions with a positive-determinant isometry.
The closed unit ball of EuclideanSpace ℝ (Fin n) #
The closed unit ball of EuclideanSpace ℝ (Fin n) is a charted space modelled on
EuclideanHalfSpace n.
The closed unit ball of EuclideanSpace ℝ (Fin n) is an analytic manifold with boundary.
A map into the closed unit ball is C^k within a set at a point exactly when its
composition with the inclusion into E is. The point need not belong to the set.
A map into the closed unit ball is C^k at a point exactly when its composition with
the inclusion into E is.
A map into the closed unit ball is C^k on a set exactly when its composition with
the inclusion into E is.
A map into the closed unit ball is C^k exactly when it is C^k as a map into E.
Diffeomorphisms of the ambient space preserving the closed ball #
A C^k diffeomorphism of E which maps the closed unit ball onto itself restricts to a C^k
diffeomorphism of the closed unit ball, in the sense of manifolds with boundary.
Instances For
Smooth embeddings of closed balls induced by linear isometries #
The restriction of a linear isometry to the closed unit balls is an immersion at every point, in the sense of manifolds with boundary: in suitable inversion charts it reads as a linear isometry of the model spaces, hence as the inclusion of a factor of a product decomposition.
The restriction of a linear isometry to the closed unit balls is a C^k immersion.
The restriction of a linear isometry to the closed unit balls is a C^k smooth embedding of
manifolds with boundary.
A linear isometry equivalence restricts to a C^k diffeomorphism of closed unit balls, in the
sense of manifolds with boundary.
Instances For
The closed complex unit disk uses its existing half-space atlas without a local dimension instance at each consumer.
The existing complex unit disk atlas is analytic.