Documentation

TauCeti.Geometry.Manifold.VectorBundle.Bilinear.Symmetric

The C^n bundle of symmetric bilinear maps #

For a C^n vector bundle V with model fibre F and a normed space G, the topological vector bundle fun x ↦ symmetricBilinearMaps π•œ (V x) G of symmetric bilinear maps is a C^n vector bundle, provided two is invertible in π•œ. For G = ℝ and the tangent bundle this is the bundle SymΒ²(T*M) of symmetric covariant two-tensors.

Its coordinate changes are pullbacks of symmetric bilinear maps along the coordinate changes of V. Their regularity is read off through the ambient space of all bilinear maps: the inclusion of the symmetric subspace and the symmetrization b ↦ (b + bα΅€) / 2 are continuous linear maps, and the symmetrization is a retraction onto the symmetric subspace.

The same retraction compares the bundle with the ambient bundle of bilinear maps: a field of symmetric bilinear maps is C^n as a section of the symmetric bundle if and only if it is C^n as a section of the bundle of all bilinear maps. Consequently the C^n sections of the symmetric bundle are identified with the symmetric C^n bilinear sections, TauCeti.Manifold.symmetricBilinearSectionEquiv. Riemannian metrics are among the latter, as the positive-definite symmetric sections.

The C^n structure follows Mathlib's C^n bundle of continuous alternating maps, Mathlib.Geometry.Manifold.VectorBundle.ContinuousAlternatingMap, by SΓ©bastien GouΓ«zel.

Main results #

Regularity of the symmetric pullback #

source
theorem ContMDiffOn.symmetricBilinearMapsComp {π•œ : Type u_1} [NontriviallyNormedField π•œ] [NeZero 2] {EM : Type u_2} [NormedAddCommGroup EM] [NormedSpace π•œ EM] {HM : Type u_3} [TopologicalSpace HM] {IM : ModelWithCorners π•œ EM HM} {M : Type u_4} [TopologicalSpace M] [ChartedSpace HM M] {F : Type u_5} {F' : Type u_6} [NormedAddCommGroup F] [NormedSpace π•œ F] [NormedAddCommGroup F'] [NormedSpace π•œ F'] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} {P : M β†’ F' β†’L[π•œ] F} {s : Set M} (hP : ContMDiffOn IM (modelWithCornersSelf π•œ (F' β†’L[π•œ] F)) n P s) :
ContMDiffOn IM (modelWithCornersSelf π•œ (β†₯(TauCeti.symmetricBilinearMaps π•œ F G) β†’L[π•œ] β†₯(TauCeti.symmetricBilinearMaps π•œ F' G))) n (fun (x : M) => (P x).symmetricBilinearMapsComp) s

When two is invertible, symmetric pullback depends in a C^n way on the map it pulls back along.

The C^n vector bundle structure #

source
theorem Bundle.Pretrivialization.contMDiffOn_symmetricBilinearMapsCoordChange {π•œ : Type u_1} [NontriviallyNormedField π•œ] [NeZero 2] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace π•œ EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners π•œ EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] {V : B β†’ Type u_6} [(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_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} [ContMDiffVectorBundle n F V IB] (e e' : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] :
ContMDiffOn IB (modelWithCornersSelf π•œ (β†₯(TauCeti.symmetricBilinearMaps π•œ F G) β†’L[π•œ] β†₯(TauCeti.symmetricBilinearMaps π•œ F G))) n (symmetricBilinearMapsCoordChange π•œ G e e') (e.baseSet ∩ e'.baseSet)

The coordinate changes of the bundle of symmetric bilinear maps are C^n.

source
instance TauCeti.isContMDiff_symmetricBilinearMapsVectorPrebundle {π•œ : Type u_1} [NontriviallyNormedField π•œ] [NeZero 2] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace π•œ EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners π•œ EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] {V : B β†’ Type u_6} [(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_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} [ContMDiffVectorBundle n F V IB] :
VectorPrebundle.IsContMDiff IB (symmetricBilinearMapsVectorPrebundle π•œ F V G) n
source
instance ContMDiffVectorBundle.symmetricBilinearMaps {π•œ : Type u_1} [NontriviallyNormedField π•œ] [NeZero 2] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace π•œ EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners π•œ EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] {V : B β†’ Type u_6} [(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_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} [ContMDiffVectorBundle n F V IB] :
ContMDiffVectorBundle n (β†₯(TauCeti.symmetricBilinearMaps π•œ F G)) (fun (x : B) => β†₯(TauCeti.symmetricBilinearMaps π•œ (V x) G)) IB

When two is invertible, the symmetric bilinear maps on the fibres of a C^n vector bundle form a C^n vector bundle.

Comparison with the bundle of all bilinear maps #

source
theorem TauCeti.Manifold.contMDiffWithinAt_symmetricBilinearMaps_section_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace π•œ EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners π•œ EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] {V : B β†’ Type u_6} [(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_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} [NeZero 2] {b : (x : B) β†’ β†₯(symmetricBilinearMaps π•œ (V x) G)} {s : Set B} {xβ‚€ : B} :
ContMDiffWithinAt IB (IB.prod (modelWithCornersSelf π•œ β†₯(symmetricBilinearMaps π•œ F G))) n (fun (x : B) => ⟨x, b x⟩) s xβ‚€ ↔ ContMDiffWithinAt IB (IB.prod (modelWithCornersSelf π•œ (F β†’L[π•œ] F β†’L[π•œ] G))) n (fun (x : B) => ⟨x, ↑(b x)⟩) s xβ‚€

A field of symmetric bilinear maps is C^n as a section of the symmetric bundle exactly when it is C^n as a section of the bundle of all bilinear maps.

source
theorem TauCeti.Manifold.contMDiffAt_symmetricBilinearMaps_section_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace π•œ EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners π•œ EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] {V : B β†’ Type u_6} [(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_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} [NeZero 2] {b : (x : B) β†’ β†₯(symmetricBilinearMaps π•œ (V x) G)} {xβ‚€ : B} :
ContMDiffAt IB (IB.prod (modelWithCornersSelf π•œ β†₯(symmetricBilinearMaps π•œ F G))) n (fun (x : B) => ⟨x, b x⟩) xβ‚€ ↔ ContMDiffAt IB (IB.prod (modelWithCornersSelf π•œ (F β†’L[π•œ] F β†’L[π•œ] G))) n (fun (x : B) => ⟨x, ↑(b x)⟩) xβ‚€

A field of symmetric bilinear maps is C^n at a point as a section of the symmetric bundle exactly when it is as a section of the bundle of all bilinear maps.

source
theorem TauCeti.Manifold.contMDiff_symmetricBilinearMaps_section_iff {π•œ : Type u_1} [NontriviallyNormedField π•œ] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace π•œ EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners π•œ EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] {V : B β†’ Type u_6} [(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_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} [NeZero 2] {b : (x : B) β†’ β†₯(symmetricBilinearMaps π•œ (V x) G)} :
(ContMDiff IB (IB.prod (modelWithCornersSelf π•œ β†₯(symmetricBilinearMaps π•œ F G))) n fun (x : B) => ⟨x, b x⟩) ↔ ContMDiff IB (IB.prod (modelWithCornersSelf π•œ (F β†’L[π•œ] F β†’L[π•œ] G))) n fun (x : B) => ⟨x, ↑(b x)⟩

A field of symmetric bilinear maps is a C^n section of the symmetric bundle exactly when it is a C^n section of the bundle of all bilinear maps.

source
def TauCeti.Manifold.symmetricBilinearSectionEquiv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace π•œ EB] {HB : Type u_3} [TopologicalSpace HB] (IB : ModelWithCorners π•œ EB HB) {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] {V : B β†’ Type u_6} [(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_7} [NormedAddCommGroup G] [NormedSpace π•œ G] (n : WithTop β„•βˆž) [NeZero 2] :
(ContMDiffSection IB (β†₯(symmetricBilinearMaps π•œ F G)) n fun (x : B) => β†₯(symmetricBilinearMaps π•œ (V x) G)) ≃ₗ[π•œ] β†₯symmetricBilinearSections

The C^n sections of the bundle of symmetric bilinear maps are the symmetric C^n bilinear sections.

Instances For
    source
    @[simp]
    theorem TauCeti.Manifold.symmetricBilinearSectionEquiv_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace π•œ EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners π•œ EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] {V : B β†’ Type u_6} [(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_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} [NeZero 2] (Οƒ : ContMDiffSection IB (β†₯(symmetricBilinearMaps π•œ F G)) n fun (x : B) => β†₯(symmetricBilinearMaps π•œ (V x) G)) (x : B) :
    ↑((symmetricBilinearSectionEquiv IB n) Οƒ) x = ↑(Οƒ x)
    source
    @[simp]
    theorem TauCeti.Manifold.coe_symmetricBilinearSectionEquiv_symm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace π•œ EB] {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners π•œ EB HB} {B : Type u_4} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π•œ F] {V : B β†’ Type u_6} [(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_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} [NeZero 2] (Ξ² : β†₯symmetricBilinearSections) (x : B) :
    ↑(((symmetricBilinearSectionEquiv IB n).symm Ξ²) x) = ↑β x