English
If a map f: M → E is C^m and its values lie in the unit sphere, then the restriction f → sphere is a C^m map to the sphere.
Русский
Если отображение f: M → E имеет класс C^m и значения лежат на единичной сфере, то ограничение f до сферы является отображением класса C^m на сферу.
LaTeX
$$If $f:M\\to E$ is ContMDiff and $\\forall x\\, f(x)\\in \\mathsf{sphere}(0,E,1)$, then $\\mathrm{Set.codRestrict}\, f\\big(\\mathsf{sphere}(0:E)1\\big) : M\\to \\mathsf{sphere}(0:E)1$ is ContMDiff of class $n$.$$
Lean4
/-- If a `C^m` function `f : M → E`, where `M` is some manifold, takes values in the
sphere, then it restricts to a `C^m` function from `M` to the sphere. -/
theorem codRestrict_sphere {n : ℕ} [Fact (finrank ℝ E = n + 1)] {f : M → E} (hf : ContMDiff I 𝓘(ℝ, E) m f)
(hf' : ∀ x, f x ∈ sphere (0 : E) 1) : ContMDiff I (𝓡 n) m (Set.codRestrict _ _ hf' : M → sphere (0 : E) 1) :=
by
rw [contMDiff_iff_target]
refine ⟨continuous_induced_rng.2 hf.continuous, ?_⟩
intro v
let U : _ ≃ₗᵢ[ℝ] _ := (OrthonormalBasis.fromOrthogonalSpanSingleton n (ne_zero_of_mem_unit_sphere (-v))).repr
have h : ContDiffOn ℝ ω _ Set.univ := U.contDiff.contDiffOn
have H₁ := (h.comp_inter contDiffOn_stereoToFun).contMDiffOn
have H₂ : ContMDiffOn _ _ _ _ Set.univ := hf.contMDiffOn
convert (H₁.of_le le_top).comp' H₂ using 1
ext x
have hfxv : f x = -↑v ↔ ⟪f x, -↑v⟫_ℝ = 1 :=
by
have hfx : ‖f x‖ = 1 := by simpa using hf' x
rw [inner_eq_one_iff_of_norm_one hfx]
exact norm_eq_of_mem_sphere (-v)
simp [chartAt, ChartedSpace.chartAt, Subtype.ext_iff, hfxv, real_inner_comm]
