Symmetry of a section of bilinear forms

Stream: new members

[Dominic Steinitz]

I've put this in "new members" as I feel it still is that sort of question.

I have a (local) section of bilinear forms (which I can prove to be smooth) and I want prove that it is symmetric. This is as minimal as I could make it. I have tried various unfolding and simp but that doesn't seem to get me anywhere. Any pointers would be very welcome.

import Mathlib.Geometry.Manifold.VectorBundle.Riemannian
import Mathlib.Geometry.Manifold.PartitionOfUnity
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Geometry.Manifold.VectorBundle.Tangent
import Mathlib.Geometry.Manifold.MFDeriv.Atlas
import Mathlib.Topology.Algebra.Module.Equiv
import Mathlib.Geometry.Manifold.ContMDiffMFDeriv

set_option linter.unusedSectionVars false
set_option synthInstance.maxHeartbeats 100000

open Bundle ContDiff Manifold

variable
  {EB : Type*} [NormedAddCommGroup EB] [InnerProductSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]
  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
  {E : B → Type*} [TopologicalSpace (TotalSpace F E)]
  [∀ x, TopologicalSpace (E x)] [∀ x, AddCommGroup (E x)] [∀ x, Module ℝ (E x)]
  [FiberBundle F E] [VectorBundle ℝ F E]
  [IsManifold IB ω B] [ContMDiffVectorBundle ω F E IB]

variable [FiniteDimensional ℝ EB] [IsManifold IB ω B] [SigmaCompactSpace B] [T2Space B]

lemma baseSet_eq_extChartAt_source (i : B) :
    (FiberBundle.trivializationAt (EB →L[ℝ] EB →L[ℝ] ℝ)
      (fun b ↦ TangentSpace IB b →L[ℝ] TangentSpace IB b →L[ℝ] ℝ) i).baseSet =
    (extChartAt IB i).source := by
  simp

noncomputable
def innerAtP_const (i : B) : EB →L[ℝ] EB →L[ℝ] ℝ := by
    let χ : Trivialization EB TotalSpace.proj :=
      FiberBundle.trivializationAt EB (fun (x : B) ↦ (TangentSpace IB x)) i
    have h1 :=
            χ.linear ℝ (mem_baseSet_trivializationAt EB (fun (x : B) ↦ (TangentSpace IB x)) i)
    let innerOnTangent : EB →L[ℝ] EB →L[ℝ] ℝ :=
    { toFun := fun u => {
      toFun := fun v => innerSL ℝ (χ ⟨i, u⟩).2 (χ ⟨i, v⟩).2,
      map_add' := by
          intro x y
          have h2 : (χ ⟨i, x + y⟩).2 = (χ ⟨i, x⟩).2 + (χ ⟨i, y⟩).2 := h1.map_add x y
          rw [h2]
          exact ContinuousLinearMap.map_add ((innerSL ℝ) (χ ⟨i, u⟩).2) (χ ⟨i, x⟩).2 (χ ⟨i, y⟩).2,
      map_smul' := by
        intro r x
        have h3 : (χ ⟨i, r • x⟩).2 = r • (χ ⟨i, x⟩).2 := h1.map_smul r x
        rw [h3]
        exact ContinuousLinearMap.map_smul _ _ _,
      cont := by
        have hi : i ∈ χ.baseSet := mem_baseSet_trivializationAt _ _ i
        have fiber_cont : Continuous (fun v : EB => (χ ⟨i, v⟩).2) :=
          (χ.continuousLinearEquivAt ℝ i hi).continuous
        exact ((innerSL ℝ) (χ ⟨i, u⟩).2).continuous.comp fiber_cont
      },
      map_add' := by
        intro x y
        ext v
        simp
        have h2 : (χ ⟨i, x + y⟩).2 = (χ ⟨i, x⟩).2 + (χ ⟨i, y⟩).2 := h1.map_add x y
        rw [h2]
        exact InnerProductSpace.add_left
          (χ { proj := i, snd := x }).2 (χ { proj := i, snd := y }).2 (χ { proj := i, snd := v }).2
      map_smul' := by
        intro r u
        ext v
        simp
        have h3 : (χ ⟨i, r • u⟩).2 = r • (χ ⟨i, u⟩).2 := h1.map_smul r u
        rw [h3]
        exact real_inner_smul_left (χ { proj := i, snd := u }).2 (χ { proj := i, snd := v }).2 r
      cont := by
        have hi : i ∈ χ.baseSet := mem_baseSet_trivializationAt _ _ i
        have fiber_cont : Continuous (fun u : EB => (χ ⟨i, u⟩).2) :=
          (χ.continuousLinearEquivAt ℝ i hi).continuous
        rw [continuous_clm_apply]
        simp
        intro v
        have : Continuous (fun u => innerSL ℝ (χ ⟨i, u⟩).2 (χ ⟨i, v⟩).2) := by
          have inner_cont : Continuous (fun w => innerSL ℝ w (χ ⟨i, v⟩).2) :=
            ((innerSL ℝ).flip (χ ⟨i, v⟩).2).continuous
          exact inner_cont.comp fiber_cont
        exact this
    }
    exact innerOnTangent

noncomputable
def g_bilin_ng (i b : B) :
 (TotalSpace (EB →L[ℝ] EB →L[ℝ] ℝ)
             (fun (x : B) ↦ TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ)) :=
  let ψ := FiberBundle.trivializationAt (EB →L[ℝ] EB →L[ℝ] ℝ)
    (fun (x : B) ↦ TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ) i
  ψ.invFun (b, innerAtP_const (EB := EB) (IB := IB) i)

-- I can do this
example (i p : B) (v w : TangentSpace IB p) :
  let χ : Trivialization EB TotalSpace.proj :=
    trivializationAt EB (fun x : B ↦ TangentSpace IB x) i
  (p, Inner.inner ℝ (χ { proj := p, snd := v }).2 (χ { proj := p, snd := w }).2) =
  (p, Inner.inner ℝ (χ { proj := p, snd := w }).2 (χ { proj := p, snd := v }).2) := by
    simp [real_inner_comm]

-- But how can this be done?
example (i p : B) (v w : TangentSpace IB p) :
  ((g_bilin_ng i p).snd.toFun v) w =
  ((g_bilin_ng i p).snd.toFun w) v := by
  have h3 : (((trivializationAt (EB →L[ℝ] EB →L[ℝ] ℝ)
              (fun x ↦ TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ) i).toPartialEquiv.symm
                (p, innerAtP_const (IB := IB) i)).snd v) w =
            (((trivializationAt (EB →L[ℝ] EB →L[ℝ] ℝ)
              (fun x ↦ TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ) i).toPartialEquiv.symm
                (p, innerAtP_const (IB := IB) i)).snd w) v := by
    exact sorry
  exact h3

[Eric Wieser]

Without answering your question, you should replace .toFun with and .invFun with .symm to remove some of the pain

[Sébastien Gouëzel]

Can you explain (with words, not Lean) what each of your objects is supposed to be mathematically?

[Sébastien Gouëzel]

(If I have an advice to give, it would be: don't build a metric on the tangent bundle, build a metric on a general vector bundle. It will be easier because you won't be distracted by the specificities of the tangent bundle, and you will have to focus on what is relevant)

[Sébastien Gouëzel]

(The key lemma for you, relating how things apply in the bilinear bundle and in the coordinates, is probably docs#inCoordinates_apply_eq₂)

[Dominic Steinitz]

Sébastien Gouëzel said:

Can you explain (with words, not Lean) what each of your objects is supposed to be mathematically?

The background to this is proving the existence of a Riemannian metric by using a partition of unity on local sections. So locally produce a bilinear form with the right properties by pushing forward vectors in the tangent bundle, applying the inner product in $\mathbb{R}$ and then pulling back to the vector bundle of bilinear forms. So $i$ is the index for the partition of unity and innerAtP_const creates a bilinear form in the target of the trivialisation. g_bilin_ng then pulls that back into the vector bundle itself. This construction is smooth (the Lean checks). All (pause for laughter) that remains is to prove symmetry and positive definiteness locally as I already have the Lean for the global section via the PoU.

Let me know if I missed anything.

[Dominic Steinitz]

Sébastien Gouëzel said:

(If I have an advice to give, it would be: don't build a metric on the tangent bundle, build a metric on a general vector bundle. It will be easier because you won't be distracted by the specificities of the tangent bundle, and you will have to focus on what is relevant)

I wanted to stay on familiar mathematical ground before attempting anything more abstract. My intention has always been to generalise thereafter.