# 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 Bundle.ContinuousLinearMap σ F₁ E₁ F₂ E₂ x to be a type synonym for fun x ↦ 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.

## Main Definitions #

• Bundle.ContinuousLinearMap.vectorBundle: continuous semilinear maps between vector bundles form a vector bundle.
@[reducible, inline]
abbrev Bundle.ContinuousLinearMap {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (E₁ : BType u_5) [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] (E₂ : BType u_7) [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → TopologicalSpace (E₂ x)] :
BType (max u_7 u_5)

A reducible type synonym for the bundle of continuous (semi)linear maps. For some reason, it helps with instance search.

Porting note: after the port is done, we may want to remove this definition.

Equations
Instances For
instance Bundle.ContinuousLinearMap.module {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (E₁ : BType u_5) [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] (E₂ : BType u_7) [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → TopologicalSpace (E₂ x)] [∀ (x : B), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousConstSMul 𝕜₂ (E₂ x)] (x : B) :
Module 𝕜₂ (Bundle.ContinuousLinearMap σ E₁ E₂ x)
Equations
• = inferInstance
def Pretrivialization.continuousLinearMapCoordChange {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [] [NormedSpace 𝕜₁ F₁] {E₁ : BType u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] {F₂ : Type u_6} [] [NormedSpace 𝕜₂ F₂] {E₂ : BType u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₁' : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) (e₂' : Trivialization F₂ Bundle.TotalSpace.proj) [] [] [] [] (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 Bundle.ContinuousLinearMap.

Equations
Instances For
theorem Pretrivialization.continuousOn_continuousLinearMapCoordChange {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {σ : 𝕜₁ →+* 𝕜₂} {B : Type u_3} {F₁ : Type u_4} [] [NormedSpace 𝕜₁ F₁] {E₁ : BType u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] {F₂ : Type u_6} [] [NormedSpace 𝕜₂ F₂] {E₂ : BType u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {e₁' : Trivialization F₁ Bundle.TotalSpace.proj} {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₂] [] [VectorBundle 𝕜₁ F₁ E₁] [VectorBundle 𝕜₂ F₂ E₂] [] [] :
ContinuousOn (Pretrivialization.continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂') (e₁.baseSet e₂.baseSet (e₁'.baseSet e₂'.baseSet))
def Pretrivialization.continuousLinearMap {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [] [NormedSpace 𝕜₁ F₁] {E₁ : BType u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] {F₂ : Type u_6} [] [NormedSpace 𝕜₂ F₂] {E₂ : BType u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] (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₂] [] [] :
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.
Instances For
instance Pretrivialization.continuousLinearMap.isLinear {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [] [NormedSpace 𝕜₁ F₁] {E₁ : BType u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] {F₂ : Type u_6} [] [NormedSpace 𝕜₂ F₂] {E₂ : BType u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] (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₂] [] [] [∀ (x : B), ContinuousAdd (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] :
Equations
• =
theorem Pretrivialization.continuousLinearMap_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [] [NormedSpace 𝕜₁ F₁] {E₁ : BType u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] {F₂ : Type u_6} [] [NormedSpace 𝕜₂ F₂] {E₂ : BType u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] (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₂] [] [] (p : Bundle.TotalSpace (F₁ →SL[σ] F₂) fun (x : B) => E₁ x →SL[σ] E₂ x) :
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} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [] [NormedSpace 𝕜₁ F₁] {E₁ : BType u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] {F₂ : Type u_6} [] [NormedSpace 𝕜₂ F₂] {E₂ : BType u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] (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₂] [] [] (p : B × (F₁ →SL[σ] F₂)) :
.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} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [] [NormedSpace 𝕜₁ F₁] {E₁ : BType u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] {F₂ : Type u_6} [] [NormedSpace 𝕜₂ F₂] {E₂ : BType u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] (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₂] [] [] {b : B} (hb : b e₁.baseSet e₂.baseSet) (L : F₁ →SL[σ] F₂) :
.symm b L = (Trivialization.symmL 𝕜₂ e₂ b).comp (L.comp )
theorem Pretrivialization.continuousLinearMapCoordChange_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [] [NormedSpace 𝕜₁ F₁] {E₁ : BType u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] {F₂ : Type u_6} [] [NormedSpace 𝕜₂ F₂] {E₂ : BType u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₁' : Trivialization F₁ Bundle.TotalSpace.proj) (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₂] [] [] [] [] (b : B) (hb : b e₁.baseSet e₂.baseSet (e₁'.baseSet e₂'.baseSet)) (L : F₁ →SL[σ] F₂) :
(Pretrivialization.continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂' b) L = ( { proj := b, snd := .symm b L }).2
def Bundle.ContinuousLinearMap.vectorPrebundle {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (F₁ : Type u_4) [] [NormedSpace 𝕜₁ F₁] (E₁ : BType u_5) [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] (F₂ : Type u_6) [] [NormedSpace 𝕜₂ F₂] (E₂ : BType u_7) [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [] :
VectorPrebundle 𝕜₂ (F₁ →SL[σ] F₂) (Bundle.ContinuousLinearMap σ E₁ E₂)

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.
Instances For
instance Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (F₁ : Type u_4) [] [NormedSpace 𝕜₁ F₁] (E₁ : BType u_5) [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] (F₂ : Type u_6) [] [NormedSpace 𝕜₂ F₂] (E₂ : BType u_7) [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [] :

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

Equations
instance Bundle.ContinuousLinearMap.fiberBundle {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (F₁ : Type u_4) [] [NormedSpace 𝕜₁ F₁] (E₁ : BType u_5) [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] (F₂ : Type u_6) [] [NormedSpace 𝕜₂ F₂] (E₂ : BType u_7) [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [] :
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
instance Bundle.ContinuousLinearMap.vectorBundle {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (F₁ : Type u_4) [] [NormedSpace 𝕜₁ F₁] (E₁ : BType u_5) [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] (F₂ : Type u_6) [] [NormedSpace 𝕜₂ F₂] (E₂ : BType u_7) [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [] :
VectorBundle 𝕜₂ (F₁ →SL[σ] F₂) (Bundle.ContinuousLinearMap σ E₁ E₂)

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

Equations
• =
def Trivialization.continuousLinearMap {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [] [NormedSpace 𝕜₁ F₁] {E₁ : BType u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] {F₂ : Type u_6} [] [NormedSpace 𝕜₂ F₂] {E₂ : BType u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] (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), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [] [he₁ : ] [he₂ : ] :
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
Instances For
instance Bundle.ContinuousLinearMap.memTrivializationAtlas {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [] [NormedSpace 𝕜₁ F₁] {E₁ : BType u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] {F₂ : Type u_6} [] [NormedSpace 𝕜₂ F₂] {E₂ : BType u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] (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), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [] [he₁ : ] [he₂ : ] :
Equations
• =
@[simp]
theorem Trivialization.baseSet_continuousLinearMap {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [] [NormedSpace 𝕜₁ F₁] {E₁ : BType u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] {F₂ : Type u_6} [] [NormedSpace 𝕜₂ F₂] {E₂ : BType u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] {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), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [] [he₁ : ] [he₂ : ] :
.baseSet = e₁.baseSet e₂.baseSet
theorem Trivialization.continuousLinearMap_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [] [NormedSpace 𝕜₁ F₁] {E₁ : BType u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] {F₂ : Type u_6} [] [NormedSpace 𝕜₂ F₂] {E₂ : BType u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] {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), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [] [he₁ : ] [he₂ : ] (p : Bundle.TotalSpace (F₁ →SL[σ] F₂) (Bundle.ContinuousLinearMap σ E₁ E₂)) :
p = (p.proj, (Trivialization.continuousLinearMapAt 𝕜₂ e₂ p.proj).comp (ContinuousLinearMap.comp p.snd (Trivialization.symmL 𝕜₁ e₁ p.proj)))
theorem hom_trivializationAt_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [] [NormedSpace 𝕜₁ F₁] {E₁ : BType u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] {F₂ : Type u_6} [] [NormedSpace 𝕜₂ F₂] {E₂ : BType u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [] (x₀ : B) (x : Bundle.TotalSpace (F₁ →SL[σ] F₂) (Bundle.ContinuousLinearMap σ E₁ E₂)) :
(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} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [] [NormedSpace 𝕜₁ F₁] {E₁ : BType u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] {F₂ : Type u_6} [] [NormedSpace 𝕜₂ F₂] {E₂ : BType u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [] (x₀ : B) :
(trivializationAt (F₁ →SL[σ] F₂) (Bundle.ContinuousLinearMap σ E₁ E₂) x₀).source = Bundle.TotalSpace.proj ⁻¹' ((trivializationAt F₁ E₁ x₀).baseSet (trivializationAt F₂ E₂ x₀).baseSet)
@[simp]
theorem hom_trivializationAt_target {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [] [NormedSpace 𝕜₁ F₁] {E₁ : BType u_5} [(x : B) → AddCommGroup (E₁ x)] [(x : B) → Module 𝕜₁ (E₁ x)] [] {F₂ : Type u_6} [] [NormedSpace 𝕜₂ F₂] {E₂ : BType u_7} [(x : B) → AddCommGroup (E₂ x)] [(x : B) → Module 𝕜₂ (E₂ x)] [] [] [(x : B) → TopologicalSpace (E₁ x)] [FiberBundle F₁ E₁] [VectorBundle 𝕜₁ F₁ E₁] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₂ E₂] [VectorBundle 𝕜₂ F₂ E₂] [∀ (x : B), TopologicalAddGroup (E₂ x)] [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [] (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