Orthogonal maps of the Euclidean disk #
A linear isometry g of ℝⁿ maps the closed unit disk TopCat.disk n onto itself and its
boundary sphere TopCat.diskBoundary n onto itself. This file bundles these restrictions as
LinearIsometryEquiv.diskMap g and LinearIsometryEquiv.diskBoundaryMap g. The disk map is a map
of pairs (D^n, ∂D^n) → (D^n, ∂D^n), and on the boundary sphere it is the boundary map.
When g preserves orientation, that is det g = 1, it is joined to the identity in the special
orthogonal group, so the disk map is homotopic to the identity through maps of pairs
(TauCeti.TopCat.exists_homotopy_diskMap_id_of_det_eq_one). Its boundary map is homotopic to the
identity of the sphere, and the composite of a map of pairs out of the disk with it is homotopic
to that map, keeping the boundary sphere where the map sends it
(TauCeti.TopCat.exists_homotopy_diskMap_comp_of_det_eq_one). This is how an orthogonal change
of parametrization of an attached cell is removed up to homotopy: the comparison of two Morse
charts at a critical point of index λ changes the characteristic map of the cell by the polar
factor of the transition, an orthogonal map of ℝ^λ.
In dimension 1 there are only two orthogonal maps. If det g = 1 then g is the identity, so
its disk map is the identity (TauCeti.TopCat.diskMap_eq_id_of_det_eq_one); if det g = -1 then
g = -1, and its boundary map swaps the two points of the sphere ∂D¹ = {-1, 1}
(TauCeti.TopCat.diskBoundaryMap_eq_diskBoundaryNeg_of_det_eq_neg_one).
Main declarations #
LinearIsometryEquiv.diskMap,LinearIsometryEquiv.diskBoundaryMap: the maps of the disk and of its boundary sphere induced by a linear isometry ofℝⁿ; the boundary map of-1is the antipodal mapTauCeti.diskBoundaryNeg(LinearIsometryEquiv.diskBoundaryMap_neg).TauCeti.TopCat.exists_homotopy_diskMap_id_of_det_eq_one: fordet g = 1, the disk map is homotopic to the identity through maps of pairs.TauCeti.TopCat.homotopic_diskBoundaryMap_id_of_det_eq_one: fordet g = 1, the boundary map is homotopic to the identity.TauCeti.TopCat.exists_homotopy_diskMap_comp_of_det_eq_one: fordet g = 1, precomposing a map of pairs with the disk map does not change its homotopy class as a map of pairs.TauCeti.TopCat.diskMap_eq_id_of_det_eq_one,TauCeti.TopCat.diskBoundaryMap_eq_diskBoundaryNeg_of_det_eq_neg_one: the two orthogonal maps ofD¹.
References #
- J. Milnor, Morse Theory, Annals of Mathematics Studies 51, Princeton University Press, 1963, Remark 3.3.
The self-map w ↦ g w of the disk TopCat.disk n induced by a linear isometry g of ℝⁿ.
Instances For
The self-map s ↦ g s of the boundary sphere TopCat.diskBoundary n induced by a linear
isometry g of ℝⁿ.
Instances For
On the boundary sphere, the disk map of g is the boundary map of g.
On the boundary sphere, the disk map of g is the boundary map of g.
The pointwise form of LinearIsometryEquiv.diskBoundaryMap_comp_diskBoundaryInclusion.
The disk map of g is a map of pairs (D^n, ∂D^n) → (D^n, ∂D^n).
The boundary map of -1 is the antipodal map of the sphere.
An orientation-preserving orthogonal map of a disk is homotopic to the identity through maps
of pairs. If det g = 1, there is a homotopy from the disk map of g to the identity of
TopCat.disk n which keeps the boundary sphere in itself at all times. The homotopy is
(t, w) ↦ γ t w for a path γ from g to the identity in the special orthogonal group.
An orientation-preserving orthogonal map of a sphere is homotopic to the identity. If
det g = 1, the boundary map of g is homotopic to the identity of TopCat.diskBoundary n.
Precomposing with an orientation-preserving orthogonal map does not change a map of pairs
up to homotopy. If det g = 1 and χ : D^n → X sends the boundary sphere into S, then the
composite of the disk map of g with χ is homotopic to χ by a homotopy which keeps the
boundary sphere in S at all times.
An orientation-preserving orthogonal map of D¹ is the identity.
An orientation-reversing orthogonal map of D¹ swaps the two boundary points. If
det e = -1, the boundary map of e is the antipodal map of the sphere ∂D¹ = {-1, 1}.