Generalising Tangent Bundles to Vector Bundles

Stream: mathlib4

[Dominic Steinitz]

I have a proof for the existence of a Riemannian metric which works for tangent bundles (https://github.com/leanprover-community/mathlib4/pull/33714) and which I am trying to generalise.

For reasons I don't understand I have to cast and as far as I can see stops the specialised proof being generalised.

import Mathlib.Analysis.InnerProductSpace.LinearMap
import Mathlib.Geometry.Manifold.VectorBundle.Tangent
import Mathlib.Topology.VectorBundle.Hom

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] [InnerProductSpace ℝ F]
  {E : B → Type*} [TopologicalSpace (TotalSpace F E)]
  [∀ x, NormedAddCommGroup (E x)]
  [∀ x, NormedSpace ℝ (E x)]
  [FiberBundle F E] [VectorBundle ℝ F E]
  [IsManifold IB ω B] [ContMDiffVectorBundle ω F E IB]

variable [FiniteDimensional ℝ EB] [SigmaCompactSpace B] [T2Space B]
variable [FiniteDimensional ℝ F]

noncomputable instance : TopologicalSpace (TotalSpace EB (TangentSpace (M := B) IB)) :=
  inferInstanceAs (TopologicalSpace (TangentBundle IB B))

noncomputable instance (p : B) : NormedAddCommGroup (TangentSpace IB p) := by
  change NormedAddCommGroup EB
  infer_instance

noncomputable instance (p : B) : NormedSpace ℝ (TangentSpace IB p) := by
  change NormedSpace ℝ EB
  infer_instance

-- The general definition
noncomputable
def g_bilin_1g (i b : B) :
 (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ)
             (fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ)) := by
  let ψ := trivializationAt (F →L[ℝ] F →L[ℝ] ℝ)
      (fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) i
  by_cases h : (b, (fun (x : B) ↦ innerSL ℝ) b) ∈ ψ.target
  · exact ψ.invFun (b, (fun (x : B) ↦ innerSL ℝ) b)
  · exact ⟨b, 0⟩

-- Specialise to tangent spaces
noncomputable
def g_bilin_1 (i b : B) :
 (TotalSpace (EB →L[ℝ] EB →L[ℝ] ℝ)
             (fun (x : B) ↦ TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ)) :=
  g_bilin_1g i b

-- The other general definition
noncomputable
def g_bilin_2g (i p : B) : E p →L[ℝ] (E p →L[ℝ] ℝ) := by
  let χ := trivializationAt F E i
  by_cases h : p ∈ χ.baseSet
  · exact (innerSL ℝ).comp (χ.continuousLinearMapAt ℝ p) |>.flip.comp (χ.continuousLinearMapAt ℝ p)
  · exact 0

-- Also specialised to tangent spaces
noncomputable
def g_bilin_2 (i p : B) :
  (TangentSpace IB) p →L[ℝ]  ((TangentSpace IB) p →L[ℝ] ℝ) :=
  g_bilin_2g (F := EB) i p

-- This checks
lemma g_bilin_eqt (i b : B)
  (hha : (b, innerSL ℝ) ∈
        (trivializationAt (EB →L[ℝ] EB →L[ℝ] ℝ)
         (fun x ↦ TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ) i).target)
  (hhb : (b, innerSL (E := EB) ℝ) ∈
        ((chartAt HB i).source ∩ ((chartAt HB i).source ∩ Set.univ)) ×ˢ Set.univ)
  -- This is true for tangent spaces so we don't really need it as a hypothesis we could just use
  -- `TangentBundle.trivializationAt_baseSet` but there is no general version
  (hhz : ∀ x, (trivializationAt EB (TangentSpace IB) x).baseSet = (chartAt HB (M := B) x).source)
  (α β : TangentSpace IB b) :
  (g_bilin_1 (IB := IB) i b).snd.toFun α β = (g_bilin_2 i b).toFun α β := by
  unfold g_bilin_1 g_bilin_2 g_bilin_1g g_bilin_2g
  let ψ := FiberBundle.trivializationAt (EB →L[ℝ] EB →L[ℝ] ℝ)
    (fun (x : B) ↦ TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ) i
  let χ := trivializationAt EB (TangentSpace (M := B) IB) i
  let w := ψ.symm b (innerSL ℝ)
  simp only []
  simp only [hom_trivializationAt_target,
    hom_trivializationAt_baseSet,
    Trivial.fiberBundle_trivializationAt', Trivial.trivialization_baseSet,
    PartialEquiv.invFun_as_coe, OpenPartialHomeomorph.coe_coe_symm,
    dite_eq_ite,
    AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, ContinuousLinearMap.coe_coe]
  have hhc : b ∈ (chartAt HB i).source := Set.mem_of_mem_inter_left hhb.1
  have hhd : ((ψ.toOpenPartialHomeomorph.symm (b, innerSL ℝ)).snd α) β =
        ((innerSL ℝ) ((Trivialization.linearMapAt ℝ χ b) β))
                     ((Trivialization.linearMapAt ℝ χ b) α) :=
                     sorry -- I have a proof for this
  rw [hhz i]
  rw [if_pos hhc, if_pos hhb]
  exact hhd

omit [SigmaCompactSpace B] [T2Space B] [FiniteDimensional ℝ F] in
lemma g_bilin_1g_proj (i b : B) :
  (g_bilin_1g (E := E) (F := F) i b).proj = b := by
  unfold g_bilin_1g
  let ψ := FiberBundle.trivializationAt (F →L[ℝ] F →L[ℝ] ℝ)
    (fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) i
  dsimp only []
  split_ifs with h
  · exact Trivialization.proj_symm_apply ψ h
  · rfl

-- In the generalised version I seem to have to write `cast`
lemma g_bilin_eqg (i b : B)
  (hha : (b, innerSL ℝ) ∈
        (trivializationAt (F →L[ℝ] F →L[ℝ] ℝ)
         (fun x ↦ E x →L[ℝ] E x →L[ℝ] ℝ) i).target)
  (hhb : (b, innerSL (E := F) ℝ) ∈
        ((chartAt HB i).source ∩ ((chartAt HB i).source ∩ Set.univ)) ×ˢ Set.univ)
  (hhz : ∀ x, (trivializationAt F E x).baseSet = (chartAt HB (M := B) x).source)
  (α β : E b) :
    (g_bilin_1g (E := E) (F := F) i b).snd.toFun
    (cast (by rw [g_bilin_1g_proj]) α)
    (cast (by rw [g_bilin_1g_proj]) β)
  = (g_bilin_2g (F := F) i b).toFun α β := by
  unfold g_bilin_1g g_bilin_2g
  let ψ := FiberBundle.trivializationAt (F →L[ℝ] F →L[ℝ] ℝ)
    (fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) i
  let χ := trivializationAt F E i
  let w := ψ.symm b (innerSL ℝ)
  simp only []
  simp only [hom_trivializationAt_target,
    hom_trivializationAt_baseSet,
    Trivial.fiberBundle_trivializationAt', Trivial.trivialization_baseSet,
    PartialEquiv.invFun_as_coe, OpenPartialHomeomorph.coe_coe_symm,
    dite_eq_ite,
    AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, ContinuousLinearMap.coe_coe]
  have hhc : b ∈ (chartAt HB i).source := Set.mem_of_mem_inter_left hhb.1
  have hhd : ((ψ.toOpenPartialHomeomorph.symm (b, innerSL ℝ)).snd α) β =
        ((innerSL ℝ) ((Trivialization.linearMapAt ℝ χ b) β))
                     ((Trivialization.linearMapAt ℝ χ b) α) :=
                      sorry -- I have a proof for this
  rw [hhz i] -- this fails
  rw [if_pos hhc, if_pos hhb]
  exact hhd

[Dominic Steinitz]

Changing the definition worked but how one is supposed to know this is beyond me.

noncomputable
def g_bilin_1g (i b : B) :
 (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ)
             (fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ)) :=
  ⟨b, by
    let ψ := trivializationAt (F →L[ℝ] F →L[ℝ] ℝ)
        (fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) i
    by_cases h : (b, (fun (x : B) ↦ innerSL ℝ) b) ∈ ψ.target
    · exact (ψ.invFun (b, (fun (x : B) ↦ innerSL ℝ) b)).snd
    · exact 0⟩