The vector bundle of symmetric bilinear maps

Let V be a topological vector bundle with model fibre F over a normed field 𝕜, and let G be a normed space. The fibres symmetricBilinearMaps 𝕜 (V x) G of symmetric continuous bilinear maps V x → V x → G form a topological vector bundle with model fibre symmetricBilinearMaps 𝕜 F G. For G = ℝ and V the tangent bundle this is the bundle Sym²(T*M) of symmetric covariant two-tensors, the ambient bundle of Riemannian metrics.

Each trivialization e of V induces the trivialization e.symmetricBilinearMaps 𝕜 G, which reads a symmetric bilinear map in the coordinates of e, pulling both arguments back along e.symmL. The coordinate changes are the pullbacks along the coordinate changes of V. The topology on the total space is then constructed by Mathlib's VectorPrebundle machinery. The inclusion into the bundle of all bilinear maps is continuous on total spaces; in induced frames it is simply the continuous linear inclusion of the symmetric model fibre.

The construction follows Mathlib's bundle of continuous alternating maps, Mathlib.Topology.VectorBundle.ContinuousAlternatingMap, by Yury Kudryashov, Heather Macbeth and Floris van Doorn.

Main definitions

• Bundle.Pretrivialization.symmetricBilinearMaps: the pretrivialization induced by a trivialization of V.
• TauCeti.symmetricBilinearMapsVectorPrebundle: the vector prebundle structure.
• Bundle.Trivialization.symmetricBilinearMaps: the induced trivialization, in the atlas of the bundle of symmetric bilinear maps.

The instances FiberBundle and VectorBundle for fun x ↦ symmetricBilinearMaps 𝕜 (V x) G are registered.

Pretrivializations

noncomputable def Bundle.Pretrivialization.symmetricBilinearMapsCoordChange (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (TotalSpace F V)] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] (e e' : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] [Trivialization.IsLinear 𝕜 e'] (b : B) : ↥(TauCeti.symmetricBilinearMaps 𝕜 F G) →L[𝕜] ↥(TauCeti.symmetricBilinearMaps 𝕜 F G)

The coordinate change between the trivializations of the bundle of symmetric bilinear maps induced by trivializations e and e' of V: pullback along the coordinate change of V from e' to e.

theorem Bundle.Pretrivialization.symmetricBilinearMapsCoordChange_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (TotalSpace F V)] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] (e e' : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] [Trivialization.IsLinear 𝕜 e'] : symmetricBilinearMapsCoordChange 𝕜 G e e' = fun (b : B) => (↑(Trivialization.coordChangeL 𝕜 e' e b)).symmetricBilinearMapsComp

theorem Bundle.Pretrivialization.continuousOn_symmetricBilinearMapsCoordChange {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] [VectorBundle 𝕜 F V] (e e' : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] : ContinuousOn (symmetricBilinearMapsCoordChange 𝕜 G e e') (e.baseSet ∩ e'.baseSet)

noncomputable def Bundle.Pretrivialization.symmetricBilinearMaps (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] : Pretrivialization (↥(TauCeti.symmetricBilinearMaps 𝕜 F G)) TotalSpace.proj

A trivialization e of V induces a pretrivialization of the bundle of symmetric bilinear maps on V, reading each map in the coordinates of e.

instance Bundle.Pretrivialization.symmetricBilinearMaps.isLinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] {e : Trivialization F TotalSpace.proj} [Trivialization.IsLinear 𝕜 e] : Pretrivialization.IsLinear 𝕜 (symmetricBilinearMaps 𝕜 G e)

theorem Bundle.Pretrivialization.symmetricBilinearMaps_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] {e : Trivialization F TotalSpace.proj} [Trivialization.IsLinear 𝕜 e] (p : TotalSpace ↥(TauCeti.symmetricBilinearMaps 𝕜 F G) fun (x : B) => ↥(TauCeti.symmetricBilinearMaps 𝕜 (V x) G)) : ↑(symmetricBilinearMaps 𝕜 G e) p = (p.proj, (Trivialization.symmL 𝕜 e p.proj).symmetricBilinearMapsComp p.snd)

@[simp]

theorem Bundle.Pretrivialization.baseSet_symmetricBilinearMaps {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] {e : Trivialization F TotalSpace.proj} [Trivialization.IsLinear 𝕜 e] : (symmetricBilinearMaps 𝕜 G e).baseSet = e.baseSet

theorem Bundle.Pretrivialization.symmetricBilinearMaps_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] {e : Trivialization F TotalSpace.proj} [Trivialization.IsLinear 𝕜 e] {b : B} (hb : b ∈ e.baseSet) (β : ↥(TauCeti.symmetricBilinearMaps 𝕜 F G)) : (symmetricBilinearMaps 𝕜 G e).symm b β = (Trivialization.continuousLinearMapAt 𝕜 e b).symmetricBilinearMapsComp β

theorem Bundle.Pretrivialization.symmetricBilinearMapsCoordChange_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] {e : Trivialization F TotalSpace.proj} [Trivialization.IsLinear 𝕜 e] {e' : Trivialization F TotalSpace.proj} [Trivialization.IsLinear 𝕜 e'] {b : B} (hb : b ∈ e.baseSet ∩ e'.baseSet) (β : ↥(TauCeti.symmetricBilinearMaps 𝕜 F G)) : (symmetricBilinearMapsCoordChange 𝕜 G e e' b) β = (↑(symmetricBilinearMaps 𝕜 G e') { proj := b, snd := (symmetricBilinearMaps 𝕜 G e).symm b β }).2

The vector bundle structure

noncomputable def TauCeti.symmetricBilinearMapsVectorPrebundle (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] (F : Type u_3) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (V : B → Type u_4) [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] : VectorPrebundle 𝕜 ↥(symmetricBilinearMaps 𝕜 F G) fun (x : B) => ↥(symmetricBilinearMaps 𝕜 (V x) G)

The symmetric bilinear maps on the fibres of a vector bundle form a vector prebundle. This auxiliary structure collects the induced pretrivializations; it provides the topology of the total space.

theorem TauCeti.mem_pretrivializationAtlas_symmetricBilinearMapsVectorPrebundle {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {e' : Bundle.Pretrivialization (↥(symmetricBilinearMaps 𝕜 F G)) Bundle.TotalSpace.proj} : e' ∈ (symmetricBilinearMapsVectorPrebundle 𝕜 F V G).pretrivializationAtlas ↔ ∃ (e : Bundle.Trivialization F Bundle.TotalSpace.proj) (x : MemTrivializationAtlas e), e' = Bundle.Pretrivialization.symmetricBilinearMaps 𝕜 G e

The pretrivializations in the atlas of the bundle of symmetric bilinear maps are those induced by the trivializations in the atlas of V.

@[instance_reducible]

noncomputable instance TauCeti.instTopologicalSpaceTotalSpaceSymmetricBilinearMaps (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] (F : Type u_3) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (V : B → Type u_4) [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] : TopologicalSpace (Bundle.TotalSpace ↥(symmetricBilinearMaps 𝕜 F G) fun (x : B) => ↥(symmetricBilinearMaps 𝕜 (V x) G))

The topology on the total space of the bundle of symmetric bilinear maps.

@[instance_reducible]

noncomputable instance TauCeti.instFiberBundleSymmetricBilinearMaps (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] (F : Type u_3) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (V : B → Type u_4) [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] : FiberBundle ↥(symmetricBilinearMaps 𝕜 F G) fun (x : B) => ↥(symmetricBilinearMaps 𝕜 (V x) G)

The symmetric bilinear maps on the fibres of a vector bundle form a fibre bundle.

instance TauCeti.instVectorBundleSymmetricBilinearMaps (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] (F : Type u_3) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (V : B → Type u_4) [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] : VectorBundle 𝕜 ↥(symmetricBilinearMaps 𝕜 F G) fun (x : B) => ↥(symmetricBilinearMaps 𝕜 (V x) G)

The symmetric bilinear maps on the fibres of a vector bundle form a vector bundle.

Trivializations

noncomputable def Bundle.Trivialization.symmetricBilinearMaps (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] (e : Trivialization F TotalSpace.proj) [he : MemTrivializationAtlas e] : Trivialization (↥(TauCeti.symmetricBilinearMaps 𝕜 F G)) TotalSpace.proj

The trivialization of the bundle of symmetric bilinear maps induced by a trivialization e in the atlas of V, with base set e.baseSet.

instance Bundle.Trivialization.memTrivializationAtlas_symmetricBilinearMaps {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] (e : Trivialization F TotalSpace.proj) [he : MemTrivializationAtlas e] : MemTrivializationAtlas (symmetricBilinearMaps 𝕜 G e)

@[simp]

theorem Bundle.Trivialization.baseSet_symmetricBilinearMaps {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] (e : Trivialization F TotalSpace.proj) [he : MemTrivializationAtlas e] : (symmetricBilinearMaps 𝕜 G e).baseSet = e.baseSet

theorem Bundle.Trivialization.symmetricBilinearMaps_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] (e : Trivialization F TotalSpace.proj) [he : MemTrivializationAtlas e] (p : TotalSpace ↥(TauCeti.symmetricBilinearMaps 𝕜 F G) fun (x : B) => ↥(TauCeti.symmetricBilinearMaps 𝕜 (V x) G)) : ↑(symmetricBilinearMaps 𝕜 G e) p = (p.proj, (symmL 𝕜 e p.proj).symmetricBilinearMapsComp p.snd)

theorem Bundle.Trivialization.symmetricBilinearMaps_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (G : Type u_5) [NormedAddCommGroup G] [NormedSpace 𝕜 G] (e : Trivialization F TotalSpace.proj) [he : MemTrivializationAtlas e] {b : B} (hb : b ∈ e.baseSet) (β : ↥(TauCeti.symmetricBilinearMaps 𝕜 F G)) : (symmetricBilinearMaps 𝕜 G e).symm b β = (continuousLinearMapAt 𝕜 e b).symmetricBilinearMapsComp β

theorem TauCeti.trivializationAt_symmetricBilinearMaps {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (x₀ : B) : trivializationAt (↥(symmetricBilinearMaps 𝕜 F G)) (fun (x : B) => ↥(symmetricBilinearMaps 𝕜 (V x) G)) x₀ = Bundle.Trivialization.symmetricBilinearMaps 𝕜 G (trivializationAt F V x₀)

The chosen trivialization of the bundle of symmetric bilinear maps at x₀ is induced by the chosen trivialization of V at x₀.

theorem TauCeti.trivializationAt_symmetricBilinearMaps_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (x₀ : B) (p : Bundle.TotalSpace ↥(symmetricBilinearMaps 𝕜 F G) fun (x : B) => ↥(symmetricBilinearMaps 𝕜 (V x) G)) : ↑(trivializationAt (↥(symmetricBilinearMaps 𝕜 F G)) (fun (x : B) => ↥(symmetricBilinearMaps 𝕜 (V x) G)) x₀) p = (p.proj, (Bundle.Trivialization.symmL 𝕜 (trivializationAt F V x₀) p.proj).symmetricBilinearMapsComp p.snd)

@[simp]

theorem TauCeti.baseSet_trivializationAt_symmetricBilinearMaps {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (x₀ : B) : (trivializationAt (↥(symmetricBilinearMaps 𝕜 F G)) (fun (x : B) => ↥(symmetricBilinearMaps 𝕜 (V x) G)) x₀).baseSet = (trivializationAt F V x₀).baseSet

@[simp]

theorem TauCeti.source_trivializationAt_symmetricBilinearMaps {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (x₀ : B) : (trivializationAt (↥(symmetricBilinearMaps 𝕜 F G)) (fun (x : B) => ↥(symmetricBilinearMaps 𝕜 (V x) G)) x₀).source = Bundle.TotalSpace.proj ⁻¹' (trivializationAt F V x₀).baseSet

@[simp]

theorem TauCeti.target_trivializationAt_symmetricBilinearMaps {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (x₀ : B) : (trivializationAt (↥(symmetricBilinearMaps 𝕜 F G)) (fun (x : B) => ↥(symmetricBilinearMaps 𝕜 (V x) G)) x₀).target = (trivializationAt F V x₀).baseSet ×ˢ Set.univ

theorem TauCeti.coe_trivializationAt_symmetricBilinearMaps_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x₀ x : B} (hx : x ∈ (trivializationAt F V x₀).baseSet) (b : ↥(symmetricBilinearMaps 𝕜 (V x) G)) : ↑(↑(trivializationAt (↥(symmetricBilinearMaps 𝕜 F G)) (fun (x : B) => ↥(symmetricBilinearMaps 𝕜 (V x) G)) x₀) { proj := x, snd := b }).2 = (↑(trivializationAt (F →L[𝕜] F →L[𝕜] G) (fun (x : B) => V x →L[𝕜] V x →L[𝕜] G) x₀) { proj := x, snd := ↑b }).2

In the chosen trivializations, a symmetric bilinear map has the same coordinates in the symmetric bundle and in the bundle of all bilinear maps.

theorem TauCeti.continuous_totalSpace_coe_symmetricBilinearMaps {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_4} [(x : B) → AddCommGroup (V x)] [(x : B) → Module 𝕜 (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace 𝕜 G] : Continuous fun (p : Bundle.TotalSpace ↥(symmetricBilinearMaps 𝕜 F G) fun (x : B) => ↥(symmetricBilinearMaps 𝕜 (V x) G)) => Bundle.TotalSpace.mk' (F →L[𝕜] F →L[𝕜] G) p.proj ↑p.snd

The inclusion of symmetric bilinear maps into all bilinear maps is continuous on total spaces, including when the fibres have no chosen norms.