Continuous bundle homomorphisms and their inverses #
For a bundle with finite-dimensional model source, continuity of a fibrewise linear map on total spaces is equivalent to continuity as a section of Mathlib's Hom bundle. Consequently a continuous fibrewise linear equivalence gives a homeomorphism of total spaces: continuity of the inverse need not be supplied separately.
We also prove local continuity of inversion for Hom-bundle sections with a Banach model
source. This local result does not require finite rank or invertibility away from the
point under consideration. The inverse is Mathlib's ContinuousLinearMap.inverse,
which is zero at noninvertible maps. In the same generality, invertibility of the fibre
maps is an open condition along a continuous Hom-bundle section, composition of
continuous Hom-bundle sections is continuous, and a σ-semilinear Hom-bundle section whose
preferred-frame coordinate expression is locally constant around each frame centre is continuous
(TauCeti.continuous_hom_bundle_of_inCoordinates_eq_const). Read in the trivializations at a
fixed point, a continuous Hom-bundle section is a continuous family of operators on their common
base set (TauCeti.continuousOn_inCoordinates).
For two vector bundle cores, a section of Mathlib's Hom bundle between them is continuous
exactly when it is continuous in every pair of a source chart and a target chart, on their
common domain, with chart expressions VectorBundleCore.inChartCoordinates
(VectorBundleCore.continuous_hom_bundle_iff_forall_continuousOn). Both directions read the
section through the local trivializations of the two charts
(VectorBundleCore.inChartCoordinates_eq_localTriv_comp in
TauCeti.Topology.VectorBundle.Coordinates).
The coordinate argument uses ContinuousLinearMap.inCoordinates_inverse and parallels
the smooth inverse argument in TauCeti.Geometry.Manifold.VectorBundle.Hom.
For the classical finite-rank bundle-isomorphism criterion see Hatcher,
Vector Bundles and K-Theory, §1.1.
Fibre maps between moving base points #
A family of fibre maps ϕ m : V (b₁ m) →L[𝕜] W (b₂ m) over two base maps is read through the
preferred trivializations centred at b₁ m₀ and b₂ m₀, as in Mathlib's
ContinuousAt.clm_apply_of_inCoordinates. Continuity of this coordinate expression within a set
at m₀ is preserved by composition and inversion, and makes invertibility an open condition at
m₀ relative to the set. The Hom-bundle lemmas below are the case of a single base map.
theorem
ContinuousWithinAt.inCoordinates_clm_comp
{𝕜 : Type u_1}
{M : Type u_2}
{B : Type u_3}
{B' : Type u_4}
{B'' : Type u_5}
{F : Type u_6}
{F' : Type u_7}
{F'' : Type u_8}
[NontriviallyNormedField 𝕜]
[TopologicalSpace M]
[TopologicalSpace B]
[TopologicalSpace B']
[TopologicalSpace B'']
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
[NormedAddCommGroup F'']
[NormedSpace 𝕜 F'']
{V : B → Type u_9}
[(x : B) → AddCommMonoid (V x)]
[(x : B) → Module 𝕜 (V x)]
[(x : B) → TopologicalSpace (V x)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜 F V]
{W : B' → Type u_10}
[(x : B') → AddCommMonoid (W x)]
[(x : B') → Module 𝕜 (W x)]
[(x : B') → TopologicalSpace (W x)]
[TopologicalSpace (Bundle.TotalSpace F' W)]
[FiberBundle F' W]
[VectorBundle 𝕜 F' W]
{U : B'' → Type u_11}
[(x : B'') → AddCommMonoid (U x)]
[(x : B'') → Module 𝕜 (U x)]
[(x : B'') → TopologicalSpace (U x)]
[TopologicalSpace (Bundle.TotalSpace F'' U)]
[FiberBundle F'' U]
[VectorBundle 𝕜 F'' U]
{b₁ : M → B}
{b₂ : M → B'}
{b₃ : M → B''}
{s : Set M}
{m₀ : M}
{ψ : (m : M) → W (b₂ m) →L[𝕜] U (b₃ m)}
{ϕ : (m : M) → V (b₁ m) →L[𝕜] W (b₂ m)}
(hψ :
ContinuousWithinAt (fun (m : M) => ContinuousLinearMap.inCoordinates F' W F'' U (b₂ m₀) (b₂ m) (b₃ m₀) (b₃ m) (ψ m)) s
m₀)
(hϕ :
ContinuousWithinAt (fun (m : M) => ContinuousLinearMap.inCoordinates F V F' W (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) s
m₀)
(hb₂ : ContinuousWithinAt b₂ s m₀)
:
ContinuousWithinAt
(fun (m : M) => ContinuousLinearMap.inCoordinates F V F'' U (b₁ m₀) (b₁ m) (b₃ m₀) (b₃ m) (ψ m ∘SL ϕ m)) s m₀
If two families of fibre maps are continuous within s at m₀ in coordinates, so is their
composite, provided the intermediate base map is continuous within s at m₀.
theorem
ContinuousAt.inCoordinates_clm_comp
{𝕜 : Type u_1}
{M : Type u_2}
{B : Type u_3}
{B' : Type u_4}
{B'' : Type u_5}
{F : Type u_6}
{F' : Type u_7}
{F'' : Type u_8}
[NontriviallyNormedField 𝕜]
[TopologicalSpace M]
[TopologicalSpace B]
[TopologicalSpace B']
[TopologicalSpace B'']
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
[NormedAddCommGroup F'']
[NormedSpace 𝕜 F'']
{V : B → Type u_9}
[(x : B) → AddCommMonoid (V x)]
[(x : B) → Module 𝕜 (V x)]
[(x : B) → TopologicalSpace (V x)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜 F V]
{W : B' → Type u_10}
[(x : B') → AddCommMonoid (W x)]
[(x : B') → Module 𝕜 (W x)]
[(x : B') → TopologicalSpace (W x)]
[TopologicalSpace (Bundle.TotalSpace F' W)]
[FiberBundle F' W]
[VectorBundle 𝕜 F' W]
{U : B'' → Type u_11}
[(x : B'') → AddCommMonoid (U x)]
[(x : B'') → Module 𝕜 (U x)]
[(x : B'') → TopologicalSpace (U x)]
[TopologicalSpace (Bundle.TotalSpace F'' U)]
[FiberBundle F'' U]
[VectorBundle 𝕜 F'' U]
{b₁ : M → B}
{b₂ : M → B'}
{b₃ : M → B''}
{m₀ : M}
{ψ : (m : M) → W (b₂ m) →L[𝕜] U (b₃ m)}
{ϕ : (m : M) → V (b₁ m) →L[𝕜] W (b₂ m)}
(hψ : ContinuousAt (fun (m : M) => ContinuousLinearMap.inCoordinates F' W F'' U (b₂ m₀) (b₂ m) (b₃ m₀) (b₃ m) (ψ m)) m₀)
(hϕ : ContinuousAt (fun (m : M) => ContinuousLinearMap.inCoordinates F V F' W (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀)
(hb₂ : ContinuousAt b₂ m₀)
:
ContinuousAt (fun (m : M) => ContinuousLinearMap.inCoordinates F V F'' U (b₁ m₀) (b₁ m) (b₃ m₀) (b₃ m) (ψ m ∘SL ϕ m)) m₀
If two families of fibre maps are continuous at m₀ in coordinates, so is their composite,
provided the intermediate base map is continuous at m₀.
theorem
ContinuousWithinAt.eventually_isInvertible_of_inCoordinates
{𝕜 : Type u_1}
{M : Type u_2}
{B : Type u_3}
{B' : Type u_4}
{F : Type u_6}
{F' : Type u_7}
[NontriviallyNormedField 𝕜]
[TopologicalSpace M]
[TopologicalSpace B]
[TopologicalSpace B']
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{V : B → Type u_9}
[(x : B) → AddCommMonoid (V x)]
[(x : B) → Module 𝕜 (V x)]
[(x : B) → TopologicalSpace (V x)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜 F V]
{W : B' → Type u_10}
[(x : B') → AddCommMonoid (W x)]
[(x : B') → Module 𝕜 (W x)]
[(x : B') → TopologicalSpace (W x)]
[TopologicalSpace (Bundle.TotalSpace F' W)]
[FiberBundle F' W]
[VectorBundle 𝕜 F' W]
{b₁ : M → B}
{b₂ : M → B'}
{s : Set M}
{m₀ : M}
[CompleteSpace F]
{ϕ : (m : M) → V (b₁ m) →L[𝕜] W (b₂ m)}
(hϕ :
ContinuousWithinAt (fun (m : M) => ContinuousLinearMap.inCoordinates F V F' W (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) s
m₀)
(hb₁ : ContinuousWithinAt b₁ s m₀)
(hb₂ : ContinuousWithinAt b₂ s m₀)
(hm₀ : (ϕ m₀).IsInvertible)
:
∀ᶠ (m : M) in nhdsWithin m₀ s, (ϕ m).IsInvertible
Along a family of fibre maps continuous within s at m₀ in coordinates and invertible at
m₀, the fibre maps at nearby points of s are invertible, provided both base maps are
continuous within s at m₀.
theorem
ContinuousAt.eventually_isInvertible_of_inCoordinates
{𝕜 : Type u_1}
{M : Type u_2}
{B : Type u_3}
{B' : Type u_4}
{F : Type u_6}
{F' : Type u_7}
[NontriviallyNormedField 𝕜]
[TopologicalSpace M]
[TopologicalSpace B]
[TopologicalSpace B']
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{V : B → Type u_9}
[(x : B) → AddCommMonoid (V x)]
[(x : B) → Module 𝕜 (V x)]
[(x : B) → TopologicalSpace (V x)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜 F V]
{W : B' → Type u_10}
[(x : B') → AddCommMonoid (W x)]
[(x : B') → Module 𝕜 (W x)]
[(x : B') → TopologicalSpace (W x)]
[TopologicalSpace (Bundle.TotalSpace F' W)]
[FiberBundle F' W]
[VectorBundle 𝕜 F' W]
{b₁ : M → B}
{b₂ : M → B'}
{m₀ : M}
[CompleteSpace F]
{ϕ : (m : M) → V (b₁ m) →L[𝕜] W (b₂ m)}
(hϕ : ContinuousAt (fun (m : M) => ContinuousLinearMap.inCoordinates F V F' W (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀)
(hb₁ : ContinuousAt b₁ m₀)
(hb₂ : ContinuousAt b₂ m₀)
(hm₀ : (ϕ m₀).IsInvertible)
:
∀ᶠ (m : M) in nhds m₀, (ϕ m).IsInvertible
Along a family of fibre maps continuous at m₀ in coordinates and invertible at m₀, the
fibre maps at nearby points are invertible, provided both base maps are continuous at m₀.
theorem
ContinuousWithinAt.inCoordinates_clm_inverse
{𝕜 : Type u_1}
{M : Type u_2}
{B : Type u_3}
{B' : Type u_4}
{F : Type u_6}
{F' : Type u_7}
[NontriviallyNormedField 𝕜]
[TopologicalSpace M]
[TopologicalSpace B]
[TopologicalSpace B']
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{V : B → Type u_9}
[(x : B) → AddCommMonoid (V x)]
[(x : B) → Module 𝕜 (V x)]
[(x : B) → TopologicalSpace (V x)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜 F V]
{W : B' → Type u_10}
[(x : B') → AddCommMonoid (W x)]
[(x : B') → Module 𝕜 (W x)]
[(x : B') → TopologicalSpace (W x)]
[TopologicalSpace (Bundle.TotalSpace F' W)]
[FiberBundle F' W]
[VectorBundle 𝕜 F' W]
{b₁ : M → B}
{b₂ : M → B'}
{s : Set M}
{m₀ : M}
[CompleteSpace F]
{ϕ : (m : M) → V (b₁ m) →L[𝕜] W (b₂ m)}
(hϕ :
ContinuousWithinAt (fun (m : M) => ContinuousLinearMap.inCoordinates F V F' W (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) s
m₀)
(hm₀ : (ϕ m₀).IsInvertible)
:
ContinuousWithinAt
(fun (m : M) => ContinuousLinearMap.inCoordinates F' W F V (b₂ m₀) (b₂ m) (b₁ m₀) (b₁ m) (ϕ m).inverse) s m₀
Inversion preserves continuity within s at m₀ in coordinates of a family of fibre maps
invertible at m₀. No continuity of the base maps is needed. Only the model source must be
complete.
theorem
ContinuousAt.inCoordinates_clm_inverse
{𝕜 : Type u_1}
{M : Type u_2}
{B : Type u_3}
{B' : Type u_4}
{F : Type u_6}
{F' : Type u_7}
[NontriviallyNormedField 𝕜]
[TopologicalSpace M]
[TopologicalSpace B]
[TopologicalSpace B']
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{V : B → Type u_9}
[(x : B) → AddCommMonoid (V x)]
[(x : B) → Module 𝕜 (V x)]
[(x : B) → TopologicalSpace (V x)]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle 𝕜 F V]
{W : B' → Type u_10}
[(x : B') → AddCommMonoid (W x)]
[(x : B') → Module 𝕜 (W x)]
[(x : B') → TopologicalSpace (W x)]
[TopologicalSpace (Bundle.TotalSpace F' W)]
[FiberBundle F' W]
[VectorBundle 𝕜 F' W]
{b₁ : M → B}
{b₂ : M → B'}
{m₀ : M}
[CompleteSpace F]
{ϕ : (m : M) → V (b₁ m) →L[𝕜] W (b₂ m)}
(hϕ : ContinuousAt (fun (m : M) => ContinuousLinearMap.inCoordinates F V F' W (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀)
(hm₀ : (ϕ m₀).IsInvertible)
:
ContinuousAt (fun (m : M) => ContinuousLinearMap.inCoordinates F' W F V (b₂ m₀) (b₂ m) (b₁ m₀) (b₁ m) (ϕ m).inverse) m₀
Inversion preserves continuity at m₀ in coordinates of a family of fibre maps invertible at
m₀. No continuity of the base maps is needed. Only the model source must be complete.
theorem
Bundle.Trivialization.continuousLinearMap_symmL
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
(e₁ : Trivialization F₁ TotalSpace.proj)
(e₂ : Trivialization F₂ TotalSpace.proj)
[MemTrivializationAtlas e₁]
[MemTrivializationAtlas e₂]
(x : B)
(A : F₁ →L[𝕜] F₂)
:
(symmL 𝕜 (continuousLinearMap (RingHom.id 𝕜) e₁ e₂) x) A = symmL 𝕜 e₂ x ∘SL A ∘SL continuousLinearMapAt 𝕜 e₁ x
Inverse Hom-frame coordinates conjugate a model operator by the inverse target frame and forward source frame. No square identity or equality of the two model fibres is required, and both sides vanish outside the common base set.
theorem
TauCeti.continuous_hom_bundle_iff
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F₁]
(ϕ : (x : B) → E₁ x →L[𝕜] E₂ x)
:
(Continuous fun (x : B) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) x (ϕ x)) ↔ Continuous fun (p : Bundle.TotalSpace F₁ E₁) => Bundle.TotalSpace.mk' F₂ p.proj ((ϕ p.proj) p.snd)
For a finite-dimensional model source, a fibrewise continuous linear map is continuous on total spaces exactly when it is continuous as a section of the Hom bundle. The target need not have finite rank.
theorem
TauCeti.continuousOn_inCoordinates
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
{ϕ : (x : B) → E₁ x →L[𝕜] E₂ x}
(hϕ : Continuous fun (x : B) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) x (ϕ x))
(x₀ : B)
:
ContinuousOn (fun (x : B) => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ x₀ x x₀ x (ϕ x))
((trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet)
On the common base set of the trivializations at x₀, the coordinate expressions of a
continuous Hom-bundle section in these fixed trivializations form a continuous family of
operators.
theorem
ContinuousWithinAt.eventually_clm_bundle_isInvertible
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_5}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[TopologicalSpace M]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
[CompleteSpace F₁]
{b : M → B}
{ϕ : (m : M) → E₁ (b m) →L[𝕜] E₂ (b m)}
{s : Set M}
{x : M}
(hϕ : ContinuousWithinAt (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m)) s x)
(hx : (ϕ x).IsInvertible)
:
∀ᶠ (m : M) in nhdsWithin x s, (ϕ m).IsInvertible
Along a Hom-bundle section continuous within a set at a point where its fibre map is invertible, the fibre maps at nearby points of the set are invertible too. Only the model source must be complete.
theorem
ContinuousAt.eventually_clm_bundle_isInvertible
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_5}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[TopologicalSpace M]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
[CompleteSpace F₁]
{b : M → B}
{ϕ : (m : M) → E₁ (b m) →L[𝕜] E₂ (b m)}
{x : M}
(hϕ : ContinuousAt (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m)) x)
(hx : (ϕ x).IsInvertible)
:
∀ᶠ (m : M) in nhds x, (ϕ m).IsInvertible
Along a Hom-bundle section continuous at a point where its fibre map is invertible, the fibre maps at nearby points are invertible too.
theorem
Continuous.isOpen_setOf_clm_bundle_isInvertible
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_5}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[TopologicalSpace M]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
[CompleteSpace F₁]
{b : M → B}
{ϕ : (m : M) → E₁ (b m) →L[𝕜] E₂ (b m)}
(hϕ : Continuous fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m))
:
The points at which a continuous Hom-bundle section is invertible form an open set.
theorem
ContinuousWithinAt.clm_bundle_inverse
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_5}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[TopologicalSpace M]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
[CompleteSpace F₁]
[∀ (x : B), IsTopologicalAddGroup (E₁ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₁ x)]
{b : M → B}
{ϕ : (m : M) → E₁ (b m) →L[𝕜] E₂ (b m)}
{s : Set M}
{x : M}
(hϕ : ContinuousWithinAt (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m)) s x)
(hx : (ϕ x).IsInvertible)
:
ContinuousWithinAt (fun (m : M) => Bundle.TotalSpace.mk' (F₂ →L[𝕜] F₁) (b m) (ϕ m).inverse) s x
Inversion of a continuous Hom-bundle section is continuous within a set at any point where the fibre map is invertible. Only the model source must be complete.
theorem
ContinuousAt.clm_bundle_inverse
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_5}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[TopologicalSpace M]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
[CompleteSpace F₁]
[∀ (x : B), IsTopologicalAddGroup (E₁ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₁ x)]
{b : M → B}
{ϕ : (m : M) → E₁ (b m) →L[𝕜] E₂ (b m)}
{x : M}
(hϕ : ContinuousAt (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m)) x)
(hx : (ϕ x).IsInvertible)
:
ContinuousAt (fun (m : M) => Bundle.TotalSpace.mk' (F₂ →L[𝕜] F₁) (b m) (ϕ m).inverse) x
Inversion of a continuous Hom-bundle section is continuous at a point where its fibre map is invertible.
theorem
ContinuousOn.clm_bundle_inverse
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_5}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[TopologicalSpace M]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
[CompleteSpace F₁]
[∀ (x : B), IsTopologicalAddGroup (E₁ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₁ x)]
{b : M → B}
{ϕ : (m : M) → E₁ (b m) →L[𝕜] E₂ (b m)}
{s : Set M}
(hϕ : ContinuousOn (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m)) s)
(hs : ∀ x ∈ s, (ϕ x).IsInvertible)
:
ContinuousOn (fun (m : M) => Bundle.TotalSpace.mk' (F₂ →L[𝕜] F₁) (b m) (ϕ m).inverse) s
Inversion preserves continuity on a set of fibrewise invertible Hom-bundle maps.
theorem
Continuous.clm_bundle_inverse
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_5}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[TopologicalSpace M]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
[CompleteSpace F₁]
[∀ (x : B), IsTopologicalAddGroup (E₁ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₁ x)]
{b : M → B}
{ϕ : (m : M) → E₁ (b m) →L[𝕜] E₂ (b m)}
(hϕ : Continuous fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m))
(hinv : ∀ (x : M), (ϕ x).IsInvertible)
:
Continuous fun (m : M) => Bundle.TotalSpace.mk' (F₂ →L[𝕜] F₁) (b m) (ϕ m).inverse
Inversion preserves continuity of a fibrewise invertible Hom-bundle section.
theorem
ContinuousWithinAt.clm_bundle_comp
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_5}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[TopologicalSpace M]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
{F₃ : Type u_8}
[NormedAddCommGroup F₃]
[NormedSpace 𝕜 F₃]
{E₃ : B → Type u_9}
[(x : B) → AddCommGroup (E₃ x)]
[(x : B) → Module 𝕜 (E₃ x)]
[(x : B) → TopologicalSpace (E₃ x)]
[TopologicalSpace (Bundle.TotalSpace F₃ E₃)]
[FiberBundle F₃ E₃]
[VectorBundle 𝕜 F₃ E₃]
[∀ (x : B), IsTopologicalAddGroup (E₃ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₃ x)]
{b : M → B}
{ψ : (m : M) → E₂ (b m) →L[𝕜] E₃ (b m)}
{ϕ : (m : M) → E₁ (b m) →L[𝕜] E₂ (b m)}
{s : Set M}
{x : M}
(hψ : ContinuousWithinAt (fun (m : M) => Bundle.TotalSpace.mk' (F₂ →L[𝕜] F₃) (b m) (ψ m)) s x)
(hϕ : ContinuousWithinAt (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m)) s x)
:
ContinuousWithinAt (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₃) (b m) (ψ m ∘SL ϕ m)) s x
Composition of Hom-bundle sections continuous within a set is continuous within it.
theorem
ContinuousAt.clm_bundle_comp
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_5}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[TopologicalSpace M]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
{F₃ : Type u_8}
[NormedAddCommGroup F₃]
[NormedSpace 𝕜 F₃]
{E₃ : B → Type u_9}
[(x : B) → AddCommGroup (E₃ x)]
[(x : B) → Module 𝕜 (E₃ x)]
[(x : B) → TopologicalSpace (E₃ x)]
[TopologicalSpace (Bundle.TotalSpace F₃ E₃)]
[FiberBundle F₃ E₃]
[VectorBundle 𝕜 F₃ E₃]
[∀ (x : B), IsTopologicalAddGroup (E₃ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₃ x)]
{b : M → B}
{ψ : (m : M) → E₂ (b m) →L[𝕜] E₃ (b m)}
{ϕ : (m : M) → E₁ (b m) →L[𝕜] E₂ (b m)}
{x : M}
(hψ : ContinuousAt (fun (m : M) => Bundle.TotalSpace.mk' (F₂ →L[𝕜] F₃) (b m) (ψ m)) x)
(hϕ : ContinuousAt (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m)) x)
:
ContinuousAt (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₃) (b m) (ψ m ∘SL ϕ m)) x
Composition of Hom-bundle sections continuous at a point is continuous there.
theorem
ContinuousOn.clm_bundle_comp
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_5}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[TopologicalSpace M]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
{F₃ : Type u_8}
[NormedAddCommGroup F₃]
[NormedSpace 𝕜 F₃]
{E₃ : B → Type u_9}
[(x : B) → AddCommGroup (E₃ x)]
[(x : B) → Module 𝕜 (E₃ x)]
[(x : B) → TopologicalSpace (E₃ x)]
[TopologicalSpace (Bundle.TotalSpace F₃ E₃)]
[FiberBundle F₃ E₃]
[VectorBundle 𝕜 F₃ E₃]
[∀ (x : B), IsTopologicalAddGroup (E₃ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₃ x)]
{b : M → B}
{ψ : (m : M) → E₂ (b m) →L[𝕜] E₃ (b m)}
{ϕ : (m : M) → E₁ (b m) →L[𝕜] E₂ (b m)}
{s : Set M}
(hψ : ContinuousOn (fun (m : M) => Bundle.TotalSpace.mk' (F₂ →L[𝕜] F₃) (b m) (ψ m)) s)
(hϕ : ContinuousOn (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m)) s)
:
ContinuousOn (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₃) (b m) (ψ m ∘SL ϕ m)) s
Composition of Hom-bundle sections continuous on a set is continuous on it.
theorem
Continuous.clm_bundle_comp
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
{M : Type u_5}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[TopologicalSpace M]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
{F₃ : Type u_8}
[NormedAddCommGroup F₃]
[NormedSpace 𝕜 F₃]
{E₃ : B → Type u_9}
[(x : B) → AddCommGroup (E₃ x)]
[(x : B) → Module 𝕜 (E₃ x)]
[(x : B) → TopologicalSpace (E₃ x)]
[TopologicalSpace (Bundle.TotalSpace F₃ E₃)]
[FiberBundle F₃ E₃]
[VectorBundle 𝕜 F₃ E₃]
[∀ (x : B), IsTopologicalAddGroup (E₃ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₃ x)]
{b : M → B}
{ψ : (m : M) → E₂ (b m) →L[𝕜] E₃ (b m)}
{ϕ : (m : M) → E₁ (b m) →L[𝕜] E₂ (b m)}
(hψ : Continuous fun (m : M) => Bundle.TotalSpace.mk' (F₂ →L[𝕜] F₃) (b m) (ψ m))
(hϕ : Continuous fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m))
:
Continuous fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₃) (b m) (ψ m ∘SL ϕ m)
Composition of continuous Hom-bundle sections is continuous.
theorem
TauCeti.continuous_bundle_symm
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F₁]
[∀ (x : B), IsTopologicalAddGroup (E₁ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₁ x)]
(e : (x : B) → E₁ x ≃L[𝕜] E₂ x)
(he : Continuous fun (p : Bundle.TotalSpace F₁ E₁) => Bundle.TotalSpace.mk' F₂ p.proj ((e p.proj) p.snd))
:
Continuous fun (p : Bundle.TotalSpace F₂ E₂) => Bundle.TotalSpace.mk' F₁ p.proj ((e p.proj).symm p.snd)
A continuous fibrewise linear equivalence with finite-dimensional model source has a continuous inverse on total spaces. No compactness or separation of the base is needed.
def
TauCeti.bundleHomeomorph
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F₁]
[∀ (x : B), IsTopologicalAddGroup (E₁ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₁ x)]
(e : (x : B) → E₁ x ≃L[𝕜] E₂ x)
(he : Continuous fun (p : Bundle.TotalSpace F₁ E₁) => Bundle.TotalSpace.mk' F₂ p.proj ((e p.proj) p.snd))
:
The homeomorphism of total spaces induced by a continuous family of fibrewise linear equivalences. Continuity of the inverse follows from finite dimensionality.
Instances For
@[simp]
theorem
TauCeti.bundleHomeomorph_apply
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F₁]
[∀ (x : B), IsTopologicalAddGroup (E₁ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₁ x)]
(e : (x : B) → E₁ x ≃L[𝕜] E₂ x)
(he : Continuous fun (p : Bundle.TotalSpace F₁ E₁) => Bundle.TotalSpace.mk' F₂ p.proj ((e p.proj) p.snd))
(p : Bundle.TotalSpace F₁ E₁)
:
@[simp]
theorem
TauCeti.bundleHomeomorph_symm_apply
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F₁]
[∀ (x : B), IsTopologicalAddGroup (E₁ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₁ x)]
(e : (x : B) → E₁ x ≃L[𝕜] E₂ x)
(he : Continuous fun (p : Bundle.TotalSpace F₁ E₁) => Bundle.TotalSpace.mk' F₂ p.proj ((e p.proj) p.snd))
(p : Bundle.TotalSpace F₂ E₂)
:
theorem
TauCeti.exists_bundleHomeomorph_of_bijective
{𝕜 : Type u_1}
{B : Type u_2}
{F₁ : Type u_3}
{F₂ : Type u_4}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 F₁]
[∀ (x : B), IsTopologicalAddGroup (E₁ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₁ x)]
(ϕ : (x : B) → E₁ x →L[𝕜] E₂ x)
(hϕ : Continuous fun (p : Bundle.TotalSpace F₁ E₁) => Bundle.TotalSpace.mk' F₂ p.proj ((ϕ p.proj) p.snd))
(hbij : ∀ (x : B), Function.Bijective ⇑(ϕ x))
:
∃ (h : Bundle.TotalSpace F₁ E₁ ≃ₜ Bundle.TotalSpace F₂ E₂),
∀ (x : B) (v : E₁ x), h { proj := x, snd := v } = { proj := x, snd := (ϕ x) v }
A continuous fibrewise bijective linear map between vector bundles with a finite-dimensional model source is induced by a homeomorphism of total spaces.
theorem
VectorBundleCore.continuousOn_inChartCoordinates
{𝕜 : Type u_1}
{B : Type u_2}
{F : Type u_3}
{G : Type u_4}
{ι : Type u_5}
{κ : Type u_6}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{Z : VectorBundleCore 𝕜 B F ι}
{W : VectorBundleCore 𝕜 B G κ}
{f : B → F →L[𝕜] G}
{i : ι}
{j : κ}
(hf : ContinuousOn (fun (x : B) => Bundle.TotalSpace.mk' (F →L[𝕜] G) x (f x)) (Z.baseSet i ∩ W.baseSet j))
:
ContinuousOn (fun (x : B) => Z.inChartCoordinates W i j x (f x)) (Z.baseSet i ∩ W.baseSet j)
A section of the Hom bundle between two cores that is continuous on the common domain of a source chart and a target chart is continuous in those charts there.
theorem
VectorBundleCore.continuous_hom_bundle_iff_forall_continuousOn
{𝕜 : Type u_1}
{B : Type u_2}
{F : Type u_3}
{G : Type u_4}
{ι : Type u_5}
{κ : Type u_6}
[NontriviallyNormedField 𝕜]
[TopologicalSpace B]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{Z : VectorBundleCore 𝕜 B F ι}
{W : VectorBundleCore 𝕜 B G κ}
{f : B → F →L[𝕜] G}
:
(Continuous fun (x : B) => Bundle.TotalSpace.mk' (F →L[𝕜] G) x (f x)) ↔ ∀ (i : ι) (j : κ), ContinuousOn (fun (x : B) => Z.inChartCoordinates W i j x (f x)) (Z.baseSet i ∩ W.baseSet j)
A family of fibre maps is a continuous section of the Hom bundle between two cores exactly when it is continuous in every pair of charts.
theorem
TauCeti.continuous_hom_bundle_of_inCoordinates_eq_const
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
{B : Type u_3}
{F₁ : Type u_4}
{F₂ : Type u_5}
[NontriviallyNormedField 𝕜₁]
[NontriviallyNormedField 𝕜₂]
{σ : 𝕜₁ →+* 𝕜₂}
[RingHomIsometric σ]
[TopologicalSpace B]
[NormedAddCommGroup F₁]
[NormedSpace 𝕜₁ F₁]
[NormedAddCommGroup F₂]
[NormedSpace 𝕜₂ F₂]
{E₁ : B → Type u_6}
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜₁ (E₁ x)]
[(x : B) → TopologicalSpace (E₁ x)]
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜₂ (E₂ x)]
[(x : B) → TopologicalSpace (E₂ x)]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜₁ F₁ E₁]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜₂ F₂ E₂]
{ϕ : (x : B) → E₁ x →SL[σ] E₂ x}
{c : B → F₁ →SL[σ] F₂}
(hϕ :
∀ (a x : B),
x ∈ (trivializationAt F₁ E₁ a).baseSet →
x ∈ (trivializationAt F₂ E₂ a).baseSet → ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ a x a x (ϕ x) = c a)
:
Continuous fun (x : B) => Bundle.TotalSpace.mk' (F₁ →SL[σ] F₂) x (ϕ x)
A section of the σ-semilinear Hom bundle is continuous whenever its coordinate expression in
each preferred frame pair is locally constant around the frame centre. Topological counterpart of
TauCeti.contMDiff_hom_bundle_of_inCoordinates_eq_const.