Last step; Smoothness of vector bundle of alternating maps

Stream: maths

[Sam Lindauer]

Hey all,

I am working on differential forms. They are defined using the smooth vector bundle of continuous alternating maps. Definitionally, this is finished. I am only missing a part of the proof of smoothness for the vector bundle of continuous alternating maps. See #mwe below (it is quite long because some of the necessary definitions and instances are not yet in mathlib).

Any help or insight is sincerely appreciated!

Sam

import Mathlib

noncomputable section

open scoped Manifold

variable {𝕜 ι E F G : Type*}
  [NontriviallyNormedField 𝕜] [Fintype ι]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  [NormedAddCommGroup G] [NormedSpace 𝕜 G]

/- Additional setup from different Mathlib branch -/
instance instSeminormedAddCommGroup : SeminormedAddCommGroup (E [⋀^ι]→L[𝕜] F) where
  toPseudoMetricSpace := .induced ContinuousAlternatingMap.toContinuousMultilinearMap inferInstance
  __ := SeminormedAddCommGroup.induced _ _ (ContinuousAlternatingMap.toMultilinearAddHom : E [⋀^ι]→L[𝕜] F →+ _)
  norm f := ‖f.toContinuousMultilinearMap‖

@[simp] theorem norm_toContinuousMultilinearMap (f : E [⋀^ι]→L[𝕜] F) : ‖f.1‖ = ‖f‖ := rfl

theorem ContinuousAlternatingMap.norm_compContinuousLinearMap_le (f : F [⋀^ι]→L[𝕜] G)
    (g : E →L[𝕜] F) : ‖f.compContinuousLinearMap g‖ ≤ ‖f‖ * (‖g‖ ^ Fintype.card ι) :=
  (f.1.norm_compContinuousLinearMap_le _).trans_eq <| by simp

instance normedAddCommGroup : NormedAddCommGroup (E [⋀^ι]→L[𝕜] F) :=
  NormedAddCommGroup.ofSeparation fun _f hf ↦
    ContinuousAlternatingMap.toContinuousMultilinearMap_injective <| norm_eq_zero.mp hf

instance instNormedSpace {𝕜' : Type*} [NormedField 𝕜'] [NormedSpace 𝕜' F] [SMulCommClass 𝕜 𝕜' F] :
    NormedSpace 𝕜' (E [⋀^ι]→L[𝕜] F) :=
  ⟨fun c f ↦ f.1.opNorm_smul_le c⟩

/- Function definition -/
def ContinuousAlternatingMap.compContinuousLinearMapCLM (f : E →L[𝕜] F) :
    (F [⋀^ι]→L[𝕜] G) →L[𝕜] (E [⋀^ι]→L[𝕜] G) :=
  LinearMap.mkContinuous
    (ContinuousAlternatingMap.compContinuousLinearMapₗ f) (‖f‖ ^ Fintype.card ι) fun g ↦
      (g.norm_compContinuousLinearMap_le f).trans_eq (mul_comm _ _)

/- Proof of smoothness -/
theorem ContinuousAlternatingMap.compContinuousLinearMapCLM_contMDiff :
    ContMDiff 𝓘(𝕜, (E →L[𝕜] E)) 𝓘(𝕜, ((E [⋀^ι]→L[𝕜] G) →L[𝕜] (E [⋀^ι]→L[𝕜] G))) ⊤
      (fun (p : (E →L[𝕜] E)) ↦ (ContinuousAlternatingMap.compContinuousLinearMapCLM p :
        ((E [⋀^ι]→L[𝕜] G) →L[𝕜] (E [⋀^ι]→L[𝕜] G)))) := by
  sorry

[Patrick Massot]

@Floris van Doorn or @Heather Macbeth can probably help.

[Sébastien Gouëzel]

I'm working on this.

[Sébastien Gouëzel]

In #22089, there is the following theorem:

lemma analyticOn_uncurry_compContinuousLinearMap :
    AnalyticOn 𝕜 (fun (p : (Π i, Fm i →L[𝕜] Em i) × (ContinuousMultilinearMap 𝕜 Em G))
      ↦ p.2.compContinuousLinearMap p.1) t := ...

Hopefully, you can proceed from there (taking inspiration from the proof if needed, or writing your map as the composition of this one, and linear maps).

Unfortunately, #22089 uncovered some API gaps, so it will take some time (and I will need to split it into several PRs) before it can get in.

[Sébastien Gouëzel]

The first PR towards this is #22102, which splits the file CPolynomial.lean in two. This is necessary before further refactors. This is purely a splitting PR, so essentially trivial.

[Sam Lindauer]

I'll try to implement this at a later date, you'll hear from me if I managed or not. Thanks immensely for your time, this will surely help!

[Sébastien Gouëzel]

The analyticity is proved in #22089. I can split it if it helps, but since it's only +317/-53, I think it makes sense to keep everyting in one single PR.

[Patrick Massot]

I am surprised to see no fun_prop annotation anywhere in this PR. Is there something that blocks fun_prop here?

[Sébastien Gouëzel]

As far as I can tell, fun_prop is not used for CPolynomialAt, which is the bulk of the PR. More importantly, what I prove is

AnalyticAt 𝕜 (fun (p : (Π i, Fm i →L[𝕜] Em i) × (ContinuousMultilinearMap 𝕜 Em G))
      ↦ p.2.compContinuousLinearMap p.1) q

but this one is not a good candidate for fun_prop: it should rather be the compositional version saying that, if f and g are analytic, then x ↦ (f x).compContinuousLinearMap (g x) is analytic. Except that the original poster doesn't need this version, but rather the version in C^k smoothness. It would make sense to add all these, but the PR is already pretty long. Tell me if you want me to add them to the PR nevertheless!

[Patrick Massot]

Yes, my question is precisely: why don’t we use fun_prop for CPolynomialAt?

[Sébastien Gouëzel]

That's a good question, but that would be for another PR.

[Sam Lindauer]

I have the feeling I am almost there, @Sébastien Gouëzel . At this point, I have proven an auxiliary lemma that proves a close relative to what we want to prove for continuous multilinear maps, namely the following (it fits into the #mwe above)

theorem ContinuousMultilinearMap.compContinuousLinearMapL_diag_contDiff :
  ContDiff 𝕜 ⊤ (fun p : E →L[𝕜] E ↦
  (ContinuousMultilinearMap.compContinuousLinearMapL (fun _ : ι ↦ p) :
    ContinuousMultilinearMap 𝕜 (fun _ ↦ E) G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun _ ↦ E) G)) := by
  let φ : ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E →L[𝕜] E) _ :=
    ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear
    𝕜 (fun _ : ι ↦ E) (fun _ : ι ↦ E) G
  show ContDiff 𝕜 ⊤ (fun p : E →L[𝕜] E ↦ φ (fun _ : ι ↦ p))
  apply ContDiff.comp
  · apply ContinuousMultilinearMap.contDiff
  · apply contDiff_pi.mpr
    intro _
    apply contDiff_id

Then, I have created a linear equivalence between alternating and multilinear maps using the inclusion and the alternatization as follows (not fully proven yet, fits into #mwe above if [DecidableEq ι] is added).

def _root_.ContinuousLinearEquiv.ContinuousAlternatingMapContinuousMultilinearMapEquiv :
    (E [⋀^ι]→L[𝕜] G) ≃L[𝕜] (ContinuousMultilinearMap 𝕜 (ι := ι) (fun x ↦ E) G) where
  toFun := ContinuousAlternatingMap.toContinuousMultilinearMap
  invFun := ContinuousMultilinearMap.alternatization
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  left_inv := sorry
  right_inv := sorry
  continuous_toFun := ContinuousAlternatingMap.continuous_toContinuousMultilinearMap
  continuous_invFun := sorry

Finally, I have gotten the proof of the theorem up to a similar statement to ContinuousMultilinearMap.compContinuousLinearMapL_diag_contDiff but the closing step eludes me. This is the proof so far (also needs [DecidableEq ι] to fit into #mwe):

theorem ContinuousAlternatingMap.compContinuousLinearMapCLM_contMDiff :
    ContMDiff 𝓘(𝕜, (E →L[𝕜] E)) 𝓘(𝕜, ((E [⋀^ι]→L[𝕜] G) →L[𝕜] (E [⋀^ι]→L[𝕜] G))) ⊤
      (fun (p : (E →L[𝕜] E)) ↦ (ContinuousAlternatingMap.compContinuousLinearMapCLM p :
        ((E [⋀^ι]→L[𝕜] G) →L[𝕜] (E [⋀^ι]→L[𝕜] G)))) := by
  rw [contMDiff_iff_contDiff]
  let θ : (E [⋀^ι]→L[𝕜] G) ≃L[𝕜] (ContinuousMultilinearMap 𝕜 (ι := ι) (fun x ↦ E) G) :=
    ContinuousLinearEquiv.ContinuousAlternatingMapContinuousMultilinearMapEquiv
  let Θ : ((E [⋀^ι]→L[𝕜] G) →L[𝕜] (E [⋀^ι]→L[𝕜] G)) ≃L[𝕜]
    ((ContinuousMultilinearMap 𝕜 (ι := ι) (fun x ↦ E) G) →L[𝕜]
      (ContinuousMultilinearMap 𝕜 (ι := ι) (fun x ↦ E) G)) :=
        ContinuousLinearEquiv.arrowCongr θ θ
  rw[← ContinuousLinearEquiv.comp_contDiff_iff (𝕜 := 𝕜)
    (F := ((E [⋀^ι]→L[𝕜] G) →L[𝕜] (E [⋀^ι]→L[𝕜] G)))
    (G := ((ContinuousMultilinearMap 𝕜 (ι := ι) (fun x ↦ E) G) →L[𝕜]
      (ContinuousMultilinearMap 𝕜 (ι := ι) (fun x ↦ E) G))) Θ]
  sorry

Thanks in advance!

[Sam Lindauer]

In case that helps, here is the full #mwe :

import Mathlib

noncomputable section

open scoped Manifold

variable {𝕜 ι E F G : Type*}
  [NontriviallyNormedField 𝕜]
  [Fintype ι]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  [NormedAddCommGroup G] [NormedSpace 𝕜 G]

/- Additional setup from different Mathlib branch -/
instance instSeminormedAddCommGroup : SeminormedAddCommGroup (E [⋀^ι]→L[𝕜] F) where
  toPseudoMetricSpace := .induced ContinuousAlternatingMap.toContinuousMultilinearMap inferInstance
  __ := SeminormedAddCommGroup.induced _ _ (ContinuousAlternatingMap.toMultilinearAddHom : E [⋀^ι]→L[𝕜] F →+ _)
  norm f := ‖f.toContinuousMultilinearMap‖

@[simp] theorem norm_toContinuousMultilinearMap (f : E [⋀^ι]→L[𝕜] F) : ‖f.1‖ = ‖f‖ := rfl

theorem ContinuousAlternatingMap.norm_compContinuousLinearMap_le (f : F [⋀^ι]→L[𝕜] G)
    (g : E →L[𝕜] F) : ‖f.compContinuousLinearMap g‖ ≤ ‖f‖ * (‖g‖ ^ Fintype.card ι) :=
  (f.1.norm_compContinuousLinearMap_le _).trans_eq <| by simp

instance normedAddCommGroup : NormedAddCommGroup (E [⋀^ι]→L[𝕜] F) :=
  NormedAddCommGroup.ofSeparation fun _f hf ↦
    ContinuousAlternatingMap.toContinuousMultilinearMap_injective <| norm_eq_zero.mp hf

instance instNormedSpace {𝕜' : Type*} [NormedField 𝕜'] [NormedSpace 𝕜' F] [SMulCommClass 𝕜 𝕜' F] :
    NormedSpace 𝕜' (E [⋀^ι]→L[𝕜] F) :=
  ⟨fun c f ↦ f.1.opNorm_smul_le c⟩

/- Function definition -/
def ContinuousAlternatingMap.compContinuousLinearMapCLM (f : E →L[𝕜] F) :
    (F [⋀^ι]→L[𝕜] G) →L[𝕜] (E [⋀^ι]→L[𝕜] G) :=
  LinearMap.mkContinuous
    (ContinuousAlternatingMap.compContinuousLinearMapₗ f) (‖f‖ ^ Fintype.card ι) fun g ↦
      (g.norm_compContinuousLinearMap_le f).trans_eq (mul_comm _ _)

theorem ContinuousMultilinearMap.compContinuousLinearMapL_diag_contDiff :
  ContDiff 𝕜 ⊤ (fun p : E →L[𝕜] E ↦
  (ContinuousMultilinearMap.compContinuousLinearMapL (fun _ : ι ↦ p) :
    ContinuousMultilinearMap 𝕜 (fun _ ↦ E) G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun _ ↦ E) G)) := by
  let φ : ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E →L[𝕜] E) _ :=
    ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear
    𝕜 (fun _ : ι ↦ E) (fun _ : ι ↦ E) G
  show ContDiff 𝕜 ⊤ (fun p : E →L[𝕜] E ↦ φ (fun _ : ι ↦ p))
  apply ContDiff.comp
  · apply ContinuousMultilinearMap.contDiff
  · apply contDiff_pi.mpr
    intro _
    apply contDiff_id

variable [DecidableEq ι]

def _root_.ContinuousLinearEquiv.ContinuousAlternatingMapContinuousMultilinearMapEquiv :
    (E [⋀^ι]→L[𝕜] G) ≃L[𝕜] (ContinuousMultilinearMap 𝕜 (ι := ι) (fun x ↦ E) G) where
  toFun := ContinuousAlternatingMap.toContinuousMultilinearMap
  invFun := ContinuousMultilinearMap.alternatization
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  left_inv := sorry
  right_inv := sorry
  continuous_toFun := ContinuousAlternatingMap.continuous_toContinuousMultilinearMap
  continuous_invFun := sorry

/- Proof of smoothness -/
theorem ContinuousAlternatingMap.compContinuousLinearMapCLM_contMDiff :
    ContMDiff 𝓘(𝕜, (E →L[𝕜] E)) 𝓘(𝕜, ((E [⋀^ι]→L[𝕜] G) →L[𝕜] (E [⋀^ι]→L[𝕜] G))) ⊤
      (fun (p : (E →L[𝕜] E)) ↦ (ContinuousAlternatingMap.compContinuousLinearMapCLM p :
        ((E [⋀^ι]→L[𝕜] G) →L[𝕜] (E [⋀^ι]→L[𝕜] G)))) := by
  rw [contMDiff_iff_contDiff]
  let θ : (E [⋀^ι]→L[𝕜] G) ≃L[𝕜] (ContinuousMultilinearMap 𝕜 (ι := ι) (fun x ↦ E) G) :=
    ContinuousLinearEquiv.ContinuousAlternatingMapContinuousMultilinearMapEquiv
  let Θ : ((E [⋀^ι]→L[𝕜] G) →L[𝕜] (E [⋀^ι]→L[𝕜] G)) ≃L[𝕜]
    ((ContinuousMultilinearMap 𝕜 (ι := ι) (fun x ↦ E) G) →L[𝕜]
      (ContinuousMultilinearMap 𝕜 (ι := ι) (fun x ↦ E) G)) :=
        ContinuousLinearEquiv.arrowCongr θ θ
  rw[← ContinuousLinearEquiv.comp_contDiff_iff (𝕜 := 𝕜)
    (F := ((E [⋀^ι]→L[𝕜] G) →L[𝕜] (E [⋀^ι]→L[𝕜] G)))
    (G := ((ContinuousMultilinearMap 𝕜 (ι := ι) (fun x ↦ E) G) →L[𝕜]
      (ContinuousMultilinearMap 𝕜 (ι := ι) (fun x ↦ E) G))) Θ]
  sorry

[Sébastien Gouëzel]

Sam Lindauer said:

Then, I have created a linear equivalence between alternating and multilinear maps using the inclusion and the alternatization as follows (not fully proven yet, fits into #mwe above if [DecidableEq ι] is added).

This can not be correct, unfortunately: there are more multilinear maps than alternating maps, so you can't have such an equivalence (for dimension reasons, for instance). What you should do instead is build on the space of alternative maps the analogues of the results we have for multilinear maps (possibly using the multilinear maps version, and then proving that what you get is alternating).

[Sam Lindauer]

Sébastien Gouëzel said:

Sam Lindauer said:

Then, I have created a linear equivalence between alternating and multilinear maps using the inclusion and the alternatization as follows (not fully proven yet, fits into #mwe above if [DecidableEq ι] is added).

This can not be correct, unfortunately: there are more multilinear maps than alternating maps, so you can't have such an equivalence (for dimension reasons, for instance). What you should do instead is build on the space of alternative maps the analogues of the results we have for multilinear maps (possibly using the multilinear maps version, and then proving that what you get is alternating).

I see, I was bit skeptical already, but good to have it assured. It's a bit bigger of a task than I initially expected then. Thanks for your quick reply!