mathlib documentation

topology.vector_bundle.hom

The topological 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*, we define bundle.continuous_linear_map 𝕜 E₁ E₂ := λ x, E₁ x →SL[𝕜] E₂ x. If the E₁ and E₂ are topological vector bundles with fibers F₁ and F₂, then this will be a topological vector bundle with fiber F₁ →SL[𝕜] F₂. The topology is inherited from the norm-topology on, without the need to define the strong topology on continuous linear maps between general topological vector spaces.

Main Definitions #

@[protected, instance]
def bundle.continuous_linear_map.inhabited {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (F₁ : Type u_4) (E₁ : B → Type u_5) [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [Π (x : B), topological_space (E₁ x)] (F₂ : Type u_6) (E₂ : B → Type u_7) [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [Π (x : B), topological_space (E₂ x)] (x : B) :
inhabited (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂ x)
@[nolint]
def bundle.continuous_linear_map {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (F₁ : Type u_4) (E₁ : B → Type u_5) [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [Π (x : B), topological_space (E₁ x)] (F₂ : Type u_6) (E₂ : B → Type u_7) [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [Π (x : B), topological_space (E₂ x)] (x : B) :
Type (max u_5 u_7)

The bundle of continuous σ-semilinear maps between the topological vector bundles E₁ and E₂. This is a type synonym for λ x, E₁ x →SL[σ] E₂ x.

We intentionally add F₁ and F₂ as arguments to this type, so that instances on this type (that depend on F₁ and F₂) actually refer to F₁ and F₂.

Equations
Instances for bundle.continuous_linear_map
@[protected, instance]
def bundle.continuous_linear_map.add_monoid_hom_class {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (F₁ : Type u_4) (E₁ : B → Type u_5) [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [Π (x : B), topological_space (E₁ x)] (F₂ : Type u_6) (E₂ : B → Type u_7) [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [Π (x : B), topological_space (E₂ x)] (x : B) :
add_monoid_hom_class (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂ x) (E₁ x) (E₂ x)
Equations
@[protected, instance]
def bundle.continuous_linear_map.add_comm_monoid {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (F₁ : Type u_4) (E₁ : B → Type u_5) [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [Π (x : B), topological_space (E₁ x)] (F₂ : Type u_6) (E₂ : B → Type u_7) [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [Π (x : B), topological_space (E₂ x)] [∀ (x : B), has_continuous_add (E₂ x)] (x : B) :
Equations
@[protected, instance]
def bundle.continuous_linear_map.module {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (F₁ : Type u_4) (E₁ : B → Type u_5) [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [Π (x : B), topological_space (E₁ x)] (F₂ : Type u_6) (E₂ : B → Type u_7) [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [Π (x : B), topological_space (E₂ x)] [∀ (x : B), has_continuous_add (E₂ x)] [∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] (x : B) :
module 𝕜₂ (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂ x)
Equations
noncomputable def topological_vector_bundle.pretrivialization.continuous_linear_map_coord_change {𝕜₁ : Type u_1} [nontrivially_normed_field 𝕜₁] {𝕜₂ : Type u_2} [nontrivially_normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} [topological_space B] {F₁ : Type u_4} [normed_add_comm_group F₁] [normed_space 𝕜₁ F₁] {E₁ : B → Type u_5} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [topological_space (bundle.total_space E₁)] {F₂ : Type u_6} [normed_add_comm_group F₂] [normed_space 𝕜₂ F₂] {E₂ : B → Type u_7} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [topological_space (bundle.total_space E₂)] (e₁ e₁' : topological_vector_bundle.trivialization 𝕜₁ F₁ E₁) (e₂ e₂' : topological_vector_bundle.trivialization 𝕜₂ F₂ E₂) [ring_hom_isometric σ] (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 continuous_linear_map_coord_change σ e₁ e₁' e₂ e₂' is the coordinate change function between the two induced (pre)trivializations pretrivialization.continuous_linear_map σ e₁ e₂ and pretrivialization.continuous_linear_map σ e₁' e₂' of bundle.continuous_linear_map.

Equations
theorem topological_vector_bundle.pretrivialization.continuous_on_continuous_linear_map_coord_change {𝕜₁ : Type u_1} [nontrivially_normed_field 𝕜₁] {𝕜₂ : Type u_2} [nontrivially_normed_field 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {B : Type u_3} [topological_space B] {F₁ : Type u_4} [normed_add_comm_group F₁] [normed_space 𝕜₁ F₁] {E₁ : B → Type u_5} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [topological_space (bundle.total_space E₁)] {F₂ : Type u_6} [normed_add_comm_group F₂] [normed_space 𝕜₂ F₂] {E₂ : B → Type u_7} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [topological_space (bundle.total_space E₂)] {e₁ e₁' : topological_vector_bundle.trivialization 𝕜₁ F₁ E₁} {e₂ e₂' : topological_vector_bundle.trivialization 𝕜₂ F₂ E₂} [ring_hom_isometric σ] [Π (x : B), topological_space (E₁ x)] [topological_vector_bundle 𝕜₁ F₁ E₁] [Π (x : B), topological_space (E₂ x)] [topological_vector_bundle 𝕜₂ F₂ E₂] (he₁ : e₁ topological_vector_bundle.trivialization_atlas 𝕜₁ F₁ E₁) (he₁' : e₁' topological_vector_bundle.trivialization_atlas 𝕜₁ F₁ E₁) (he₂ : e₂ topological_vector_bundle.trivialization_atlas 𝕜₂ F₂ E₂) (he₂' : e₂' topological_vector_bundle.trivialization_atlas 𝕜₂ F₂ E₂) :
noncomputable def topological_vector_bundle.pretrivialization.continuous_linear_map {𝕜₁ : Type u_1} [nontrivially_normed_field 𝕜₁] {𝕜₂ : Type u_2} [nontrivially_normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} [topological_space B] {F₁ : Type u_4} [normed_add_comm_group F₁] [normed_space 𝕜₁ F₁] {E₁ : B → Type u_5} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [topological_space (bundle.total_space E₁)] {F₂ : Type u_6} [normed_add_comm_group F₂] [normed_space 𝕜₂ F₂] {E₂ : B → Type u_7} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [topological_space (bundle.total_space E₂)] (e₁ : topological_vector_bundle.trivialization 𝕜₁ F₁ E₁) (e₂ : topological_vector_bundle.trivialization 𝕜₂ F₂ E₂) [ring_hom_isometric σ] [Π (x : B), topological_space (E₁ x)] [topological_vector_bundle 𝕜₁ F₁ E₁] [Π (x : B), topological_space (E₂ x)] [topological_vector_bundle 𝕜₂ F₂ E₂] [∀ (x : B), has_continuous_add (E₂ x)] [∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] :

Given trivializations e₁, e₂ for vector bundles E₁, E₂ over a base B, pretrivialization.continuous_linear_map σ 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
theorem topological_vector_bundle.pretrivialization.continuous_linear_map_apply {𝕜₁ : Type u_1} [nontrivially_normed_field 𝕜₁] {𝕜₂ : Type u_2} [nontrivially_normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} [topological_space B] {F₁ : Type u_4} [normed_add_comm_group F₁] [normed_space 𝕜₁ F₁] {E₁ : B → Type u_5} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [topological_space (bundle.total_space E₁)] {F₂ : Type u_6} [normed_add_comm_group F₂] [normed_space 𝕜₂ F₂] {E₂ : B → Type u_7} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [topological_space (bundle.total_space E₂)] (e₁ : topological_vector_bundle.trivialization 𝕜₁ F₁ E₁) (e₂ : topological_vector_bundle.trivialization 𝕜₂ F₂ E₂) [ring_hom_isometric σ] [Π (x : B), topological_space (E₁ x)] [topological_vector_bundle 𝕜₁ F₁ E₁] [Π (x : B), topological_space (E₂ x)] [topological_vector_bundle 𝕜₂ F₂ E₂] [∀ (x : B), has_continuous_add (E₂ x)] [∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] (p : bundle.total_space (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂)) :
theorem topological_vector_bundle.pretrivialization.continuous_linear_map_symm_apply {𝕜₁ : Type u_1} [nontrivially_normed_field 𝕜₁] {𝕜₂ : Type u_2} [nontrivially_normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} [topological_space B] {F₁ : Type u_4} [normed_add_comm_group F₁] [normed_space 𝕜₁ F₁] {E₁ : B → Type u_5} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [topological_space (bundle.total_space E₁)] {F₂ : Type u_6} [normed_add_comm_group F₂] [normed_space 𝕜₂ F₂] {E₂ : B → Type u_7} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [topological_space (bundle.total_space E₂)] (e₁ : topological_vector_bundle.trivialization 𝕜₁ F₁ E₁) (e₂ : topological_vector_bundle.trivialization 𝕜₂ F₂ E₂) [ring_hom_isometric σ] [Π (x : B), topological_space (E₁ x)] [topological_vector_bundle 𝕜₁ F₁ E₁] [Π (x : B), topological_space (E₂ x)] [topological_vector_bundle 𝕜₂ F₂ E₂] [∀ (x : B), has_continuous_add (E₂ x)] [∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] (p : B × (F₁ →SL[σ] F₂)) :
theorem topological_vector_bundle.pretrivialization.continuous_linear_map_symm_apply' {𝕜₁ : Type u_1} [nontrivially_normed_field 𝕜₁] {𝕜₂ : Type u_2} [nontrivially_normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} [topological_space B] {F₁ : Type u_4} [normed_add_comm_group F₁] [normed_space 𝕜₁ F₁] {E₁ : B → Type u_5} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [topological_space (bundle.total_space E₁)] {F₂ : Type u_6} [normed_add_comm_group F₂] [normed_space 𝕜₂ F₂] {E₂ : B → Type u_7} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [topological_space (bundle.total_space E₂)] (e₁ : topological_vector_bundle.trivialization 𝕜₁ F₁ E₁) (e₂ : topological_vector_bundle.trivialization 𝕜₂ F₂ E₂) [ring_hom_isometric σ] [Π (x : B), topological_space (E₁ x)] [topological_vector_bundle 𝕜₁ F₁ E₁] [Π (x : B), topological_space (E₂ x)] [topological_vector_bundle 𝕜₂ F₂ E₂] [∀ (x : B), has_continuous_add (E₂ x)] [∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] {b : B} (hb : b e₁.to_fiber_bundle_trivialization.base_set e₂.to_fiber_bundle_trivialization.base_set) (L : F₁ →SL[σ] F₂) :
theorem topological_vector_bundle.pretrivialization.continuous_linear_map_coord_change_apply {𝕜₁ : Type u_1} [nontrivially_normed_field 𝕜₁] {𝕜₂ : Type u_2} [nontrivially_normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} [topological_space B] {F₁ : Type u_4} [normed_add_comm_group F₁] [normed_space 𝕜₁ F₁] {E₁ : B → Type u_5} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [topological_space (bundle.total_space E₁)] {F₂ : Type u_6} [normed_add_comm_group F₂] [normed_space 𝕜₂ F₂] {E₂ : B → Type u_7} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [topological_space (bundle.total_space E₂)] (e₁ e₁' : topological_vector_bundle.trivialization 𝕜₁ F₁ E₁) (e₂ e₂' : topological_vector_bundle.trivialization 𝕜₂ F₂ E₂) [ring_hom_isometric σ] [Π (x : B), topological_space (E₁ x)] [topological_vector_bundle 𝕜₁ F₁ E₁] [Π (x : B), topological_space (E₂ x)] [topological_vector_bundle 𝕜₂ F₂ E₂] [∀ (x : B), has_continuous_add (E₂ x)] [∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] (b : B) (hb : b e₁.to_fiber_bundle_trivialization.base_set e₂.to_fiber_bundle_trivialization.base_set (e₁'.to_fiber_bundle_trivialization.base_set e₂'.to_fiber_bundle_trivialization.base_set)) (L : F₁ →SL[σ] F₂) :
noncomputable def bundle.continuous_linear_map.topological_vector_prebundle {𝕜₁ : Type u_1} [nontrivially_normed_field 𝕜₁] {𝕜₂ : Type u_2} [nontrivially_normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} [topological_space B] (F₁ : Type u_4) [normed_add_comm_group F₁] [normed_space 𝕜₁ F₁] (E₁ : B → Type u_5) [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [topological_space (bundle.total_space E₁)] (F₂ : Type u_6) [normed_add_comm_group F₂] [normed_space 𝕜₂ F₂] (E₂ : B → Type u_7) [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [topological_space (bundle.total_space E₂)] [ring_hom_isometric σ] [Π (x : B), topological_space (E₁ x)] [topological_vector_bundle 𝕜₁ F₁ E₁] [Π (x : B), topological_space (E₂ x)] [topological_vector_bundle 𝕜₂ F₂ E₂] [∀ (x : B), has_continuous_add (E₂ x)] [∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] :
topological_vector_prebundle 𝕜₂ (F₁ →SL[σ] F₂) (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂)

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

Equations
@[protected, instance]
noncomputable def topological_vector_bundle.bundle.continuous_linear_map.topological_space {𝕜₁ : Type u_1} [nontrivially_normed_field 𝕜₁] {𝕜₂ : Type u_2} [nontrivially_normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} [topological_space B] (F₁ : Type u_4) [normed_add_comm_group F₁] [normed_space 𝕜₁ F₁] (E₁ : B → Type u_5) [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [topological_space (bundle.total_space E₁)] (F₂ : Type u_6) [normed_add_comm_group F₂] [normed_space 𝕜₂ F₂] (E₂ : B → Type u_7) [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [topological_space (bundle.total_space E₂)] [ring_hom_isometric σ] [Π (x : B), topological_space (E₁ x)] [topological_vector_bundle 𝕜₁ F₁ E₁] [Π (x : B), topological_space (E₂ x)] [topological_vector_bundle 𝕜₂ F₂ E₂] [∀ (x : B), has_continuous_add (E₂ x)] [∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] (x : B) :

Topology on the continuous σ-semilinear_maps between the respective fibers at a point of two "normable" vector bundles over the same base. Here "normable" means that the bundles have fibers modelled on normed spaces F₁, F₂ respectively. The topology we put on the continuous σ-semilinear_maps is the topology coming from the operator norm on maps from F₁ to F₂.

Equations
@[protected, instance]
noncomputable def topological_vector_bundle.bundle.total_space.topological_space {𝕜₁ : Type u_1} [nontrivially_normed_field 𝕜₁] {𝕜₂ : Type u_2} [nontrivially_normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} [topological_space B] (F₁ : Type u_4) [normed_add_comm_group F₁] [normed_space 𝕜₁ F₁] (E₁ : B → Type u_5) [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [topological_space (bundle.total_space E₁)] (F₂ : Type u_6) [normed_add_comm_group F₂] [normed_space 𝕜₂ F₂] (E₂ : B → Type u_7) [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [topological_space (bundle.total_space E₂)] [ring_hom_isometric σ] [Π (x : B), topological_space (E₁ x)] [topological_vector_bundle 𝕜₁ F₁ E₁] [Π (x : B), topological_space (E₂ x)] [topological_vector_bundle 𝕜₂ F₂ E₂] [∀ (x : B), has_continuous_add (E₂ x)] [∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] :

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

Equations
@[protected, instance]
noncomputable def bundle.continuous_linear_map.topological_vector_bundle {𝕜₁ : Type u_1} [nontrivially_normed_field 𝕜₁] {𝕜₂ : Type u_2} [nontrivially_normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} [topological_space B] (F₁ : Type u_4) [normed_add_comm_group F₁] [normed_space 𝕜₁ F₁] (E₁ : B → Type u_5) [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [topological_space (bundle.total_space E₁)] (F₂ : Type u_6) [normed_add_comm_group F₂] [normed_space 𝕜₂ F₂] (E₂ : B → Type u_7) [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [topological_space (bundle.total_space E₂)] [ring_hom_isometric σ] [Π (x : B), topological_space (E₁ x)] [topological_vector_bundle 𝕜₁ F₁ E₁] [Π (x : B), topological_space (E₂ x)] [topological_vector_bundle 𝕜₂ F₂ E₂] [∀ (x : B), has_continuous_add (E₂ x)] [∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] :
topological_vector_bundle 𝕜₂ (F₁ →SL[σ] F₂) (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂)

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

Equations
noncomputable def topological_vector_bundle.trivialization.continuous_linear_map {𝕜₁ : Type u_1} [nontrivially_normed_field 𝕜₁] {𝕜₂ : Type u_2} [nontrivially_normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} [topological_space B] {F₁ : Type u_4} [normed_add_comm_group F₁] [normed_space 𝕜₁ F₁] {E₁ : B → Type u_5} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [topological_space (bundle.total_space E₁)] {F₂ : Type u_6} [normed_add_comm_group F₂] [normed_space 𝕜₂ F₂] {E₂ : B → Type u_7} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [topological_space (bundle.total_space E₂)] (e₁ : topological_vector_bundle.trivialization 𝕜₁ F₁ E₁) (e₂ : topological_vector_bundle.trivialization 𝕜₂ F₂ E₂) [ring_hom_isometric σ] [Π (x : B), topological_space (E₁ x)] [topological_vector_bundle 𝕜₁ F₁ E₁] [Π (x : B), topological_space (E₂ x)] [topological_vector_bundle 𝕜₂ F₂ E₂] [∀ (x : B), has_continuous_add (E₂ x)] [∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] (he₁ : e₁ topological_vector_bundle.trivialization_atlas 𝕜₁ F₁ E₁) (he₂ : e₂ topological_vector_bundle.trivialization_atlas 𝕜₂ F₂ E₂) :

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₁.base_set ∩ e₂.base_set.

Equations
@[simp]
theorem topological_vector_bundle.trivialization.base_set_continuous_linear_map {𝕜₁ : Type u_1} [nontrivially_normed_field 𝕜₁] {𝕜₂ : Type u_2} [nontrivially_normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} [topological_space B] {F₁ : Type u_4} [normed_add_comm_group F₁] [normed_space 𝕜₁ F₁] {E₁ : B → Type u_5} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [topological_space (bundle.total_space E₁)] {F₂ : Type u_6} [normed_add_comm_group F₂] [normed_space 𝕜₂ F₂] {E₂ : B → Type u_7} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [topological_space (bundle.total_space E₂)] {e₁ : topological_vector_bundle.trivialization 𝕜₁ F₁ E₁} {e₂ : topological_vector_bundle.trivialization 𝕜₂ F₂ E₂} [ring_hom_isometric σ] [Π (x : B), topological_space (E₁ x)] [topological_vector_bundle 𝕜₁ F₁ E₁] [Π (x : B), topological_space (E₂ x)] [topological_vector_bundle 𝕜₂ F₂ E₂] [∀ (x : B), has_continuous_add (E₂ x)] [∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] (he₁ : e₁ topological_vector_bundle.trivialization_atlas 𝕜₁ F₁ E₁) (he₂ : e₂ topological_vector_bundle.trivialization_atlas 𝕜₂ F₂ E₂) :
theorem topological_vector_bundle.trivialization.continuous_linear_map_apply {𝕜₁ : Type u_1} [nontrivially_normed_field 𝕜₁] {𝕜₂ : Type u_2} [nontrivially_normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} [topological_space B] {F₁ : Type u_4} [normed_add_comm_group F₁] [normed_space 𝕜₁ F₁] {E₁ : B → Type u_5} [Π (x : B), add_comm_monoid (E₁ x)] [Π (x : B), module 𝕜₁ (E₁ x)] [topological_space (bundle.total_space E₁)] {F₂ : Type u_6} [normed_add_comm_group F₂] [normed_space 𝕜₂ F₂] {E₂ : B → Type u_7} [Π (x : B), add_comm_monoid (E₂ x)] [Π (x : B), module 𝕜₂ (E₂ x)] [topological_space (bundle.total_space E₂)] {e₁ : topological_vector_bundle.trivialization 𝕜₁ F₁ E₁} {e₂ : topological_vector_bundle.trivialization 𝕜₂ F₂ E₂} [ring_hom_isometric σ] [Π (x : B), topological_space (E₁ x)] [topological_vector_bundle 𝕜₁ F₁ E₁] [Π (x : B), topological_space (E₂ x)] [topological_vector_bundle 𝕜₂ F₂ E₂] [∀ (x : B), has_continuous_add (E₂ x)] [∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] (he₁ : e₁ topological_vector_bundle.trivialization_atlas 𝕜₁ F₁ E₁) (he₂ : e₂ topological_vector_bundle.trivialization_atlas 𝕜₂ F₂ E₂) (p : bundle.total_space (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂)) :