Documentation

TauCeti.Geometry.Manifold.VectorBundle.Bilinear.Section

Symmetrization of C^n bilinear fields #

The transpose of a C^n bilinear field is C^n. When two is nonzero in the scalar field, averaging a field with its transpose defines a linear projection onto the symmetric C^n sections. Over the reals this provides a linear ambient space for C^n Riemannian metrics, without choosing an inner product on the original bundle fibres.

The construction uses Mathlib's ContMDiffSection of the iterated hom bundle. In bundle coordinates transposition is the fixed continuous linear isometry ContinuousLinearMap.flipβ‚—α΅’; in particular preservation of regularity is valid in boundary charts as well. No compactness or finite-dimensionality is needed. The fibres are topological vector spaces isomorphic to the normed model fibre and need not carry chosen norms.

source
@[reducible, inline]
abbrev TauCeti.Manifold.BilinearSection {π•œ : 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) [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] (G : Type u_7) [NormedAddCommGroup G] [NormedSpace π•œ G] (n : WithTop β„•βˆž) :
Type (max u_4 u_7 u_6)

C^n bilinear fields with values in a normed space on a vector bundle.

Instances For
    source
    theorem TauCeti.Manifold.contMDiffAt_flip_section {π•œ : 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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} [βˆ€ (x : B), IsNormableSpace π•œ (V x)] {b : (x : B) β†’ V x β†’L[π•œ] V x β†’L[π•œ] G} {x : B} (hb : ContMDiffAt IB (IB.prod (modelWithCornersSelf π•œ (F β†’L[π•œ] F β†’L[π•œ] G))) n (fun (y : B) => ⟨y, b y⟩) x) :
    ContMDiffAt IB (IB.prod (modelWithCornersSelf π•œ (F β†’L[π•œ] F β†’L[π•œ] G))) n (fun (y : B) => ⟨y, (b y).flip⟩) x

    Fibrewise flip preserves C^n regularity at a point.

    source
    theorem TauCeti.Manifold.contMDiff_flip_section {π•œ : 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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} [βˆ€ (x : B), IsNormableSpace π•œ (V x)] {b : (x : B) β†’ V x β†’L[π•œ] V x β†’L[π•œ] G} (hb : ContMDiff IB (IB.prod (modelWithCornersSelf π•œ (F β†’L[π•œ] F β†’L[π•œ] G))) n fun (y : B) => ⟨y, b y⟩) :
    ContMDiff IB (IB.prod (modelWithCornersSelf π•œ (F β†’L[π•œ] F β†’L[π•œ] G))) n fun (x : B) => ⟨x, (b x).flip⟩

    Fibrewise flip preserves C^n regularity of a bilinear section.

    source
    noncomputable def TauCeti.Manifold.transposeBilinearSection {π•œ : 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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} :
    BilinearSection IB F V G n β†’β‚—[π•œ] BilinearSection IB F V G n

    Transposition as a linear involution on C^n bilinear fields.

    Instances For
      source
      @[simp]
      theorem TauCeti.Manifold.transposeBilinearSection_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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} (b : BilinearSection IB F V G n) (x : B) (v w : V x) :
      (((transposeBilinearSection b) x) v) w = ((b x) w) v
      source
      @[simp]
      theorem TauCeti.Manifold.transposeBilinearSection_transposeBilinearSection {π•œ : 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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} (b : BilinearSection IB F V G n) :
      transposeBilinearSection (transposeBilinearSection b) = b

      Transposing a C^n bilinear field twice recovers the original field.

      source
      noncomputable def TauCeti.Manifold.symmetricBilinearSections {π•œ : 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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} :
      Submodule π•œ (BilinearSection IB F V G n)

      The linear subspace of symmetric C^n bilinear fields.

      Instances For
        source
        @[simp]
        theorem TauCeti.Manifold.mem_symmetricBilinearSections {π•œ : 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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} (b : BilinearSection IB F V G n) :
        b ∈ symmetricBilinearSections ↔ βˆ€ (x : B) (v w : V x), ((b x) v) w = ((b x) w) v
        source
        @[simp]
        theorem TauCeti.Manifold.transposeBilinearSection_of_mem {π•œ : 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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} {b : BilinearSection IB F V G n} (hb : b ∈ symmetricBilinearSections) :
        transposeBilinearSection b = b

        Transposition fixes every symmetric section.

        source
        noncomputable def TauCeti.Manifold.symmetrizeBilinearSection {π•œ : 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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} :
        BilinearSection IB F V G n β†’β‚—[π•œ] BilinearSection IB F V G n

        The symmetrization projection b ↦ (b + bα΅€) / 2 on C^n bilinear fields.

        Instances For
          source
          @[simp]
          theorem TauCeti.Manifold.symmetrizeBilinearSection_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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} (b : BilinearSection IB F V G n) (x : B) (v w : V x) :
          (((symmetrizeBilinearSection b) x) v) w = 2⁻¹ β€’ (((b x) v) w + ((b x) w) v)
          source
          @[simp]
          theorem TauCeti.Manifold.symmetrizeBilinearSection_mem {π•œ : 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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} (b : BilinearSection IB F V G n) :
          symmetrizeBilinearSection b ∈ symmetricBilinearSections

          Symmetrization takes values in the symmetric sections.

          source
          @[simp]
          theorem TauCeti.Manifold.symmetrizeBilinearSection_eq_self_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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} [NeZero 2] (b : BilinearSection IB F V G n) :
          symmetrizeBilinearSection b = b ↔ b ∈ symmetricBilinearSections

          The fixed points of symmetrization are exactly the symmetric sections.

          source
          @[simp]
          theorem TauCeti.Manifold.symmetrizeBilinearSection_of_mem {π•œ : 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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} [NeZero 2] {b : BilinearSection IB F V G n} (hb : b ∈ symmetricBilinearSections) :
          symmetrizeBilinearSection b = b

          Symmetrization fixes every symmetric section.

          source
          theorem TauCeti.Manifold.isProj_symmetrizeBilinearSection {π•œ : 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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} [NeZero 2] :
          LinearMap.IsProj symmetricBilinearSections symmetrizeBilinearSection

          Symmetrization is a projection onto the submodule of symmetric sections.

          source
          theorem TauCeti.Manifold.range_symmetrizeBilinearSection {π•œ : 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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} [NeZero 2] :
          symmetrizeBilinearSection.range = symmetricBilinearSections

          Every symmetric C^n field is the symmetrization of a C^n bilinear field.

          source
          theorem ContMDiffAt.bilinearComp_bundle {π•œ : 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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] [βˆ€ (x : B), IsNormableSpace π•œ (V x)] {F' : Type u_7} [NormedAddCommGroup F'] [NormedSpace π•œ F'] {W : B β†’ Type u_8} [TopologicalSpace (Bundle.TotalSpace F' W)] [(x : B) β†’ TopologicalSpace (W x)] [(x : B) β†’ AddCommGroup (W x)] [(x : B) β†’ Module π•œ (W x)] [βˆ€ (x : B), IsTopologicalAddGroup (W x)] [βˆ€ (x : B), ContinuousSMul π•œ (W x)] [FiberBundle F' W] [VectorBundle π•œ F' W] [βˆ€ (x : B), IsNormableSpace π•œ (W x)] {G : Type u_9} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} {x : B} {Ξ² : (x : B) β†’ W x β†’L[π•œ] W x β†’L[π•œ] G} (hΞ² : ContMDiffAt IB (IB.prod (modelWithCornersSelf π•œ (F' β†’L[π•œ] F' β†’L[π•œ] G))) n (fun (x : B) => ⟨x, Ξ² x⟩) x) {A : (x : B) β†’ V x β†’L[π•œ] W x} (hA : ContMDiffAt IB (IB.prod (modelWithCornersSelf π•œ (F β†’L[π•œ] F'))) n (fun (x : B) => ⟨x, A x⟩) x) :
          ContMDiffAt IB (IB.prod (modelWithCornersSelf π•œ (F β†’L[π•œ] F β†’L[π•œ] G))) n (fun (x : B) => ⟨x, (Ξ² x).bilinearComp (A x) (A x)⟩) x

          Precomposing both arguments of a bilinear field on W that is C^n at x with a field of continuous linear maps V x β†’ W x that is C^n at x gives a bilinear field on V that is C^n at x.

          source
          theorem ContMDiff.bilinearComp_bundle {π•œ : 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} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) β†’ TopologicalSpace (V x)] [(x : B) β†’ AddCommGroup (V x)] [(x : B) β†’ Module π•œ (V x)] [FiberBundle F V] [VectorBundle π•œ F V] [βˆ€ (x : B), IsNormableSpace π•œ (V x)] {F' : Type u_7} [NormedAddCommGroup F'] [NormedSpace π•œ F'] {W : B β†’ Type u_8} [TopologicalSpace (Bundle.TotalSpace F' W)] [(x : B) β†’ TopologicalSpace (W x)] [(x : B) β†’ AddCommGroup (W x)] [(x : B) β†’ Module π•œ (W x)] [βˆ€ (x : B), IsTopologicalAddGroup (W x)] [βˆ€ (x : B), ContinuousSMul π•œ (W x)] [FiberBundle F' W] [VectorBundle π•œ F' W] [βˆ€ (x : B), IsNormableSpace π•œ (W x)] {G : Type u_9} [NormedAddCommGroup G] [NormedSpace π•œ G] {n : WithTop β„•βˆž} {Ξ² : (x : B) β†’ W x β†’L[π•œ] W x β†’L[π•œ] G} (hΞ² : ContMDiff IB (IB.prod (modelWithCornersSelf π•œ (F' β†’L[π•œ] F' β†’L[π•œ] G))) n fun (x : B) => ⟨x, Ξ² x⟩) {A : (x : B) β†’ V x β†’L[π•œ] W x} (hA : ContMDiff IB (IB.prod (modelWithCornersSelf π•œ (F β†’L[π•œ] F'))) n fun (x : B) => ⟨x, A x⟩) :
          ContMDiff IB (IB.prod (modelWithCornersSelf π•œ (F β†’L[π•œ] F β†’L[π•œ] G))) n fun (x : B) => ⟨x, (Ξ² x).bilinearComp (A x) (A x)⟩

          Precomposing both arguments of a C^n bilinear field on W with a C^n field of continuous linear maps V x β†’ W x gives a C^n bilinear field on V.