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.
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
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)
Equations
Equations
- bundle.continuous_linear_map.module σ F₁ E₁ F₂ E₂ x = continuous_linear_map.module
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))
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' := _}
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 := _}
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
Topology on the total space of the continuous σ
-semilinear_maps between two "normable" vector
bundles over the same base.
Equations
The continuous σ
-semilinear_maps between two vector bundles form a vector bundle.
Equations
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
.