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.continuous_linear_map σ F₁ E₁ F₂ E₂ x to be a
type synonym for λ 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 is constructed from the trivializations for E₁ and E₂ and the norm-topology on the
model fiber F₁ →SL[𝕜] F₂ using the vector_prebundle construction. This is a bit awkward because
it introduces a spurious (?) dependence on the normed space structure of the model fiber, rather
than just its topological vector space structure; this might be fixable now that we have
continuous_linear_map.strong_topology.
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.continuous_linear_map.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
- bundle.continuous_linear_map.inhabited
- bundle.continuous_linear_map.add_monoid_hom_class
- bundle.continuous_linear_map.add_comm_monoid
- bundle.continuous_linear_map.module
- bundle.continuous_linear_map.topological_space
- bundle.continuous_linear_map.fiber_bundle
- bundle.continuous_linear_map.vector_bundle
@[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
pretrivialization.continuous_linear_map_coord_change
{𝕜₁ : Type u_1}
[nontrivially_normed_field 𝕜₁]
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₂]
(σ : 𝕜₁ →+* 𝕜₂)
[iσ : ring_hom_isometric σ]
{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₁' : trivialization F₁ bundle.total_space.proj)
(e₂ e₂' : trivialization F₂ bundle.total_space.proj)
[trivialization.is_linear 𝕜₁ e₁]
[trivialization.is_linear 𝕜₁ e₁']
[trivialization.is_linear 𝕜₂ e₂]
[trivialization.is_linear 𝕜₂ e₂']
(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
- pretrivialization.continuous_linear_map_coord_change σ e₁ e₁' e₂ e₂' b = ↑((trivialization.coord_changeL 𝕜₁ e₁' e₁ b).symm.arrow_congrSL (trivialization.coord_changeL 𝕜₂ e₂ e₂' b))
theorem
pretrivialization.continuous_on_continuous_linear_map_coord_change
{𝕜₁ : Type u_1}
[nontrivially_normed_field 𝕜₁]
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₂]
{σ : 𝕜₁ →+* 𝕜₂}
[iσ : ring_hom_isometric σ]
{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₁' : trivialization F₁ bundle.total_space.proj}
{e₂ e₂' : trivialization F₂ bundle.total_space.proj}
[Π (x : B), topological_space (E₁ x)]
[fiber_bundle F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[vector_bundle 𝕜₁ F₁ E₁]
[vector_bundle 𝕜₂ F₂ E₂]
[mem_trivialization_atlas e₁]
[mem_trivialization_atlas e₁']
[mem_trivialization_atlas e₂]
[mem_trivialization_atlas e₂'] :
continuous_on (pretrivialization.continuous_linear_map_coord_change σ e₁ e₁' e₂ e₂') (e₁.base_set ∩ e₂.base_set ∩ (e₁'.base_set ∩ e₂'.base_set))
noncomputable
def
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₁ : trivialization F₁ bundle.total_space.proj)
(e₂ : trivialization F₂ bundle.total_space.proj)
[Π (x : B), topological_space (E₁ x)]
[fiber_bundle F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[trivialization.is_linear 𝕜₁ e₁]
[trivialization.is_linear 𝕜₂ 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
- pretrivialization.continuous_linear_map σ e₁ e₂ = {to_local_equiv := {to_fun := λ (p : bundle.total_space (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂)), (p.fst, (trivialization.continuous_linear_map_at 𝕜₂ e₂ p.fst).comp (continuous_linear_map.comp p.snd (trivialization.symmL 𝕜₁ e₁ p.fst))), inv_fun := λ (p : B × (F₁ →SL[σ] F₂)), ⟨p.fst, (trivialization.symmL 𝕜₂ e₂ p.fst).comp (p.snd.comp (trivialization.continuous_linear_map_at 𝕜₁ e₁ p.fst))⟩, source := bundle.total_space.proj ⁻¹' (e₁.base_set ∩ e₂.base_set), target := (e₁.base_set ∩ e₂.base_set) ×ˢ set.univ, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_target := _, base_set := e₁.base_set ∩ e₂.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
Instances for pretrivialization.continuous_linear_map
@[protected, instance]
def
pretrivialization.continuous_linear_map.is_linear
{𝕜₁ : 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₁ : trivialization F₁ bundle.total_space.proj)
(e₂ : trivialization F₂ bundle.total_space.proj)
[Π (x : B), topological_space (E₁ x)]
[fiber_bundle F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[trivialization.is_linear 𝕜₁ e₁]
[trivialization.is_linear 𝕜₂ e₂]
[∀ (x : B), has_continuous_add (E₂ x)]
[∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] :
theorem
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₁ : trivialization F₁ bundle.total_space.proj)
(e₂ : trivialization F₂ bundle.total_space.proj)
[Π (x : B), topological_space (E₁ x)]
[fiber_bundle F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[trivialization.is_linear 𝕜₁ e₁]
[trivialization.is_linear 𝕜₂ e₂]
(p : bundle.total_space (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂)) :
⇑(pretrivialization.continuous_linear_map σ e₁ e₂) p = (p.fst, (trivialization.continuous_linear_map_at 𝕜₂ e₂ p.fst).comp (continuous_linear_map.comp p.snd (trivialization.symmL 𝕜₁ e₁ p.fst)))
theorem
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₁ : trivialization F₁ bundle.total_space.proj)
(e₂ : trivialization F₂ bundle.total_space.proj)
[Π (x : B), topological_space (E₁ x)]
[fiber_bundle F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[trivialization.is_linear 𝕜₁ e₁]
[trivialization.is_linear 𝕜₂ e₂]
(p : B × (F₁ →SL[σ] F₂)) :
⇑((pretrivialization.continuous_linear_map σ e₁ e₂).to_local_equiv.symm) p = ⟨p.fst, (trivialization.symmL 𝕜₂ e₂ p.fst).comp (p.snd.comp (trivialization.continuous_linear_map_at 𝕜₁ e₁ p.fst))⟩
theorem
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₁ : trivialization F₁ bundle.total_space.proj)
(e₂ : trivialization F₂ bundle.total_space.proj)
[Π (x : B), topological_space (E₁ x)]
[fiber_bundle F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[trivialization.is_linear 𝕜₁ e₁]
[trivialization.is_linear 𝕜₂ e₂]
[∀ (x : B), has_continuous_add (E₂ x)]
{b : B}
(hb : b ∈ e₁.base_set ∩ e₂.base_set)
(L : F₁ →SL[σ] F₂) :
(pretrivialization.continuous_linear_map σ e₁ e₂).symm b L = (trivialization.symmL 𝕜₂ e₂ b).comp (L.comp (trivialization.continuous_linear_map_at 𝕜₁ e₁ b))
theorem
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₁' : trivialization F₁ bundle.total_space.proj)
(e₂ e₂' : trivialization F₂ bundle.total_space.proj)
[Π (x : B), topological_space (E₁ x)]
[fiber_bundle F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[trivialization.is_linear 𝕜₁ e₁]
[trivialization.is_linear 𝕜₁ e₁']
[trivialization.is_linear 𝕜₂ e₂]
[trivialization.is_linear 𝕜₂ e₂']
[∀ (x : B), has_continuous_add (E₂ x)]
[ring_hom_isometric σ]
(b : B)
(hb : b ∈ e₁.base_set ∩ e₂.base_set ∩ (e₁'.base_set ∩ e₂'.base_set))
(L : F₁ →SL[σ] F₂) :
⇑(pretrivialization.continuous_linear_map_coord_change σ e₁ e₁' e₂ e₂' b) L = (⇑(pretrivialization.continuous_linear_map σ e₁' e₂') (bundle.total_space_mk b ((pretrivialization.continuous_linear_map σ e₁ e₂).symm b L))).snd
noncomputable
def
bundle.continuous_linear_map.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)]
[fiber_bundle F₁ E₁]
[vector_bundle 𝕜₁ F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[vector_bundle 𝕜₂ F₂ E₂]
[∀ (x : B), has_continuous_add (E₂ x)]
[∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] :
vector_prebundle 𝕜₂ (F₁ →SL[σ] F₂) (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂)
The continuous σ-semilinear maps between two topological vector bundles form a
vector_prebundle (this is an auxiliary construction for the
vector_bundle instance, in which the pretrivializations are collated but no topology
on the total space is yet provided).
Equations
- bundle.continuous_linear_map.vector_prebundle σ F₁ E₁ F₂ E₂ = {pretrivialization_atlas := {e : pretrivialization (F₁ →SL[σ] F₂) bundle.total_space.proj | ∃ (e₁ : trivialization F₁ bundle.total_space.proj) (e₂ : trivialization F₂ bundle.total_space.proj) [_inst_23 : mem_trivialization_atlas e₁] [_inst_24 : mem_trivialization_atlas e₂], e = pretrivialization.continuous_linear_map σ e₁ e₂}, pretrivialization_linear' := _, pretrivialization_at := λ (x : B), pretrivialization.continuous_linear_map σ (fiber_bundle.trivialization_at F₁ E₁ x) (fiber_bundle.trivialization_at F₂ E₂ x), mem_base_pretrivialization_at := _, pretrivialization_mem_atlas := _, exists_coord_change := _}
@[protected, instance]
noncomputable
def
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)]
[fiber_bundle F₁ E₁]
[vector_bundle 𝕜₁ F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[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
- bundle.continuous_linear_map.topological_space σ F₁ E₁ F₂ E₂ x = (bundle.continuous_linear_map.vector_prebundle σ F₁ E₁ F₂ E₂).fiber_topology x
@[protected, instance]
noncomputable
def
bundle.continuous_linear_map.topological_space_total_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)]
[fiber_bundle F₁ E₁]
[vector_bundle 𝕜₁ F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[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
- bundle.continuous_linear_map.topological_space_total_space σ F₁ E₁ F₂ E₂ = (bundle.continuous_linear_map.vector_prebundle σ F₁ E₁ F₂ E₂).total_space_topology
@[protected, instance]
noncomputable
def
bundle.continuous_linear_map.fiber_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)]
[fiber_bundle F₁ E₁]
[vector_bundle 𝕜₁ F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[vector_bundle 𝕜₂ F₂ E₂]
[∀ (x : B), has_continuous_add (E₂ x)]
[∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] :
fiber_bundle (F₁ →SL[σ] F₂) (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂)
The continuous σ-semilinear_maps between two vector bundles form a fiber bundle.
Equations
- bundle.continuous_linear_map.fiber_bundle σ F₁ E₁ F₂ E₂ = (bundle.continuous_linear_map.vector_prebundle σ F₁ E₁ F₂ E₂).to_fiber_bundle
@[protected, instance]
def
bundle.continuous_linear_map.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)]
[fiber_bundle F₁ E₁]
[vector_bundle 𝕜₁ F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[vector_bundle 𝕜₂ F₂ E₂]
[∀ (x : B), has_continuous_add (E₂ x)]
[∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)] :
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.
noncomputable
def
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₁ : trivialization F₁ bundle.total_space.proj)
(e₂ : trivialization F₂ bundle.total_space.proj)
[ring_hom_isometric σ]
[Π (x : B), topological_space (E₁ x)]
[fiber_bundle F₁ E₁]
[vector_bundle 𝕜₁ F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[vector_bundle 𝕜₂ F₂ E₂]
[∀ (x : B), has_continuous_add (E₂ x)]
[∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)]
[he₁ : mem_trivialization_atlas e₁]
[he₂ : mem_trivialization_atlas e₂] :
trivialization (F₁ →SL[σ] F₂) bundle.total_space.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₁.base_set ∩ e₂.base_set.
Equations
Instances for trivialization.continuous_linear_map
@[protected, instance]
def
bundle.continuous_linear_map.mem_trivialization_atlas
{𝕜₁ : 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₁ : trivialization F₁ bundle.total_space.proj)
(e₂ : trivialization F₂ bundle.total_space.proj)
[ring_hom_isometric σ]
[Π (x : B), topological_space (E₁ x)]
[fiber_bundle F₁ E₁]
[vector_bundle 𝕜₁ F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[vector_bundle 𝕜₂ F₂ E₂]
[∀ (x : B), has_continuous_add (E₂ x)]
[∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)]
[he₁ : mem_trivialization_atlas e₁]
[he₂ : mem_trivialization_atlas e₂] :
@[simp]
theorem
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₁ : trivialization F₁ bundle.total_space.proj}
{e₂ : trivialization F₂ bundle.total_space.proj}
[ring_hom_isometric σ]
[Π (x : B), topological_space (E₁ x)]
[fiber_bundle F₁ E₁]
[vector_bundle 𝕜₁ F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[vector_bundle 𝕜₂ F₂ E₂]
[∀ (x : B), has_continuous_add (E₂ x)]
[∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)]
[he₁ : mem_trivialization_atlas e₁]
[he₂ : mem_trivialization_atlas e₂] :
theorem
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₁ : trivialization F₁ bundle.total_space.proj}
{e₂ : trivialization F₂ bundle.total_space.proj}
[ring_hom_isometric σ]
[Π (x : B), topological_space (E₁ x)]
[fiber_bundle F₁ E₁]
[vector_bundle 𝕜₁ F₁ E₁]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₂ E₂]
[vector_bundle 𝕜₂ F₂ E₂]
[∀ (x : B), has_continuous_add (E₂ x)]
[∀ (x : B), has_continuous_smul 𝕜₂ (E₂ x)]
[he₁ : mem_trivialization_atlas e₁]
[he₂ : mem_trivialization_atlas e₂]
(p : bundle.total_space (bundle.continuous_linear_map σ F₁ E₁ F₂ E₂)) :
⇑(trivialization.continuous_linear_map σ e₁ e₂) p = (p.fst, (trivialization.continuous_linear_map_at 𝕜₂ e₂ p.fst).comp (continuous_linear_map.comp p.snd (trivialization.symmL 𝕜₁ e₁ p.fst)))