Morse functions under boundaryless model transport

Passing from an arbitrary boundaryless model to its vector-space-valued atlas preserves critical points, nondegenerate critical points, the Morse index, and the Morse property on any subset. These comparisons use the identical extended charts, not a new choice of Morse coordinates. Thus self-modelled local constructions can be applied without changing the critical-point data.

@[simp]

theorem TauCeti.BoundarylessModel.criticalPoints_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] (f : M → ℝ) : criticalPoints (modelWithCornersSelf ℝ E) (f ∘ ⇑(homeomorph I M).symm) = ⇑(homeomorph I M).symm ⁻¹' criticalPoints I f

Critical points are unchanged by the boundaryless model transport.

@[simp]

theorem TauCeti.BoundarylessModel.isManifoldNondegenerateCriticalPoint_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] (f : M → ℝ) (x : BoundarylessModel I M) : IsManifoldNondegenerateCriticalPoint (modelWithCornersSelf ℝ E) (f ∘ ⇑(homeomorph I M).symm) x ↔ IsManifoldNondegenerateCriticalPoint I f ((homeomorph I M).symm x)

Nondegenerate critical points are unchanged by the boundaryless model transport.

@[simp]

theorem TauCeti.BoundarylessModel.manifoldMorseIndex_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] (f : M → ℝ) (x : BoundarylessModel I M) : manifoldMorseIndex (modelWithCornersSelf ℝ E) (f ∘ ⇑(homeomorph I M).symm) x = manifoldMorseIndex I f ((homeomorph I M).symm x)

The Morse index is unchanged, since the extended coordinate expression is identical.

@[simp]

theorem TauCeti.BoundarylessModel.isMorseOn_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] (f : M → ℝ) (s : Set M) : IsMorseOn (modelWithCornersSelf ℝ E) (f ∘ ⇑(homeomorph I M).symm) (⇑(homeomorph I M).symm ⁻¹' s) ↔ IsMorseOn I f s

Being Morse on a subset is preserved, including the smoothness requirement.

@[simp]

theorem TauCeti.BoundarylessModel.isMorse_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] (f : M → ℝ) : IsMorse (modelWithCornersSelf ℝ E) (f ∘ ⇑(homeomorph I M).symm) ↔ IsMorse I f

Global Morse functions are unchanged by replacing a boundaryless model by its vector space.