mfderiv_coe_sphere_injective — Mathlib

English

The differential of the sphere inclusion map at v is injective: dι_v : T_vS → E is one-to-one.

Русский

Дифференциал включения сферы в точке v является инъективным: dι_v : T_vS → E — взаимно однозначен по своим значениям.

LaTeX

$$$$\text{the map } d\iota_v: T_vS \to E \text{ is injective.}$$$$

Lean4

/-- Consider the differential of the inclusion of the sphere in `E` at the point `v` as a continuous
linear map from `TangentSpace (𝓡 n) v` to `E`.  This map is injective. -/
theorem mfderiv_coe_sphere_injective {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1) :
    Injective (mfderiv (𝓡 n) 𝓘(ℝ, E) ((↑) : sphere (0 : E) 1 → E) v) :=
  by
  rw [((contMDiff_coe_sphere v).mdifferentiableAt le_top).mfderiv]
  simp only [chartAt, fderivWithin_univ, mfld_simps]
  let U := (OrthonormalBasis.fromOrthogonalSpanSingleton (𝕜 := ℝ) n (ne_zero_of_mem_unit_sphere (-v))).repr
  suffices Injective (fderiv ℝ ((stereoInvFunAux (-v : E) ∘ (↑)) ∘ U.symm) 0)
    by
    convert this using 3
    apply stereographic'_neg
  have :
    HasFDerivAt (stereoInvFunAux (-v : E) ∘ (Subtype.val : (ℝ ∙ (↑(-v) : E))ᗮ → E)) (ℝ ∙ (↑(-v) : E))ᗮ.subtypeL
      (U.symm 0) :=
    by
    convert hasFDerivAt_stereoInvFunAux_comp_coe (-v : E)
    simp
  have := congr_arg DFunLike.coe <| (this.comp 0 U.symm.toContinuousLinearEquiv.hasFDerivAt).fderiv
  refine Eq.subst this.symm ?_
  rw [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe]
  simpa [-Subtype.val_injective] using Subtype.val_injective

Похожие утверждения