English
Under the same locality assumptions, there exists Φ on a set U with neighborhood patches such that e restricted to patches equals the fiberwise open partial homeomorphism induced by Φ, in a coherent way across overlaps.
Русский
При тех же допущениях локальности существует Φ на множестве U с участками, так что ограничение e на локальных участках совпадает с соответствующим волокновым отображением, задаваемым Φ, на пересечениях они согласованы.
LaTeX
$$$\\exists Φ: B \\to F \\; [fields],\\ U, hU, hΦ, h2Φ:\\; e|_{u\\times univ} = FiberwiseLinear.openPartialHomeomorph Φ hU hΦ h2Φ$$$
Lean4
/-- Let `e` be an open partial homeomorphism of `B × F` whose source is `U ×ˢ univ`, for some set
`U` in `B`, and which, 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. Then `e` itself
is equal to some bi-`C^n` fiberwise linear open partial homeomorphism.
This is the key mathematical point of the `locality` condition in the construction of the
`StructureGroupoid` of bi-`C^n` fiberwise linear open partial homeomorphisms. The proof is by
gluing together the various bi-`C^n` fiberwise linear open partial homeomorphism which exist
locally.
The `U` in the conclusion is the same `U` as in the hypothesis. We state it like this, because this
is exactly what we need for `contMDiffFiberwiseLinear`. -/
theorem locality_aux₂ (n : WithTop ℕ∞) (e : OpenPartialHomeomorph (B × F) (B × F)) (U : Set B)
(hU : e.source = U ×ˢ univ)
(h :
∀ 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)) :
∃ (Φ : 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.EqOnSource (FiberwiseLinear.openPartialHomeomorph Φ hU₀ hΦ.continuousOn h2Φ.continuousOn) :=
by
classical
rw [SetCoe.forall'] at h
choose! φ u hu hUu hux hφ h2φ heφ using h
have heuφ : ∀ x : U, EqOn e (fun q => (q.1, φ x q.1 q.2)) (u x ×ˢ univ) := fun x p hp ↦
by
refine (heφ x).2 ?_
rw [(heφ x).1]
exact hp
have huφ : ∀ (x x' : U) (y : B), y ∈ u x → y ∈ u x' → φ x y = φ x' y := fun p p' y hyp hyp' ↦
by
ext v
have h1 : e (y, v) = (y, φ p y v) := heuφ _ ⟨(id hyp : (y, v).fst ∈ u p), trivial⟩
have h2 : e (y, v) = (y, φ p' y v) := heuφ _ ⟨(id hyp' : (y, v).fst ∈ u p'), trivial⟩
exact congr_arg Prod.snd (h1.symm.trans h2)
have hUu' : U = ⋃ i, u i := by
ext x
rw [mem_iUnion]
refine ⟨fun h => ⟨⟨x, h⟩, hux _⟩, ?_⟩
rintro ⟨x, hx⟩
exact hUu x hx
have hU' : IsOpen U := by
rw [hUu']
apply isOpen_iUnion hu
let Φ₀ : U → F ≃L[𝕜] F := iUnionLift u (fun x => φ x ∘ (↑)) huφ U hUu'.le
let Φ : B → F ≃L[𝕜] F := fun y => if hy : y ∈ U then Φ₀ ⟨y, hy⟩ else ContinuousLinearEquiv.refl 𝕜 F
have hΦ : ∀ (y) (hy : y ∈ U), Φ y = Φ₀ ⟨y, hy⟩ := fun y hy => dif_pos hy
have hΦφ : ∀ x : U, ∀ y ∈ u x, Φ y = φ x y := by
intro x y hyu
refine (hΦ y (hUu x hyu)).trans ?_
exact iUnionLift_mk ⟨y, hyu⟩ _
have hΦ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun y => (Φ y : F →L[𝕜] F)) U :=
by
apply contMDiffOn_of_locally_contMDiffOn
intro x hx
refine ⟨u ⟨x, hx⟩, hu ⟨x, hx⟩, hux _, ?_⟩
refine (ContMDiffOn.congr (hφ ⟨x, hx⟩) ?_).mono inter_subset_right
intro y hy
rw [hΦφ ⟨x, hx⟩ y hy]
have h2Φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun y => ((Φ y).symm : F →L[𝕜] F)) U :=
by
apply contMDiffOn_of_locally_contMDiffOn
intro x hx
refine ⟨u ⟨x, hx⟩, hu ⟨x, hx⟩, hux _, ?_⟩
refine (ContMDiffOn.congr (h2φ ⟨x, hx⟩) ?_).mono inter_subset_right
intro y hy
rw [hΦφ ⟨x, hx⟩ y hy]
refine ⟨Φ, U, hU', hΦ, h2Φ, hU, fun p hp => ?_⟩
rw [hU] at hp
rw [heuφ ⟨p.fst, hp.1⟩ ⟨hux _, hp.2⟩]
congrm (_, ?_)
rw [hΦφ]
apply hux
