English
A bijective local diffeomorphism is a diffeomorphism.
Русский
Биективный локальный диффеоморфизм есть диффеоморфизм.
LaTeX
$$$IsLocalDiffeomorph I J n f \wedge Function.Bijective f \Rightarrow Diffeomorph I J M N n$$$
Lean4
/-- A bijective local diffeomorphism is a diffeomorphism. -/
noncomputable def diffeomorph_of_bijective (hf : IsLocalDiffeomorph I J n f) (hf' : Function.Bijective f) :
Diffeomorph I J M N n := by
-- Choose a right inverse `g` of `f`.
choose g hgInverse using (Function.bijective_iff_has_inverse).mp hf'
choose Φ hyp using
(fun x ↦ hf x)
-- Two such diffeomorphisms (and their inverses!) coincide on their sources:
-- they're both inverses to g. In fact, the latter suffices for our proof.
-- have (x y) : EqOn (Φ x).symm (Φ y).symm ((Φ x).target ∩ (Φ y).target) := sorry
have aux (x) : EqOn g (Φ x).symm (Φ x).target :=
eqOn_of_leftInvOn_of_rightInvOn (fun x' _ ↦ hgInverse.1 x')
(LeftInvOn.congr_left ((Φ x).toOpenPartialHomeomorph).rightInvOn ((Φ x).toOpenPartialHomeomorph).symm_mapsTo
(hyp x).2.symm)
(fun _y hy ↦ (Φ x).map_target hy)
exact
{ toFun := f
invFun := g
left_inv := hgInverse.1
right_inv := hgInverse.2
contMDiff_toFun := hf.contMDiff
contMDiff_invFun := by
intro y
let x := g y
obtain ⟨hx, hfx⟩ := hyp x
apply ((Φ x).symm.contMDiffOn.congr (aux x)).contMDiffAt (((Φ x).open_target).mem_nhds ?_)
have : y = (Φ x) x := ((hgInverse.2 y).congr (hfx hx)).mp rfl
exact this ▸ (Φ x).map_source hx }
