Properties of wedge product of differential forms

Stream: maths

[Sam Lindauer]

Hey all! I am currently working on the repository for differential forms on manifolds. At this point, we have made quite a bit of progress including the definition of differential forms on manifolds using the smooth vector bundle of continuous alternating maps. My main purpose at this point is to define the wedge product, exterior derivative and their properties for differential forms on manifolds using the background that we have implemented. There are a few background proofs that need to be finished still to do that though and there is a collection of details that I need help with to be able to finish this. These details show up in the proofs of properties of the wedge product on differential forms in normed spaces.

There is a lot of code as background for these definitions and proofs that can be found in the repository here: https://github.com/urkud/DeRhamCohomology/tree/SL-properties-wedge_product
All the sorry's that these questions correspond to can be found under DeRhamCohomology/DifferentialForm.lean and DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean

There is a collection of 6 questions in total:

Three of these have to do with sums and rewriting sums over quotients:
1) For the proof of the leibniz rule for the exterior derivative of differential forms on normed spaces, see ederiv_wedge in DeRhamCohomology/DifferentialForm.lean, I want to eventually be able to discard the sums that are left, see

E : Type u_1
F : Type u_2
F' : Type u_3
F'' : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup F''
inst✝ : NormedSpace ℝ F''
n m : ℕ
ω : E → E [⋀^Fin m]→L[ℝ] F
τ : E → E [⋀^Fin n]→L[ℝ] F'
f : F →L[ℝ] F' →L[ℝ] F''
x : E
y : Fin (m + n + 1) → E
⊢ ∑ k : Fin (m + n + 1), (-1) ^ ↑k • ((fderiv ℝ (ω∧[f]τ) x) (y k)) (k.removeNth y) =
  ∑ a : Equiv.Perm.ModSumCongr (Fin (m + 1)) (Fin n),
      (uncurrySum.summand (f.compContinuousAlternatingMap₂ (ederiv ω x) (τ x)) a)
        ((y ∘ ⇑finAddFlipAssoc) ∘ ⇑finSumFinEquiv) +
    (-1) ^ m •
      ∑ a : Equiv.Perm.ModSumCongr (Fin m) (Fin (n + 1)),
        (uncurrySum.summand (f.compContinuousAlternatingMap₂ (ω x) (ederiv τ x)) a) (y ∘ ⇑finSumFinEquiv)

However, as can be seen in the above (or in the repo), the sums aren't equivalent, so I cannot use Finset.sum_congr or something similar. For the other unknown definitions in the above Infoview text, have a look at the repo. I am not sure what a next step should or even could be here.

2) The second sorry is a similar, if not the same, question for the Leibniz rule of the interior product of the wedge product, iprod_wedge also found in DeRhamCohomology/DifferentialForm.lean.

3) The third question that has to do with sums comes from the proof of the associativity of the wedge product of continuous alternating maps in normed spaces, namely wedge_assoc in DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean. Here, the state is as follows:

𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
M : Type u_2
inst✝³ : NormedAddCommGroup M
inst✝² : NormedSpace 𝕜 M
N : Type u_5
inst✝¹ : NormedAddCommGroup N
inst✝ : NormedSpace 𝕜 N
m n p : ℕ
g : M [⋀^Fin m]→L[𝕜] N
h : M [⋀^Fin n]→L[𝕜] N
f : N →L[𝕜] N →L[𝕜] N
l : M [⋀^Fin p]→L[𝕜] N
f' : N →L[𝕜] N →L[𝕜] N
v : Fin (m + n + p) → M
⊢ ∑ a : Equiv.Perm.ModSumCongr (Fin m) (Fin (n + p)),
    (uncurrySum.summand (f.compContinuousAlternatingMap₂ g (f'.compContinuousAlternatingMap₂ h l).uncurryFinAdd) a)
      ((v ∘ ⇑finAssoc.symm) ∘ ⇑finSumFinEquiv) =
  ∑ a : Equiv.Perm.ModSumCongr (Fin (m + n)) (Fin p),
    (uncurrySum.summand (f'.compContinuousAlternatingMap₂ (f.compContinuousAlternatingMap₂ g h).uncurryFinAdd l) a)
      (v ∘ ⇑finSumFinEquiv)

Once again, refer to the repo for a complete overview of the definitions etc. The goal here is to eventually discard the sums by seeing that they consist of the same arguments. How does one approach this?

The rest of the questions are not related:
4) To complete to proof that g ∧ g = 0 for odd degree continuous alternating maps g, see wedge_self_odd_zero in DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean, I need to be able to rewrite the following goal (and a similar goal with Sum.inl and Sum.inr swapped)

m : ℕ
M : Type u_8
inst✝¹ : NormedAddCommGroup M
inst✝ : NormedSpace ℝ M
g : M [⋀^Fin m]→L[ℝ] ℝ
m_odd : Odd m
x : Fin (m + m) → M
h : (g∧[ContinuousLinearMap.mul ℝ ℝ]g) x = -1 • (g∧[ContinuousLinearMap.mul ℝ ℝ]g) (x ∘ ⇑finAddFlip)
σ : Equiv.Perm.ModSumCongr (Fin m) (Fin m)
σ₁ : Equiv.Perm (Fin m ⊕ Fin m)
hσ : Quot.mk (⇑(QuotientGroup.leftRel (Equiv.Perm.sumCongrHom (Fin m) (Fin m)).range)) σ₁ ∈ Finset.univ
n : Fin m
⊢ ↑(finAddFlip (finSumFinEquiv (σ₁ (Sum.inl n)))) = ↑(finSumFinEquiv (σ₁ (Sum.inr n)))

I am not sure how to approach this.

5) For antisymmetry of the wedge product on continuous alternating maps, see wedge_antisymm in DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean, we start with a sum setup, similar to the first three questions, namely

𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
M : Type u_2
inst✝¹ : NormedAddCommGroup M
inst✝ : NormedSpace 𝕜 M
m n : ℕ
g : M [⋀^Fin m]→L[𝕜] 𝕜
h : M [⋀^Fin n]→L[𝕜] 𝕜
x : Fin (m + n) → M
⊢ ∑ a : Equiv.Perm.ModSumCongr (Fin m) (Fin n),
    (uncurrySum.summand ((ContinuousLinearMap.mul 𝕜 𝕜).compContinuousAlternatingMap₂ g h) a) (x ∘ ⇑finSumFinEquiv) =
  ∑ x_1 : Equiv.Perm.ModSumCongr (Fin n) (Fin m),
    (-1) ^ (m * n) •
      (uncurrySum.summand ((ContinuousLinearMap.mul 𝕜 𝕜).compContinuousAlternatingMap₂ h g) x_1)
        ((x ∘ ⇑finAddFlip) ∘ ⇑finSumFinEquiv)

With help from Johan Commelin, I was able to remove the sum by introducing an equivalence introduced as **h2** : Equiv.Perm.ModSumCongr (Fin m) (Fin n) ≃ Equiv.Perm.ModSumCongr (Fin n) (Fin m) which is yet to be proven. However, assuming this is proven, I get to a problem later in the proof where I cannot rewrite using uncurrySum.summand_mk, because of the h2 that is stuck before the quotient term. It is clear to me why it is there, but how does one deal with this? Here is what the infoview tells us there:

𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
M : Type u_2
inst✝¹ : NormedAddCommGroup M
inst✝ : NormedSpace 𝕜 M
m n : ℕ
g : M [⋀^Fin m]→L[𝕜] 𝕜
h : M [⋀^Fin n]→L[𝕜] 𝕜
x : Fin (m + n) → M
h2 : Equiv.Perm.ModSumCongr (Fin m) (Fin n) ≃ Equiv.Perm.ModSumCongr (Fin n) (Fin m)
σ : Equiv.Perm.ModSumCongr (Fin m) (Fin n)
σ₁ : Equiv.Perm (Fin m ⊕ Fin n)
hσ : Quot.mk (⇑(QuotientGroup.leftRel (Equiv.Perm.sumCongrHom (Fin m) (Fin n)).range)) σ₁ ∈ Finset.univ
⊢ Equiv.Perm.sign σ₁ •
    (g ((fun i ↦ (x ∘ ⇑finSumFinEquiv) (σ₁ i)) ∘ Sum.inl) * h ((fun i ↦ (x ∘ ⇑finSumFinEquiv) (σ₁ i)) ∘ Sum.inr)) =
  (-1) ^ (m * n) •
    (uncurrySum.summand ((ContinuousLinearMap.mul 𝕜 𝕜).compContinuousAlternatingMap₂ h g)
        (h2 (Quot.mk (⇑(QuotientGroup.leftRel (Equiv.Perm.sumCongrHom (Fin m) (Fin n)).range)) σ₁)))
      ((x ∘ ⇑finAddFlip) ∘ ⇑finSumFinEquiv)

6) Lastly, for the proof that the pullback and exterior derivative commute, see pullback_ederiv in DeRhamCohomology/DifferentialForm.lean, I need only prove two coditions: The first is the differentiability of the following function:

E : Type u_1
F : Type u_2
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
n : ℕ
f : E → F
ω : F → F [⋀^Fin n]→L[ℝ] G
x : E
hf : DifferentiableAt ℝ f x
hω : DifferentiableAt ℝ ω (f x)
hff : UniqueDiffOn ℝ univ
v : Fin (n + 1) → E
p : Fin (n + 1)
q : p ∈ Finset.univ
⊢ DifferentiableAt ℝ (fun x ↦ (ω (f x)).compContinuousLinearMap (fderiv ℝ f x)) x

and the second is an equivalence of two fderiv in neighbourdhoods, namely

E : Type u_1
F : Type u_2
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
n : ℕ
f : E → F
ω : F → F [⋀^Fin n]→L[ℝ] G
x : E
hf : DifferentiableAt ℝ f x
hω : DifferentiableAt ℝ ω (f x)
hff : UniqueDiffOn ℝ univ
v : Fin (n + 1) → E
p : Fin (n + 1)
q : p ∈ Finset.univ
this : p.removeNth (⇑(fderiv ℝ f x) ∘ v) = ⇑(fderiv ℝ f x) ∘ p.removeNth v
⊢ (fun x_1 ↦ fderiv ℝ f x) =ᶠ[𝓝 x] fderiv ℝ f

To me these seem doable, but I am lost as to how to prove these.

Sorry for the sheer number of questions. Any help on any of the above questions is greatly appreciated. Also sorry for not being able to provide full mwe's. The amount of background would make each question quite large in and of itself, so I decided to do it this way by referencing the repo that the code is in.

Thanks so much in advance for even looking at the questions.

Sam

[Eric Wieser]

At a glance some of these goals look similar to the ones I had to solve around docs#AlternatingMap.domCoprod. I assume you're already leveraging what you can from that though?

[Sébastien Gouëzel]

If you give me a #mwe for (6) 1, I'll give it a try.

[Sam Lindauer]

Eric Wieser said:

At a glance some of these goals look similar to the ones I had to solve around docs#AlternatingMap.domCoprod. I assume you're already leveraging what you can from that though?

I have used the code there as the inspiration for the definitions and necessary proofs for the wedge product. I think I have used most of the ideas and tricks that are there, but I might have missed a thing or two. I'll definitely have another look. Thanks.

[Sam Lindauer]

Sébastien Gouëzel said:

If you give me a #mwe for (6) 1, I'll give it a try.

Thanks for considering! I believe this should be the right #mwe :

import Mathlib

variable {E F G : Type*}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  [NormedAddCommGroup G] [NormedSpace ℝ G]
  {n : ℕ}
  (f : E → F)
  (ω : F → F [⋀^Fin n]→L[ℝ] G)

theorem differentiable_compContinuousLinearMap (x : E)
    (hf : DifferentiableAt ℝ f x) (hω : DifferentiableAt ℝ ω (f x)) (hff : UniqueDiffOn ℝ (univ : Set E)) :
    DifferentiableAt ℝ (fun x ↦ (ω (f x)).compContinuousLinearMap (fderiv ℝ f x)) x :=
  sorry

The differentiability conditions are the ones that I currently have set on the theorem. I believe these should be the right ones, but if there is a stronger condition necessary, do not hesitate to enforce it.

Btw, thanks a lot for your message from a while ago where you referenced the branch with the lie bracket of vector fields. This branch has been my main inspiration for setting up differential forms on manifolds and the exterior derivative. It has been and probably will continue to be tremendously helpful to take inspiration from!

[Michael Rothgang]

Quick thought about (6):

• first, you probably need to expand .compContinuousLinearMap, so you (morally) want to apply docs#ContinuousAlternatingMap.compContinuousLinearMap_apply
• in principle, then you have a composition of differentiable maps, so DifferentiableAt.comp should get you there

I'd need to wrap my head further around the types here to yield a compiling suggestion.

[Sébastien Gouëzel]

hff won't be needed (univ is always a set of unique differentiability). hf : DifferentiableAt ℝ f x won't be enough: you want something involving the derivative of f to be differentiable, so an assumption like C^2 would be more natural.

[Sam Lindauer]

Sébastien Gouëzel said:

hff won't be needed (univ is always a set of unique differentiability). hf : DifferentiableAt ℝ f x won't be enough: you want something involving the derivative of f to be differentiable, so an assumption like C^2 would be more natural.

That makes sense :smile: