Regular fibres of manifold-valued maps

A regular fibre over an interior value of a C^m map, m ≥ 1, from a finite-dimensional boundaryless real manifold to a finite-dimensional real manifold is an embedded submanifold of the expected dimension. The carrier is the actual subtype {x // f x = c}, with its subspace topology; neither manifold needs to be Hausdorff, and the fibre may be empty.

TauCeti.regularFiberChartedSpace constructs an atlas using the preferred extended target chart. TauCeti.RegularFiber.chartedSpaceOfChart allows any target chart containing the value. TauCeti.isManifold_regularFiber, TauCeti.isSmoothEmbedding_coe_regularFiber, and TauCeti.range_mfderiv_coe_regularFiber give its manifold, embedding, and tangent-kernel properties. TauCeti.exists_regularFiber_smoothEmbedding packages these properties existentially. The smooth universal property follows from Mathlib's ContMDiff.iff_comp_isImmersion and continuity into a subtype. No global charted-space instance is installed on a fibre or on its ambient manifold.

The construction uses one extended target chart at c. Its open preimage contains the entire fibre, and the regular level of the coordinate map there is homeomorphic to the original fibre. The atlas is transported from TauCeti.regularLevelChartedSpace; no gluing of local fibre atlases is needed.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer, 2013, Corollary 5.14 and Proposition 5.38 (regular level sets and their tangent spaces).

@[instance_reducible]

noncomputable def TauCeti.RegularFiber.chartedSpaceOfChart {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} {G : Type u_5} {N : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace G] {J : ModelWithCorners ℝ F G} [TopologicalSpace N] [ChartedSpace G N] {f : M → N} {c : N} {m : WithTop ℕ∞} [I.Boundaryless] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (hm : 1 ≤ m) (hf : ContMDiff I J m f) (φ : PartialDiffeomorph J (modelWithCornersSelf ℝ F) N F m) (hc : c ∈ φ.source) (hreg : IsRegularValue I J f c) : ChartedSpace (Fin (Module.finrank ℝ E - Module.finrank ℝ F) → ℝ) { x : M // f x = c }

The atlas of a regular fibre transported from its coordinate level in a target chart φ containing the value c. The fibre retains its subspace topology, and no global instance is installed.

theorem TauCeti.RegularFiber.isManifold_of_chart {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} {G : Type u_5} {N : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace G] {J : ModelWithCorners ℝ F G} [TopologicalSpace N] [ChartedSpace G N] {f : M → N} {c : N} {m : WithTop ℕ∞} [I.Boundaryless] [IsManifold I m M] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (hm : 1 ≤ m) (hf : ContMDiff I J m f) (φ : PartialDiffeomorph J (modelWithCornersSelf ℝ F) N F m) (hc : c ∈ φ.source) (hreg : IsRegularValue I J f c) : IsManifold (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ E - Module.finrank ℝ F) → ℝ)) m { x : M // f x = c }

A regular fibre with the atlas constructed in any target chart containing its value is a C^m manifold.

theorem TauCeti.RegularFiber.isSmoothEmbedding_coe_of_chart {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} {G : Type u_5} {N : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace G] {J : ModelWithCorners ℝ F G} [TopologicalSpace N] [ChartedSpace G N] {f : M → N} {c : N} {m : WithTop ℕ∞} [I.Boundaryless] [IsManifold I m M] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (hm : 1 ≤ m) (hf : ContMDiff I J m f) (φ : PartialDiffeomorph J (modelWithCornersSelf ℝ F) N F m) (hc : c ∈ φ.source) (hreg : IsRegularValue I J f c) : Manifold.IsSmoothEmbedding (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ E - Module.finrank ℝ F) → ℝ)) I m Subtype.val

The inclusion of a regular fibre is a C^m smooth embedding for the atlas constructed in any target chart containing its value.

@[instance_reducible]

noncomputable def TauCeti.regularFiberChartedSpace {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} {G : Type u_5} {N : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {m : WithTop ℕ∞} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace G] {J : ModelWithCorners ℝ F G} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J m N] {f : M → N} {c : N} (hm : 1 ≤ m) (hf : ContMDiff I J m f) (hc : J.IsInteriorPoint c) (hreg : IsRegularValue I J f c) : ChartedSpace (Fin (Module.finrank ℝ E - Module.finrank ℝ F) → ℝ) { x : M // f x = c }

The atlas on a regular fibre of a C^m map, m ≥ 1, over an interior value c, transported from the regular level in the preferred extended target chart at c. It uses the subspace topology and is not a global instance.

theorem TauCeti.regularFiberChartedSpace_eq_chartedSpaceOfChart {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} {G : Type u_5} {N : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {m : WithTop ℕ∞} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace G] {J : ModelWithCorners ℝ F G} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J m N] {f : M → N} {c : N} (hm : 1 ≤ m) (hf : ContMDiff I J m f) (hc : J.IsInteriorPoint c) (hreg : IsRegularValue I J f c) : regularFiberChartedSpace hm hf hc hreg = RegularFiber.chartedSpaceOfChart hm hf (extChartPartialDiffeomorph J m c) ⋯ hreg

The preferred regular-fibre atlas uses the extended target chart at the value. This equation allows comparisons with atlases constructed in other target charts without unfolding the atlas.

theorem TauCeti.isManifold_regularFiber {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} {G : Type u_5} {N : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {m : WithTop ℕ∞} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I m M] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace G] {J : ModelWithCorners ℝ F G} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J m N] {f : M → N} {c : N} (hm : 1 ≤ m) (hf : ContMDiff I J m f) (hc : J.IsInteriorPoint c) (hreg : IsRegularValue I J f c) : IsManifold (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ E - Module.finrank ℝ F) → ℝ)) m { x : M // f x = c }

The regular fibre over an interior value with its preferred atlas is a C^m manifold.

theorem TauCeti.isSmoothEmbedding_coe_regularFiber {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} {G : Type u_5} {N : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {m : WithTop ℕ∞} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I m M] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace G] {J : ModelWithCorners ℝ F G} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J m N] {f : M → N} {c : N} (hm : 1 ≤ m) (hf : ContMDiff I J m f) (hc : J.IsInteriorPoint c) (hreg : IsRegularValue I J f c) : Manifold.IsSmoothEmbedding (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ E - Module.finrank ℝ F) → ℝ)) I m Subtype.val

The inclusion of the regular fibre over an interior value with its preferred atlas is a C^m smooth embedding.

theorem TauCeti.range_mfderiv_coe_regularFiber {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} {G : Type u_5} {N : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {m : WithTop ℕ∞} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I m M] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace G] {J : ModelWithCorners ℝ F G} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J m N] {f : M → N} {c : N} (hm : 1 ≤ m) (hf : ContMDiff I J m f) (hc : J.IsInteriorPoint c) (hreg : IsRegularValue I J f c) (z : { x : M // f x = c }) : (↑(mfderiv% Subtype.val z)).range = (↑(mfderiv% f ↑z)).ker

The tangent image of the regular-fibre inclusion is the kernel of the ambient differential.

theorem TauCeti.exists_regularFiber_smoothEmbedding {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} {G : Type u_5} {N : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {m : WithTop ℕ∞} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I m M] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace G] {J : ModelWithCorners ℝ F G} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J m N] {f : M → N} {c : N} (hm : 1 ≤ m) (hf : ContMDiff I J m f) (hc : J.IsInteriorPoint c) (hreg : IsRegularValue I J f c) : ∃ (a : ChartedSpace (Fin (Module.finrank ℝ E - Module.finrank ℝ F) → ℝ) { x : M // f x = c }), IsManifold (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ E - Module.finrank ℝ F) → ℝ)) m { x : M // f x = c } ∧ Manifold.IsSmoothEmbedding (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ E - Module.finrank ℝ F) → ℝ)) I m Subtype.val ∧ ∀ (z : { x : M // f x = c }), (↑(mfderiv% Subtype.val z)).range = (↑(mfderiv% f ↑z)).ker

The regular-fibre theorem. A regular fibre over an interior value of a C^m map, m ≥ 1, from a finite-dimensional boundaryless real manifold to a finite-dimensional real manifold admits a C^m manifold structure of dimension dim M - dim N, with its subspace topology, for which the inclusion is a C^m smooth embedding and has tangent image ker df. No separation or countability assumptions are needed, and an empty fibre is allowed.