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 #
bundle.continuous_linear_map.topological_vector_bundle: continuous semilinear maps between vector bundles form a vector bundle.
@[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
- bundle.continuous_linear_map σ F₁ E₁ F₂ E₂ x = (E₁ x →SL[σ] E₂ x)
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
- bundle.continuous_linear_map.add_monoid_hom_class σ F₁ E₁ F₂ E₂ x = semilinear_map_class.add_monoid_hom_class (E₁ x →SL[σ] E₂ x)
@[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) :
add_comm_monoid (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂ x)
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
- bundle.continuous_linear_map.module σ F₁ E₁ F₂ E₂ x = continuous_linear_map.module
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) :
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
- topological_vector_bundle.pretrivialization.continuous_linear_map_coord_change σ e₁ e₁' e₂ e₂' b = ↑((e₁'.coord_change e₁ b).symm.arrow_congrSL (e₂.coord_change e₂' b))
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)] :
topological_vector_bundle.pretrivialization 𝕜₂ (F₁ →SL[σ] F₂) (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂)
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
- topological_vector_bundle.pretrivialization.continuous_linear_map σ e₁ e₂ = {to_fiber_bundle_pretrivialization := {to_local_equiv := {to_fun := λ (p : bundle.total_space (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂)), (p.fst, (e₂.continuous_linear_map_at p.fst).comp (continuous_linear_map.comp p.snd (e₁.symmL p.fst))), inv_fun := λ (p : B × (F₁ →SL[σ] F₂)), ⟨p.fst, (e₂.symmL p.fst).comp (p.snd.comp (e₁.continuous_linear_map_at p.fst))⟩, source := bundle.total_space.proj ⁻¹' (e₁.to_fiber_bundle_trivialization.base_set ∩ e₂.to_fiber_bundle_trivialization.base_set), target := (e₁.to_fiber_bundle_trivialization.base_set ∩ e₂.to_fiber_bundle_trivialization.base_set) ×ˢ set.univ, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_target := _, base_set := e₁.to_fiber_bundle_trivialization.base_set ∩ e₂.to_fiber_bundle_trivialization.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}, linear' := _}
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₂)) :
⇑(topological_vector_bundle.pretrivialization.continuous_linear_map σ e₁ e₂) p = (p.fst, (e₂.continuous_linear_map_at p.fst).comp (continuous_linear_map.comp p.snd (e₁.symmL p.fst)))
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₂)) :
⇑((topological_vector_bundle.pretrivialization.continuous_linear_map σ e₁ e₂).to_fiber_bundle_pretrivialization.to_local_equiv.symm) p = ⟨p.fst, (e₂.symmL p.fst).comp (p.snd.comp (e₁.continuous_linear_map_at p.fst))⟩
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₂) :
(topological_vector_bundle.pretrivialization.continuous_linear_map σ e₁ e₂).symm b L = (e₂.symmL b).comp (L.comp (e₁.continuous_linear_map_at b))
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₂) :
⇑(topological_vector_bundle.pretrivialization.continuous_linear_map_coord_change σ e₁ e₁' e₂ e₂' b) L = (⇑(topological_vector_bundle.pretrivialization.continuous_linear_map σ e₁' e₂') (bundle.total_space_mk b ((topological_vector_bundle.pretrivialization.continuous_linear_map σ e₁ e₂).symm b L))).snd
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
- bundle.continuous_linear_map.topological_vector_prebundle σ F₁ E₁ F₂ E₂ = {pretrivialization_atlas := set.image2 (λ (e₁ : topological_vector_bundle.trivialization 𝕜₁ F₁ E₁) (e₂ : topological_vector_bundle.trivialization 𝕜₂ F₂ E₂), topological_vector_bundle.pretrivialization.continuous_linear_map σ e₁ e₂) (topological_vector_bundle.trivialization_atlas 𝕜₁ F₁ E₁) (topological_vector_bundle.trivialization_atlas 𝕜₂ F₂ E₂), pretrivialization_at := λ (x : B), topological_vector_bundle.pretrivialization.continuous_linear_map σ (topological_vector_bundle.trivialization_at 𝕜₁ F₁ E₁ x) (topological_vector_bundle.trivialization_at 𝕜₂ F₂ E₂ x), mem_base_pretrivialization_at := _, pretrivialization_mem_atlas := _, exists_coord_change := _}
@[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) :
topological_space (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂ x)
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
- topological_vector_bundle.bundle.continuous_linear_map.topological_space σ F₁ E₁ F₂ E₂ x = (bundle.continuous_linear_map.topological_vector_prebundle σ F₁ E₁ F₂ E₂).fiber_topology x
@[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)] :
topological_space (bundle.total_space (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂))
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₂) :
topological_vector_bundle.trivialization 𝕜₂ (F₁ →SL[σ] F₂) (bundle.continuous_linear_map σ F₁ E₁ 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₂)) :
⇑(topological_vector_bundle.trivialization.continuous_linear_map σ e₁ e₂ he₁ he₂) p = (p.fst, (e₂.continuous_linear_map_at p.fst).comp (continuous_linear_map.comp p.snd (e₁.symmL p.fst)))