mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm

English

Again, the range of mfderiv at x equals the entire tangent space (top).

Русский

Ещё раз: диапазон mfderiv в x равен всему касательному пространству (верх).

LaTeX

$$$\operatorname{range}(mfderiv I I' e x) = \top$$$

Lean4

/-- The composition of the derivative of `extChartAt` with the derivative of the inverse of
`extChartAt` gives the identity.
Version where the basepoint belongs to `(extChartAt I x).target`. -/
theorem mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm {x : M} {y : E} (hy : y ∈ (extChartAt I x).target) :
    (mfderiv I 𝓘(𝕜, E) (extChartAt I x) ((extChartAt I x).symm y)) ∘L
        (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) y) =
      ContinuousLinearMap.id _ _ :=
  by
  have U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range ↑I) y :=
    by
    apply I.uniqueMDiffOn
    exact extChartAt_target_subset_range x hy
  have h'y : (extChartAt I x).symm y ∈ (extChartAt I x).source := (extChartAt I x).map_target hy
  have h''y : (extChartAt I x).symm y ∈ (chartAt H x).source := by rwa [← extChartAt_source (I := I)]
  rw [← mfderiv_comp_mfderivWithin]; rotate_left
  · apply mdifferentiableAt_extChartAt h''y
  · exact mdifferentiableWithinAt_extChartAt_symm hy
  · exact U
  rw [← mfderivWithin_id U]
  apply Filter.EventuallyEq.mfderivWithin_eq
  · filter_upwards [extChartAt_target_mem_nhdsWithin_of_mem hy] with z hz
    simp only [Function.comp_def, PartialEquiv.right_inv (extChartAt I x) hz, id_eq]
  · simp only [Function.comp_def, PartialEquiv.right_inv (extChartAt I x) hy, id_eq]

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