English
A local diffeomorphism that is bijective yields a diffeomorphism structure.
Русский
Локальный диффеоморфизм, являющийся биективным, образует структуру диффеоморфизма.
LaTeX
$$$IsLocalDiffeomorph I J n f \Rightarrow Function.Bijective f \Rightarrow Diffeomorph I J M N n$$$
Lean4
/-- If `f` is a `C^n` local diffeomorphism at `x`, for `n ≥ 1`, the differential `df_x`
is a linear equivalence. -/
noncomputable def mfderivToContinuousLinearEquiv (hf : IsLocalDiffeomorphAt I J n f x) (hn : 1 ≤ n) :
TangentSpace I x ≃L[𝕜] TangentSpace J (f x)
where
toFun := mfderiv I J f x
invFun := mfderiv J I hf.localInverse (f x)
left_inv := by
apply ContinuousLinearMap.leftInverse_of_comp
rw [← mfderiv_id, ← hf.localInverse_eventuallyEq_left.mfderiv_eq]
exact (mfderiv_comp _ (hf.localInverse_mdifferentiableAt hn) (hf.mdifferentiableAt hn)).symm
right_inv := by
apply ContinuousLinearMap.rightInverse_of_comp
rw [← mfderiv_id, ← hf.localInverse_eventuallyEq_right.mfderiv_eq]
-- We need to rewrite the base point hf.localInverse (f x) = x twice,
-- in the differentiability hypothesis and for applying the chain rule.
have hf' : MDifferentiableAt I J f (hf.localInverse (f x)) :=
by
rw [hf.localInverse_left_inv hf.localInverse_mem_target]
exact hf.mdifferentiableAt hn
rw [mfderiv_comp _ hf' (hf.localInverse_mdifferentiableAt hn), hf.localInverse_left_inv hf.localInverse_mem_target]
continuous_toFun := (mfderiv I J f x).cont
continuous_invFun := (mfderiv J I hf.localInverse (f x)).cont
map_add' := fun x_1 y ↦ ContinuousLinearMap.map_add _ x_1 y
map_smul' := by intros; simp
