The exterior product of continuous alternating maps

TERM-SCOPE(Kahler) — the phrase "top-power identity" appears below in the restricted sense the source repository's terms register records: the identity is what this file makes sayable, and it is neither stated nor proved here. (The marker is repository bookkeeping; it goes with the References block if the file is ever sent upstream.)

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Analysis.Normed.Module.Alternating).

Mathlib has the exterior product of two AlternatingMaps (AlternatingMap.domCoprod, valued in the tensor product of the two codomains) and it has ContinuousAlternatingMap. It does not have the exterior product of two continuous alternating maps: domCoprod occurs in exactly three algebraic files, and ContinuousAlternatingMap.domCoprod is zero declarations at the pin. MATHLIB-ABSENT(ContinuousAlternatingMap.domCoprod)

⚠️ And it cannot be stated in the tensor-valued form. There is no topology on F ⊗[𝕜] G at the pin, so E [⋀^ιa ⊕ ιb]→L[𝕜] (F ⊗[𝕜] G) is not a type. The standard fix, and the one taken here, is to pair the two codomains through a continuous bilinear map B : F →L[𝕜] G →L[𝕜] H. Every use in sight has that shape — for real-valued forms B is multiplication — and the tensor-valued version is recovered from this one the moment a topology on the tensor product exists, by taking B to be TensorProduct.mk.

Contents

• ContinuousLinearMap.liftTensor — the linear map F ⊗[𝕜] G →ₗ[𝕜] H induced by a continuous bilinear B;
• ContinuousAlternatingMap.continuous_liftTensor_summand — each summand of the antisymmetrisation, paired through B, is continuous. This is the whole mathematical content of the file;
• ★ ContinuousAlternatingMap.wedge — the exterior product itself;
• wedge_toAlternatingMap (rfl) — it is the algebraic AlternatingMap.domCoprod postcomposed with liftTensor B, so every algebraic fact about domCoprod transfers and this file adds exactly one thing: boundedness;
• wedge_apply — the pointwise signed sum over Equiv.Perm.ModSumCongr ιa ιb.

Honest scope

Delivered: the binary product and its two defining equations. NOT built here, and not claimed:

• associativity, graded commutativity and the Leibniz rule for extDeriv. All three are algebraic facts about domCoprod before they are facts about its continuous form, so the transport route (wedge_toAlternatingMap) can only carry what the algebraic side already proves. None of them is proved here;
• the iterated power: the index type of wedge is ιa ⊕ ιb, so an iterated product on Fin (2 * k) needs a domDomCongr along finSumFinEquiv at each step plus a recursion on k. That is the next brick, not this one;
• any nonvanishing statement. A wedge can be zero for good reasons (a 1-form with itself), and nothing here rules that out in any particular case;
• a norm bound. The construction goes through continuity rather than AlternatingMap.mkContinuous, so no constant is produced. The bound is true and is a natural follow-up; it is not needed in order to state a top power.

The point of the file is narrow and worth stating plainly: with it, a top-power identity of the shape ω^(N-1)/(N-1)! = μ_FS becomes sayable in Lean. It does not make any such statement true, and nothing here depends on it.

Provenance and references. The Mathlib-gaps register; the backlog (XL, "Manifold exterior calculus"); the terms register (moment map); CsdLean4/Mathlib/Analysis/InnerProductSpace/KahlerWedge.lean (the consumer).

noncomputable def ContinuousLinearMap.liftTensor {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} {G : Type u_4} {H : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup H] [NormedSpace 𝕜 H] (B : F →L[𝕜] G →L[𝕜] H) : TensorProduct 𝕜 F G →ₗ[𝕜] H

The linear map F ⊗[𝕜] G →ₗ[𝕜] H induced by a continuous bilinear map B.

This is TensorProduct.lift of the underlying bilinear map. The continuity of B is not used here — there is no topology on the source — only downstream, where the composite is shown to be a continuous function of the vector family.

Equations

• B.liftTensor = TensorProduct.lift (ContinuousLinearMap.coeLM 𝕜 ∘ₗ ↑B)

@[simp]

theorem ContinuousLinearMap.liftTensor_tmul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} {G : Type u_4} {H : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup H] [NormedSpace 𝕜 H] (B : F →L[𝕜] G →L[𝕜] H) (x : F) (y : G) : B.liftTensor (x ⊗ₜ[𝕜] y) = (B x) y

def ContinuousAlternatingMap.domDomCongr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_8} {ι' : Type u_9} (σ : ι ≃ ι') (f : E [⋀^ι]→L[𝕜] F) : E [⋀^ι']→L[𝕜] F

Reindex a continuous alternating map along an equivalence of index types.

Mathlib has this for AlternatingMap (AlternatingMap.domDomCongr) and for ContinuousMultilinearMap (ContinuousMultilinearMap.domDomCongr), but not for ContinuousAlternatingMap — MATHLIB-ABSENT(ContinuousAlternatingMap.domDomCongr).

It is needed here rather than merely wanted: wedge is indexed by ιa ⊕ ιb, while extDeriv and every other differential-form API in Mathlib is indexed by Fin n, so without a reindexing the product of two forms cannot be fed back into the calculus it came from.

Equations

• ContinuousAlternatingMap.domDomCongr σ f = { toContinuousMultilinearMap := ContinuousMultilinearMap.domDomCongr σ f.toContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.domDomCongr_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_8} {ι' : Type u_9} (σ : ι ≃ ι') (f : E [⋀^ι]→L[𝕜] F) (v : ι' → E) : (domDomCongr σ f) v = f fun (i : ι) => v (σ i)

theorem ContinuousAlternatingMap.continuous_liftTensor_summand {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {ιa : Type u_6} {ιb : Type u_7} [Fintype ιa] [Fintype ιb] [DecidableEq ιa] [DecidableEq ιb] (B : F →L[𝕜] G →L[𝕜] H) (a : E [⋀^ιa]→L[𝕜] F) (b : E [⋀^ιb]→L[𝕜] G) (σ : Equiv.Perm.ModSumCongr ιa ιb) : Continuous fun (v : ιa ⊕ ιb → E) => B.liftTensor ((AlternatingMap.domCoprod.summand a.toAlternatingMap b.toAlternatingMap σ) v)

The mathematical content of this file. One summand of the antisymmetrisation, paired through B, is a continuous function of the vector family.

The summand is a class in Equiv.Perm.ModSumCongr ιa ιb; on a representative σ it is Equiv.Perm.sign σ • (a (v ∘ σ ∘ Sum.inl) ⊗ₜ b (v ∘ σ ∘ Sum.inr)). Pairing through B and reading off continuity needs precomposition with σ (continuous coordinatewise), a and b, and the joint continuity of B (ContinuousLinearMap.continuous₂) — being separately continuous in each slot would not suffice.

noncomputable def ContinuousAlternatingMap.wedge {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {ιa : Type u_6} {ιb : Type u_7} [Fintype ιa] [Fintype ιb] [DecidableEq ιa] [DecidableEq ιb] (B : F →L[𝕜] G →L[𝕜] H) (a : E [⋀^ιa]→L[𝕜] F) (b : E [⋀^ιb]→L[𝕜] G) : E [⋀^ιa ⊕ ιb]→L[𝕜] H

★ The exterior product of two continuous alternating maps, with the codomains paired through a continuous bilinear map B.

Its underlying alternating map is the algebraic AlternatingMap.domCoprod postcomposed with ContinuousLinearMap.liftTensor B (wedge_toAlternatingMap, which is rfl); the new content is that the result is continuous.

Equations

• ContinuousAlternatingMap.wedge B a b = { toMultilinearMap := ↑(B.liftTensor.compAlternatingMap (a.toAlternatingMap.domCoprod b.toAlternatingMap)), cont := ⋯, map_eq_zero_of_eq' := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.wedge_toAlternatingMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {ιa : Type u_6} {ιb : Type u_7} [Fintype ιa] [Fintype ιb] [DecidableEq ιa] [DecidableEq ιb] (B : F →L[𝕜] G →L[𝕜] H) (a : E [⋀^ιa]→L[𝕜] F) (b : E [⋀^ιb]→L[𝕜] G) : (wedge B a b).toAlternatingMap = B.liftTensor.compAlternatingMap (a.toAlternatingMap.domCoprod b.toAlternatingMap)

The continuous exterior product is the algebraic one, paired through B. Every fact Mathlib proves about AlternatingMap.domCoprod transfers along this equation.

theorem ContinuousAlternatingMap.wedge_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {ιa : Type u_6} {ιb : Type u_7} [Fintype ιa] [Fintype ιb] [DecidableEq ιa] [DecidableEq ιb] (B : F →L[𝕜] G →L[𝕜] H) (a : E [⋀^ιa]→L[𝕜] F) (b : E [⋀^ιb]→L[𝕜] G) (v : ιa ⊕ ιb → E) : (wedge B a b) v = ∑ σ : Equiv.Perm.ModSumCongr ιa ιb, B.liftTensor ((AlternatingMap.domCoprod.summand a.toAlternatingMap b.toAlternatingMap σ) v)

The pointwise formula: a signed sum over shuffle classes.