English
Variant identity for derivative composition with inverse chart.
Русский
Вариант тождества композиции дифференциалов с инверсной картой.
LaTeX
$$$mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm' : \; \text{identity formula}$$$
Lean4
/-- The composition of the derivative of the inverse of `extChartAt` with the derivative of
`extChartAt` gives the identity.
Version where the basepoint belongs to `(extChartAt I x).target`. -/
theorem mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt {y : E} (hy : y ∈ (extChartAt I x).target) :
(mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) y) ∘L
(mfderiv I 𝓘(𝕜, E) (extChartAt I x) ((extChartAt I x).symm y)) =
ContinuousLinearMap.id _ _ :=
by
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)]
have U' : UniqueMDiffWithinAt I (extChartAt I x).source ((extChartAt I x).symm y) :=
(isOpen_extChartAt_source x).uniqueMDiffWithinAt h'y
have :
mfderiv I 𝓘(𝕜, E) (extChartAt I x) ((extChartAt I x).symm y) =
mfderivWithin I 𝓘(𝕜, E) (extChartAt I x) (extChartAt I x).source ((extChartAt I x).symm y) :=
by
rw [mfderivWithin_eq_mfderiv U']
exact mdifferentiableAt_extChartAt h''y
rw [this, ← mfderivWithin_comp_of_eq]; rotate_left
· exact mdifferentiableWithinAt_extChartAt_symm hy
· exact (mdifferentiableAt_extChartAt h''y).mdifferentiableWithinAt
· intro z hz
apply extChartAt_target_subset_range x
exact PartialEquiv.map_source (extChartAt I x) hz
· exact U'
· exact PartialEquiv.right_inv (extChartAt I x) hy
rw [← mfderivWithin_id U']
apply Filter.EventuallyEq.mfderivWithin_eq
· filter_upwards [extChartAt_source_mem_nhdsWithin' h'y] with z hz
simp only [Function.comp_def, PartialEquiv.left_inv (extChartAt I x) hz, id_eq]
· simp only [Function.comp_def, PartialEquiv.right_inv (extChartAt I x) hy, id_eq]
