Interior product of an alternatization

Open

ContWeatherall.alternatizeUncurryFin_apply_cons

by Alien60 · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

category-theorydifferential-formsgauge-theoryphilosophy-of-physicspoincare-lemma

For a continuous linear $L:E\to E[\wedge^{n+1}]\to_LF$ over a nontrivially normed field, $\mathrm{alt}(L)(x,v)=L(x)(v)-\sum_i(-1)^iL(v_i)(x,v_0,\dots,\widehat{v_i},\dots,v_n)$ , where alt is alternatizeUncurryFin.

Preamble

import Mathlib
import Definitions.Def_ContWeatherall_defs

open CategoryTheory ContinuousAlternatingMap
open scoped ContDiff

Formal statement

namespace ContWeatherall

/-- Interior product of the alternatization: for `L : E →L E [⋀^Fin (n+1)]→L F`,
`(alt L)(x, v) = L x v - ∑ i, (-1)^i L (v i) (x, v without vᵢ)`. -/
theorem alternatizeUncurryFin_apply_cons {𝕜 E F : Type*} [NontriviallyNormedField 𝕜]
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ}
    (L : E →L[𝕜] E [⋀^Fin (n + 1)]→L[𝕜] F) (x : E) (v : Fin (n + 1) → E) :
    alternatizeUncurryFin L (Fin.cons x v) =
      L x v - ∑ i : Fin (n + 1), (-1 : ℤ) ^ (i : ℕ) • L (v i) (Fin.cons x (i.removeNth v)) := by
  sorry

end ContWeatherall

Source

M. Spivak, Calculus on Manifolds (W. A. Benjamin, 1965), Theorem 4-11 (Poincaré lemma) and its proof (the d-of-insertion step)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $\mathbb{K}$ be a nontrivially normed field, $E,F$ normed spaces over $\mathbb{K}$ , $n\in\mathbb{N}$ , and $L:E\to\mathrm{Alt}^{n+1}(E;F)$ a continuous $\mathbb{K}$ -linear map. Let $x\in E$ , $v=(v_0,\dots,v_n)\in E^{n+1}$ . Writing $\operatorname{alt}(L)\in\mathrm{Alt}^{n+2}(E;F)$ for Mathlib's alternatization of the uncurried $L$ , the statement is

\operatorname{alt}(L)(x,v_0,\dots,v_n)=L(x)(v_0,\dots,v_n)-\sum_{i=0}^{n}(-1)^i\,L(v_i)\big(x,v_0,\dots,\widehat{v_i},\dots,v_n\big),

with $(-1)^i$ an integer scalar acting on $F$ and $(x,v)$ meaning $x$ prepended to $v$ .

View graph