English
If a lift-prop hf expresses a local structomorphism for contDiffGroupoid n I, then f is C^n on its domain I.
Русский
Если hf выражает локальную структуроморфность для contDiffGroupoid n I, то f является C^n на своей области
Lean4
theorem isLocalStructomorphOn_contDiffGroupoid_iff_aux {f : OpenPartialHomeomorph M M'}
(hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt f f.source) : ContMDiffOn I I n f f.source := by
-- It suffices to show regularity near each `x`
apply contMDiffOn_of_locally_contMDiffOn
intro x hx
let c := chartAt H x
let c' := chartAt H (f x)
obtain ⟨-, hxf⟩ := hf x hx
obtain ⟨e, he, he' : EqOn (c' ∘ f ∘ c.symm) e (c.symm ⁻¹' f.source ∩ e.source), hex : c x ∈ e.source⟩ :=
hxf
(by simp only [hx, mfld_simps])
-- We choose a convenient set `s` in `M`.
let s : Set M := (f.trans c').source ∩ ((c.trans e).trans c'.symm).source
refine ⟨s, (f.trans c').open_source.inter ((c.trans e).trans c'.symm).open_source, ?_, ?_⟩
· simp only [s, mfld_simps]
rw [← he'] <;>
simp only [c, c', hx, hex, mfld_simps]
-- We need to show `f` is `ContMDiffOn` the domain `s ∩ f.source`. We show this in two
-- steps: `f` is equal to `c'.symm ∘ e ∘ c` on that domain and that function is
-- `ContMDiffOn` it.
have H₁ : ContMDiffOn I I n (c'.symm ∘ e ∘ c) s :=
by
have hc' : ContMDiffOn I I n c'.symm _ := contMDiffOn_chart_symm
have he'' : ContMDiffOn I I n e _ := contMDiffOn_of_mem_contDiffGroupoid he
have hc : ContMDiffOn I I n c _ := contMDiffOn_chart
refine (hc'.comp' (he''.comp' hc)).mono ?_
dsimp [s, c, c']
mfld_set_tac
have H₂ : EqOn f (c'.symm ∘ e ∘ c) s := by
intro y hy
simp only [s, mfld_simps] at hy
have hy₁ : f y ∈ c'.source := by simp only [hy, mfld_simps]
have hy₂ : y ∈ c.source := by simp only [hy, mfld_simps]
have hy₃ : c y ∈ c.symm ⁻¹' f.source ∩ e.source := by simp only [hy, mfld_simps]
calc
f y = c'.symm (c' (f y)) := by rw [c'.left_inv hy₁]
_ = c'.symm (c' (f (c.symm (c y)))) := by rw [c.left_inv hy₂]
_ = c'.symm (e (c y)) := by rw [← he' hy₃]; rfl
refine (H₁.congr H₂).mono ?_
mfld_set_tac
