The vector bundle of continuous (semi)linear maps

We define the (topological) vector bundle of continuous (semi)linear maps between two vector bundles over the same base.

Given bundles E₁ E₂ : B → Type*, normed spaces F₁ and F₂, and a ring-homomorphism σ between their respective scalar fields, we define a vector bundle with fiber E₁ x →SL[σ] E₂ x. If the E₁ and E₂ are vector bundles with model fibers F₁ and F₂, then this will be a vector bundle with fiber F₁ →SL[σ] F₂.

The topology on the total space is constructed from the trivializations for E₁ and E₂ and the norm-topology on the model fiber F₁ →SL[𝕜] F₂ using the VectorPrebundle construction. This is a bit awkward because it introduces a dependence on the normed space structure of the model fibers, rather than just their topological vector space structure; it is not clear whether this is necessary.

Similar constructions should be possible (but are yet to be formalized) for tensor products of topological vector bundles, exterior algebras, and so on, where again the topology can be defined using a norm on the fiber model if this helps.

@[reducible, inline, deprecated "Use the plain bundle syntax `fun (b : B) ↦ E₁ b →SL[σ] E₂ b` or `fun (b : B) ↦ E₁ b →L[𝕜] E₂ b` instead" (since := "2025-06-12")]

abbrev Bundle.ContinuousLinearMap {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (E₁ : B → Type u_5) [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] (E₂ : B → Type u_7) [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → TopologicalSpace (E₂ x)] : B → Type (max u_7 u_5)

A reducible type synonym for the bundle of continuous (semi)linear maps.

Equations

• Bundle.ContinuousLinearMap σ E₁ E₂ x = (E₁ x →SL[σ] E₂ x)

def Pretrivialization.continuousLinearMapCoordChange {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] (e₁ e₁' : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ e₂' : Trivialization F₂ Bundle.TotalSpace.proj) [Trivialization.IsLinear 𝕜₁ e₁] [Trivialization.IsLinear 𝕜₁ e₁'] [Trivialization.IsLinear 𝕜₂ e₂] [Trivialization.IsLinear 𝕜₂ e₂'] (b : B) : (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂

Assume eᵢ and eᵢ' are trivializations of the bundles Eᵢ over base B with fiber Fᵢ (i ∈ {1,2}), then Pretrivialization.continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂' is the coordinate change function between the two induced (pre)trivializations Pretrivialization.continuousLinearMap σ e₁ e₂ and Pretrivialization.continuousLinearMap σ e₁' e₂' of the bundle of continuous linear maps.

Equations

• Pretrivialization.continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂' b = ↑((Trivialization.coordChangeL 𝕜₁ e₁' e₁ b).symm.arrowCongrSL (Trivialization.coordChangeL 𝕜₂ e₂ e₂' b))

theorem Pretrivialization.continuousOn_continuousLinearMapCoordChange {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] {e₁ e₁' : Trivialization F₁ Bundle.TotalSpace.proj} {e₂ e₂' : Trivialization F₂ Bundle.TotalSpace.proj} [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [RingHomIsometric σ] [VectorBundle 𝕜₁ F₁ E₁] [VectorBundle 𝕜₂ F₂ E₂] [MemTrivializationAtlas e₁] [MemTrivializationAtlas e₁'] [MemTrivializationAtlas e₂] [MemTrivializationAtlas e₂'] : ContinuousOn (continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂') (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

def Pretrivialization.continuousLinearMap {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [Trivialization.IsLinear 𝕜₁ e₁] [Trivialization.IsLinear 𝕜₂ e₂] : Pretrivialization (F₁ →SL[σ] F₂) Bundle.TotalSpace.proj

Given trivializations e₁, e₂ for vector bundles E₁, E₂ over a base B, Pretrivialization.continuousLinearMap σ e₁ e₂ is the induced pretrivialization for the continuous σ-semilinear maps from E₁ to E₂. That is, the map which will later become a trivialization, after the bundle of continuous semilinear maps is equipped with the right topological vector bundle structure.

Equations

• One or more equations did not get rendered due to their size.

instance Pretrivialization.continuousLinearMap.isLinear {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [Trivialization.IsLinear 𝕜₁ e₁] [Trivialization.IsLinear 𝕜₂ e₂] [∀ (x : B), ContinuousAdd (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] : Pretrivialization.IsLinear 𝕜₂ (continuousLinearMap σ e₁ e₂)

theorem Pretrivialization.continuousLinearMap_apply {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [Trivialization.IsLinear 𝕜₁ e₁] [Trivialization.IsLinear 𝕜₂ e₂] (p : Bundle.TotalSpace (F₁ →SL[σ] F₂) fun (x : B) => E₁ x →SL[σ] E₂ x) : ↑(continuousLinearMap σ e₁ e₂) p = (p.proj, (Trivialization.continuousLinearMapAt 𝕜₂ e₂ p.proj).comp (p.snd.comp (Trivialization.symmL 𝕜₁ e₁ p.proj)))

theorem Pretrivialization.continuousLinearMap_symm_apply {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [Trivialization.IsLinear 𝕜₁ e₁] [Trivialization.IsLinear 𝕜₂ e₂] (p : B × (F₁ →SL[σ] F₂)) : ↑(continuousLinearMap σ e₁ e₂).symm p = { proj := p.1, snd := (Trivialization.symmL 𝕜₂ e₂ p.1).comp (p.2.comp (Trivialization.continuousLinearMapAt 𝕜₁ e₁ p.1)) }

theorem Pretrivialization.continuousLinearMap_symm_apply' {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [Trivialization.IsLinear 𝕜₁ e₁] [Trivialization.IsLinear 𝕜₂ e₂] {b : B} (hb : b ∈ e₁.baseSet ∩ e₂.baseSet) (L : F₁ →SL[σ] F₂) : (continuousLinearMap σ e₁ e₂).symm b L = (Trivialization.symmL 𝕜₂ e₂ b).comp (L.comp (Trivialization.continuousLinearMapAt 𝕜₁ e₁ b))

theorem Pretrivialization.continuousLinearMapCoordChange_apply {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] (e₁ e₁' : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ e₂' : Trivialization F₂ Bundle.TotalSpace.proj) [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [Trivialization.IsLinear 𝕜₁ e₁] [Trivialization.IsLinear 𝕜₁ e₁'] [Trivialization.IsLinear 𝕜₂ e₂] [Trivialization.IsLinear 𝕜₂ e₂'] (b : B) (hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)) (L : F₁ →SL[σ] F₂) : (continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂' b) L = (↑(continuousLinearMap σ e₁' e₂') { proj := b, snd := (continuousLinearMap σ e₁ e₂).symm b L }).2

def Bundle.ContinuousLinearMap.vectorPrebundle {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (F₁ : Type u_4) [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] (E₁ : B → Type u_5) [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (TotalSpace F₁ E₁)] (F₂ : Type u_6) [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] (E₂ : B → Type u_7) [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (TotalSpace F₂ E₂)] [TopologicalSpace B] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [RingHomIsometric σ] : VectorPrebundle 𝕜₂ (F₁ →SL[σ] F₂) fun (x : B) => E₁ x →SL[σ] E₂ x

The continuous σ-semilinear maps between two topological vector bundles form a VectorPrebundle (this is an auxiliary construction for the VectorBundle instance, in which the pretrivializations are collated but no topology on the total space is yet provided).

Equations

• One or more equations did not get rendered due to their size.

instance Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (F₁ : Type u_4) [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] (E₁ : B → Type u_5) [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (TotalSpace F₁ E₁)] (F₂ : Type u_6) [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] (E₂ : B → Type u_7) [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (TotalSpace F₂ E₂)] [TopologicalSpace B] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [RingHomIsometric σ] : TopologicalSpace (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) => E₁ x →SL[σ] E₂ x)

Topology on the total space of the continuous σ-semilinear maps between two "normable" vector bundles over the same base.

Equations

• Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace σ F₁ E₁ F₂ E₂ = (Bundle.ContinuousLinearMap.vectorPrebundle σ F₁ E₁ F₂ E₂).totalSpaceTopology

instance Bundle.ContinuousLinearMap.fiberBundle {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (F₁ : Type u_4) [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] (E₁ : B → Type u_5) [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (TotalSpace F₁ E₁)] (F₂ : Type u_6) [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] (E₂ : B → Type u_7) [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (TotalSpace F₂ E₂)] [TopologicalSpace B] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [RingHomIsometric σ] : FiberBundle (F₁ →SL[σ] F₂) fun (x : B) => E₁ x →SL[σ] E₂ x

The continuous σ-semilinear maps between two vector bundles form a fiber bundle.

Equations

• Bundle.ContinuousLinearMap.fiberBundle σ F₁ E₁ F₂ E₂ = (Bundle.ContinuousLinearMap.vectorPrebundle σ F₁ E₁ F₂ E₂).toFiberBundle

instance Bundle.ContinuousLinearMap.vectorBundle {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (F₁ : Type u_4) [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] (E₁ : B → Type u_5) [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (TotalSpace F₁ E₁)] (F₂ : Type u_6) [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] (E₂ : B → Type u_7) [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (TotalSpace F₂ E₂)] [TopologicalSpace B] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [RingHomIsometric σ] : VectorBundle 𝕜₂ (F₁ →SL[σ] F₂) fun (x : B) => E₁ x →SL[σ] E₂ x

The continuous σ-semilinear maps between two vector bundles form a vector bundle.

def Trivialization.continuousLinearMap {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [RingHomIsometric σ] [he₁ : MemTrivializationAtlas e₁] [he₂ : MemTrivializationAtlas e₂] : Trivialization (F₁ →SL[σ] F₂) Bundle.TotalSpace.proj

Given trivializations e₁, e₂ in the atlas for vector bundles E₁, E₂ over a base B, the induced trivialization for the continuous σ-semilinear maps from E₁ to E₂, whose base set is e₁.baseSet ∩ e₂.baseSet.

Equations

• Trivialization.continuousLinearMap σ e₁ e₂ = (Bundle.ContinuousLinearMap.vectorPrebundle σ F₁ E₁ F₂ E₂).trivializationOfMemPretrivializationAtlas ⋯

instance Bundle.ContinuousLinearMap.memTrivializationAtlas {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (TotalSpace F₂ E₂)] [TopologicalSpace B] (e₁ : Trivialization F₁ TotalSpace.proj) (e₂ : Trivialization F₂ TotalSpace.proj) [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [RingHomIsometric σ] [he₁ : MemTrivializationAtlas e₁] [he₂ : MemTrivializationAtlas e₂] : MemTrivializationAtlas (Trivialization.continuousLinearMap σ e₁ e₂)

@[simp]

theorem Trivialization.baseSet_continuousLinearMap {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Trivialization F₂ Bundle.TotalSpace.proj} [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [RingHomIsometric σ] [he₁ : MemTrivializationAtlas e₁] [he₂ : MemTrivializationAtlas e₂] : (continuousLinearMap σ e₁ e₂).baseSet = e₁.baseSet ∩ e₂.baseSet

theorem Trivialization.continuousLinearMap_apply {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Trivialization F₂ Bundle.TotalSpace.proj} [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [RingHomIsometric σ] [he₁ : MemTrivializationAtlas e₁] [he₂ : MemTrivializationAtlas e₂] (p : Bundle.TotalSpace (F₁ →SL[σ] F₂) fun (x : B) => E₁ x →SL[σ] E₂ x) : ↑(continuousLinearMap σ e₁ e₂) p = (p.proj, (continuousLinearMapAt 𝕜₂ e₂ p.proj).comp (p.snd.comp (symmL 𝕜₁ e₁ p.proj)))

theorem hom_trivializationAt {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [RingHomIsometric σ] (x₀ : B) : trivializationAt (F₁ →SL[σ] F₂) (fun (x : B) => E₁ x →SL[σ] E₂ x) x₀ = Trivialization.continuousLinearMap σ (trivializationAt F₁ E₁ x₀) (trivializationAt F₂ E₂ x₀)

theorem hom_trivializationAt_apply {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [RingHomIsometric σ] (x₀ : B) (x : Bundle.TotalSpace (F₁ →SL[σ] F₂) fun (x : B) => E₁ x →SL[σ] E₂ x) : ↑(trivializationAt (F₁ →SL[σ] F₂) (fun (x : B) => E₁ x →SL[σ] E₂ x) x₀) x = (x.proj, ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ x₀ x.proj x₀ x.proj x.snd)

@[simp]

theorem hom_trivializationAt_source {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [RingHomIsometric σ] (x₀ : B) : (trivializationAt (F₁ →SL[σ] F₂) (fun (x : B) => E₁ x →SL[σ] E₂ x) x₀).source = Bundle.TotalSpace.proj ⁻¹' ((trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet)

@[simp]

theorem hom_trivializationAt_target {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [RingHomIsometric σ] (x₀ : B) : (trivializationAt (F₁ →SL[σ] F₂) (fun (x : B) => E₁ x →SL[σ] E₂ x) x₀).target = ((trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet) ×ˢ Set.univ

@[simp]

theorem hom_trivializationAt_baseSet {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [RingHomIsometric σ] (x₀ : B) : (trivializationAt (F₁ →SL[σ] F₂) (fun (x : B) => E₁ x →SL[σ] E₂ x) x₀).baseSet = (trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet

theorem continuousWithinAt_hom_bundle {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [RingHomIsometric σ] {M : Type u_8} [TopologicalSpace M] (f : M → Bundle.TotalSpace (F₁ →SL[σ] F₂) fun (x : B) => E₁ x →SL[σ] E₂ x) {s : Set M} {x₀ : M} : ContinuousWithinAt f s x₀ ↔ ContinuousWithinAt (fun (x : M) => (f x).proj) s x₀ ∧ ContinuousWithinAt (fun (x : M) => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd) s x₀

theorem continuousAt_hom_bundle {𝕜₁ : Type u_1} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [NontriviallyNormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [NormedAddCommGroup F₁] [NormedSpace 𝕜₁ F₁] {E₁ : B → Type u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [TopologicalSpace B] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [RingHomIsometric σ] {M : Type u_8} [TopologicalSpace M] (f : M → Bundle.TotalSpace (F₁ →SL[σ] F₂) fun (x : B) => E₁ x →SL[σ] E₂ x) {x₀ : M} : ContinuousAt f x₀ ↔ ContinuousAt (fun (x : M) => (f x).proj) x₀ ∧ ContinuousAt (fun (x : M) => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd) x₀

theorem ContinuousWithinAt.clm_apply_of_inCoordinates {𝕜 : Type u_8} {F₁ : Type u_9} {F₂ : Type u_10} {B₁ : Type u_11} {B₂ : Type u_12} {M : Type u_13} {E₁ : B₁ → Type u_14} {E₂ : B₂ → Type u_15} [NontriviallyNormedField 𝕜] [(x : B₁) → AddCommGroup (E₁ x)] [(x : B₁) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B₁) → TopologicalSpace (E₁ x)] [(x : B₂) → AddCommGroup (E₂ x)] [(x : B₂) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B₂) → TopologicalSpace (E₂ x)] [TopologicalSpace B₁] [TopologicalSpace B₂] [TopologicalSpace M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁} {b₂ : M → B₂} {m₀ : M} {ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)} {v : (m : M) → E₁ (b₁ m)} {s : Set M} (hϕ : ContinuousWithinAt (fun (m : M) => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) s m₀) (hv : ContinuousWithinAt (fun (m : M) => { proj := b₁ m, snd := v m }) s m₀) (hb₂ : ContinuousWithinAt b₂ s m₀) : ContinuousWithinAt (fun (m : M) => { proj := b₂ m, snd := (ϕ m) (v m) }) s m₀

Consider a continuous map v : M → E₁ to a vector bundle, over a base map b₁ : M → B₁, and another basemap b₂ : M → B₂. Given linear maps ϕ m : E₁ (b₁ m) → E₂ (b₂ m) depending continuously on m, one can apply ϕ m to g m, and the resulting map is continuous.

Note that the continuity of ϕ can not be always be stated as continuity of a map into a bundle, as the pullback bundles b₁ *ᵖ E₁ and b₂ *ᵖ E₂ only have a nice topology when b₁ and b₂ are globally continuous, but we want to apply this lemma with only local information. Therefore, we formulate it using continuity of ϕ read in coordinates.

Version for ContinuousWithinAt. We also give a version for ContinuousAt, but no version for ContinuousOn or Continuous as our assumption, written in coordinates, only makes sense around a point.

For a version with B₁ = B₂ and b₁ = b₂, in which continuity can be expressed without inCoordinates, see ContinuousWithinAt.clm_bundle_apply

theorem ContinuousAt.clm_apply_of_inCoordinates {𝕜 : Type u_8} {F₁ : Type u_9} {F₂ : Type u_10} {B₁ : Type u_11} {B₂ : Type u_12} {M : Type u_13} {E₁ : B₁ → Type u_14} {E₂ : B₂ → Type u_15} [NontriviallyNormedField 𝕜] [(x : B₁) → AddCommGroup (E₁ x)] [(x : B₁) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B₁) → TopologicalSpace (E₁ x)] [(x : B₂) → AddCommGroup (E₂ x)] [(x : B₂) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B₂) → TopologicalSpace (E₂ x)] [TopologicalSpace B₁] [TopologicalSpace B₂] [TopologicalSpace M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁} {b₂ : M → B₂} {m₀ : M} {ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)} {v : (m : M) → E₁ (b₁ m)} (hϕ : ContinuousAt (fun (m : M) => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀) (hv : ContinuousAt (fun (m : M) => { proj := b₁ m, snd := v m }) m₀) (hb₂ : ContinuousAt b₂ m₀) : ContinuousAt (fun (m : M) => { proj := b₂ m, snd := (ϕ m) (v m) }) m₀

Consider a continuous map v : M → E₁ to a vector bundle, over a base map b₁ : M → B₁, and another basemap b₂ : M → B₂. Given linear maps ϕ m : E₁ (b₁ m) → E₂ (b₂ m) depending continuously on m, one can apply ϕ m to g m, and the resulting map is continuous.

Note that the continuity of ϕ can not be always be stated as continuity of a map into a bundle, as the pullback bundles b₁ *ᵖ E₁ and b₂ *ᵖ E₂ only have a nice topology when b₁ and b₂ are globally continuous, but we want to apply this lemma with only local information. Therefore, we formulate it using continuity of ϕ read in coordinates.

Version for ContinuousAt. We also give a version for ContinuousWithinAt, but no version for ContinuousOn or Continuous as our assumption, written in coordinates, only makes sense around a point.

For a version with B₁ = B₂ and b₁ = b₂, in which continuity can be expressed without inCoordinates, see ContinuousWithinAt.clm_bundle_apply

theorem ContinuousWithinAt.clm_bundle_apply {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {M : Type u_13} [NontriviallyNormedField 𝕜] {E₁ : B → Type u_14} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_15} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] [TopologicalSpace B] [TopologicalSpace M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : (x : M) → E₁ (b x)} {s : Set M} {x : M} [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)} (hϕ : ContinuousWithinAt (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m)) s x) (hv : ContinuousWithinAt (fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m)) s x) : ContinuousWithinAt (fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) ((ϕ m) (v m))) s x

Consider a C^n map v : M → E₁ to a vector bundle, over a basemap b : M → B, and linear maps ϕ m : E₁ (b m) → E₂ (b m) depending smoothly on m. One can apply ϕ m to v m, and the resulting map is C^n.

theorem ContinuousAt.clm_bundle_apply {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {M : Type u_13} [NontriviallyNormedField 𝕜] {E₁ : B → Type u_14} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_15} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] [TopologicalSpace B] [TopologicalSpace M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : (x : M) → E₁ (b x)} {x : M} [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)} (hϕ : ContinuousAt (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m)) x) (hv : ContinuousAt (fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m)) x) : ContinuousAt (fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) ((ϕ m) (v m))) x

Consider a C^n map v : M → E₁ to a vector bundle, over a basemap b : M → B, and linear maps ϕ m : E₁ (b m) → E₂ (b m) depending smoothly on m. One can apply ϕ m to v m, and the resulting map is C^n.

theorem ContinuousOn.clm_bundle_apply {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {M : Type u_13} [NontriviallyNormedField 𝕜] {E₁ : B → Type u_14} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_15} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] [TopologicalSpace B] [TopologicalSpace M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : (x : M) → E₁ (b x)} {s : Set M} [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)} (hϕ : ContinuousOn (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m)) s) (hv : ContinuousOn (fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m)) s) : ContinuousOn (fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) ((ϕ m) (v m))) s

Consider a C^n map v : M → E₁ to a vector bundle, over a basemap b : M → B, and linear maps ϕ m : E₁ (b m) → E₂ (b m) depending smoothly on m. One can apply ϕ m to v m, and the resulting map is C^n.

theorem Continuous.clm_bundle_apply {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {M : Type u_13} [NontriviallyNormedField 𝕜] {E₁ : B → Type u_14} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_15} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] [TopologicalSpace B] [TopologicalSpace M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : (x : M) → E₁ (b x)} [∀ (x : B), IsTopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)} (hϕ : Continuous fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂) (b m) (ϕ m)) (hv : Continuous fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m)) : Continuous fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) ((ϕ m) (v m))

Consider a C^n map v : M → E₁ to a vector bundle, over a basemap b : M → B, and linear maps ϕ m : E₁ (b m) → E₂ (b m) depending smoothly on m. One can apply ϕ m to v m, and the resulting map is C^n.

theorem ContinuousWithinAt.clm_bundle_apply₂ {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {F₃ : Type u_12} {M : Type u_13} [NontriviallyNormedField 𝕜] {E₁ : B → Type u_14} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_15} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_16} [(x : B) → AddCommGroup (E₃ x)] [(x : B) → Module 𝕜 (E₃ x)] [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] [TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [(x : B) → TopologicalSpace (E₃ x)] [TopologicalSpace B] [TopologicalSpace M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] [FiberBundle F₃ E₃] [VectorBundle 𝕜 F₃ E₃] {b : M → B} {v : (x : M) → E₁ (b x)} {s : Set M} {x : M} [∀ (x : B), IsTopologicalAddGroup (E₃ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₃ x)] {ψ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x) →L[𝕜] E₃ (b x)} {w : (x : M) → E₂ (b x)} (hψ : ContinuousWithinAt (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (b m) (ψ m)) s x) (hv : ContinuousWithinAt (fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m)) s x) (hw : ContinuousWithinAt (fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) (w m)) s x) : ContinuousWithinAt (fun (m : M) => Bundle.TotalSpace.mk' F₃ (b m) (((ψ m) (v m)) (w m))) s x

Consider C^n maps v : M → E₁ and v : M → E₂ to vector bundles, over a basemap b : M → B, and bilinear maps ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m) depending smoothly on m. One can apply ψ m to v m and w m, and the resulting map is C^n.

theorem ContinuousAt.clm_bundle_apply₂ {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {F₃ : Type u_12} {M : Type u_13} [NontriviallyNormedField 𝕜] {E₁ : B → Type u_14} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_15} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_16} [(x : B) → AddCommGroup (E₃ x)] [(x : B) → Module 𝕜 (E₃ x)] [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] [TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [(x : B) → TopologicalSpace (E₃ x)] [TopologicalSpace B] [TopologicalSpace M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] [FiberBundle F₃ E₃] [VectorBundle 𝕜 F₃ E₃] {b : M → B} {v : (x : M) → E₁ (b x)} {x : M} [∀ (x : B), IsTopologicalAddGroup (E₃ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₃ x)] {ψ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x) →L[𝕜] E₃ (b x)} {w : (x : M) → E₂ (b x)} (hψ : ContinuousAt (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (b m) (ψ m)) x) (hv : ContinuousAt (fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m)) x) (hw : ContinuousAt (fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) (w m)) x) : ContinuousAt (fun (m : M) => Bundle.TotalSpace.mk' F₃ (b m) (((ψ m) (v m)) (w m))) x

Consider C^n maps v : M → E₁ and v : M → E₂ to vector bundles, over a basemap b : M → B, and bilinear maps ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m) depending smoothly on m. One can apply ψ m to v m and w m, and the resulting map is C^n.

theorem ContinuousOn.clm_bundle_apply₂ {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {F₃ : Type u_12} {M : Type u_13} [NontriviallyNormedField 𝕜] {E₁ : B → Type u_14} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_15} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_16} [(x : B) → AddCommGroup (E₃ x)] [(x : B) → Module 𝕜 (E₃ x)] [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] [TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [(x : B) → TopologicalSpace (E₃ x)] [TopologicalSpace B] [TopologicalSpace M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] [FiberBundle F₃ E₃] [VectorBundle 𝕜 F₃ E₃] {b : M → B} {v : (x : M) → E₁ (b x)} {s : Set M} [∀ (x : B), IsTopologicalAddGroup (E₃ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₃ x)] {ψ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x) →L[𝕜] E₃ (b x)} {w : (x : M) → E₂ (b x)} (hψ : ContinuousOn (fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (b m) (ψ m)) s) (hv : ContinuousOn (fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m)) s) (hw : ContinuousOn (fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) (w m)) s) : ContinuousOn (fun (m : M) => Bundle.TotalSpace.mk' F₃ (b m) (((ψ m) (v m)) (w m))) s

Consider C^n maps v : M → E₁ and v : M → E₂ to vector bundles, over a basemap b : M → B, and bilinear maps ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m) depending smoothly on m. One can apply ψ m to v m and w m, and the resulting map is C^n.

theorem Continuous.clm_bundle_apply₂ {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {F₃ : Type u_12} {M : Type u_13} [NontriviallyNormedField 𝕜] {E₁ : B → Type u_14} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_15} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_16} [(x : B) → AddCommGroup (E₃ x)] [(x : B) → Module 𝕜 (E₃ x)] [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] [TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [(x : B) → TopologicalSpace (E₃ x)] [TopologicalSpace B] [TopologicalSpace M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] [FiberBundle F₃ E₃] [VectorBundle 𝕜 F₃ E₃] {b : M → B} {v : (x : M) → E₁ (b x)} [∀ (x : B), IsTopologicalAddGroup (E₃ x)] [∀ (x : B), ContinuousSMul 𝕜 (E₃ x)] {ψ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x) →L[𝕜] E₃ (b x)} {w : (x : M) → E₂ (b x)} (hψ : Continuous fun (m : M) => Bundle.TotalSpace.mk' (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (b m) (ψ m)) (hv : Continuous fun (m : M) => Bundle.TotalSpace.mk' F₁ (b m) (v m)) (hw : Continuous fun (m : M) => Bundle.TotalSpace.mk' F₂ (b m) (w m)) : Continuous fun (m : M) => Bundle.TotalSpace.mk' F₃ (b m) (((ψ m) (v m)) (w m))

Consider C^n maps v : M → E₁ and v : M → E₂ to vector bundles, over a basemap b : M → B, and bilinear maps ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m) depending smoothly on m. One can apply ψ m to v m and w m, and the resulting map is C^n.

theorem inCoordinates_apply_eq₂ {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {F₃ : Type u_12} [NontriviallyNormedField 𝕜] {E₁ : B → Type u_14} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_15} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_16} [(x : B) → AddCommGroup (E₃ x)] [(x : B) → Module 𝕜 (E₃ x)] [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] [TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [(x : B) → TopologicalSpace (E₃ x)] [TopologicalSpace B] [FiberBundle F₁ E₁] [VectorBundle 𝕜 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₀ x : B} {ϕ : E₁ x →L[𝕜] E₂ x →L[𝕜] E₃ x} {v : F₁} {w : F₂} (h₁x : x ∈ (trivializationAt F₁ E₁ x₀).baseSet) (h₂x : x ∈ (trivializationAt F₂ E₂ x₀).baseSet) (h₃x : x ∈ (trivializationAt F₃ E₃ x₀).baseSet) : ((ContinuousLinearMap.inCoordinates F₁ E₁ (F₂ →L[𝕜] F₃) (fun (x : B) => E₂ x →L[𝕜] E₃ x) x₀ x x₀ x ϕ) v) w = (Trivialization.linearMapAt 𝕜 (trivializationAt F₃ E₃ x₀) x) ((ϕ ((trivializationAt F₁ E₁ x₀).symm x v)) ((trivializationAt F₂ E₂ x₀).symm x w))

Rewrite ContinuousLinearMap.inCoordinates using continuous linear equivalences, in the bundle of bilinear maps.