English
If an open partial homeomorphism of B×F can be locally described as a bi-C^n fiberwise linear partial homeomorphism around each point, then globally around a neighborhood of each base point there exists a bi-C^n fiberwise linear partial homeomorphism representing the map on a patch, with the same base neighborhood U.
Русский
Если отображение вдоль волокна можно локально описать как би-C^n гомоморфизм вдоль каждого пункта, то по основе существует локальная би-C^n линейная картина на участке, соответствующая глобальной карте.
LaTeX
$$$\\forall p\\in e.s; \\exists s,\\; p\\in s,\\; \\exists φ,u,hu,hφ,h2φ:\\; (e|_s) = (FiberwiseLinear.openPartialHomeomorph φ hu hφ.hcontinuous h2φ.continuous).$$$
Lean4
/-- Let `e` be an open partial homeomorphism of `B × F`. Suppose that at every point `p` in the
source of `e`, there is some neighbourhood `s` of `p` on which `e` is equal to a bi-`C^n` fiberwise
linear open partial homeomorphism.
Then the source of `e` is of the form `U ×ˢ univ`, for some set `U` in `B`, and, at any point `x` in
`U`, admits a neighbourhood `u` of `x` such that `e` is equal on `u ×ˢ univ` to some bi-`C^n`
fiberwise linear open partial homeomorphism. -/
theorem locality_aux₁ (n : WithTop ℕ∞) (e : OpenPartialHomeomorph (B × F) (B × F))
(h :
∀ p ∈ e.source,
∃ s : Set (B × F),
IsOpen s ∧
p ∈ s ∧
∃ (φ : B → F ≃L[𝕜] F) (u : Set B) (hu : IsOpen u) (hφ :
ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => (φ x : F →L[𝕜] F)) u) (h2φ :
ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => ((φ x).symm : F →L[𝕜] F)) u),
(e.restr s).EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hu hφ.continuousOn h2φ.continuousOn)) :
∃ U : Set B,
e.source = U ×ˢ univ ∧
∀ x ∈ U,
∃ (φ : B → F ≃L[𝕜] F) (u : Set B) (hu : IsOpen u) (_huU : u ⊆ U) (_hux : x ∈ u),
∃ (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => (φ x : F →L[𝕜] F)) u) (h2φ :
ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => ((φ x).symm : F →L[𝕜] F)) u),
(e.restr (u ×ˢ univ)).EqOnSource
(FiberwiseLinear.openPartialHomeomorph φ hu hφ.continuousOn h2φ.continuousOn) :=
by
rw [SetCoe.forall'] at h
choose s hs hsp φ u hu hφ h2φ heφ using h
have hesu : ∀ p : e.source, e.source ∩ s p = u p ×ˢ univ :=
by
intro p
rw [← e.restr_source' (s _) (hs _)]
exact (heφ p).1
have hu' : ∀ p : e.source, (p : B × F).fst ∈ u p := by
intro p
have : (p : B × F) ∈ e.source ∩ s p := ⟨p.prop, hsp p⟩
simpa only [hesu, mem_prod, mem_univ, and_true] using this
have heu : ∀ p : e.source, ∀ q : B × F, q.fst ∈ u p → q ∈ e.source :=
by
intro p q hq
have : q ∈ u p ×ˢ (univ : Set F) := ⟨hq, trivial⟩
rw [← hesu p] at this
exact this.1
have he : e.source = (Prod.fst '' e.source) ×ˢ (univ : Set F) :=
by
apply HasSubset.Subset.antisymm
· intro p hp
exact ⟨⟨p, hp, rfl⟩, trivial⟩
· rintro ⟨x, v⟩ ⟨⟨p, hp, rfl : p.fst = x⟩, -⟩
exact heu ⟨p, hp⟩ (p.fst, v) (hu' ⟨p, hp⟩)
refine ⟨Prod.fst '' e.source, he, ?_⟩
rintro x ⟨p, hp, rfl⟩
refine ⟨φ ⟨p, hp⟩, u ⟨p, hp⟩, hu ⟨p, hp⟩, ?_, hu' _, hφ ⟨p, hp⟩, h2φ ⟨p, hp⟩, ?_⟩
· intro y hy; exact ⟨(y, 0), heu ⟨p, hp⟩ ⟨_, _⟩ hy, rfl⟩
· rw [← hesu, e.restr_source_inter]; exact heφ ⟨p, hp⟩
