The wedge as a bounded bilinear map; reindexing as a continuous linear map

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

The norm bound that Wedge.lean's honest scope listed as "true and a natural follow-up". Wedge.lean proved the exterior product of two continuous alternating maps continuous in the vector family; this module proves it bilinear and bounded in the pair of forms, which is what makes the wedge of two smooth sections smooth:

• liftTensor_summand_mk'' — one summand of the shuffle sum, on a representative permutation: sign σ • B (a (v ∘ σ ∘ inl)) (b (v ∘ σ ∘ inr));
• ★ wedge_compContinuousLinearMap — pullback commutes with the wedge, (a ∧ b) ∘ L = (a ∘ L) ∧ (b ∘ L);
• wedge_add_left, wedge_smul_left, wedge_add_right, wedge_smul_right — bilinearity;
• ★ norm_wedge_le — ‖a ∧ b‖ ≤ card (shuffle classes) · ‖B‖ · ‖a‖ · ‖b‖;
• ★ wedgeL — the wedge as a continuous bilinear map, and contDiff_wedge, ContDiff.wedge, ContDiffAt.wedge — it is C^n in the pair, so a wedge of C^n families of forms is C^n;
• domDomCongr_compContinuousLinearMap, norm_domDomCongr_le, domDomCongrL, ContDiff.domDomCongr, ContDiffAt.domDomCongr — the same for reindexing along an equivalence of index types, which the iterated power needs at every step.

Honest scope

⚠️ The constant in norm_wedge_le is the crude one (the number of shuffle classes times ‖B‖); no sharp bound is claimed. ⚠️ Associativity, graded commutativity and the Leibniz rule of the wedge are still not here (they are algebraic facts about AlternatingMap.domCoprod first, and Mathlib does not have them either; MATHLIB-ABSENT(ContinuousAlternatingMap.wedgeL)).

Provenance and references. The top-power plan (M2); Alternating/Wedge.lean (the wedge); Geometry/Manifold/WedgeForm.lean (the consumer: the wedge of sections); the completed-work ledger.

theorem ContinuousAlternatingMap.liftTensor_summand_mk'' {𝕜 : 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 (ιa ⊕ ιb)) (v : ιa ⊕ ιb → E) : B.liftTensor ((AlternatingMap.domCoprod.summand a.toAlternatingMap b.toAlternatingMap (Quotient.mk'' σ)) v) = ↑(Equiv.Perm.sign σ) • (B (a fun (i : ιa) => v (σ (Sum.inl i)))) (b fun (i : ιb) => v (σ (Sum.inr i)))

One summand of the wedge, on a representative permutation.

theorem ContinuousAlternatingMap.wedge_compContinuousLinearMap {𝕜 : 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] {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (B : F →L[𝕜] G →L[𝕜] H) (a : E [⋀^ιa]→L[𝕜] F) (b : E [⋀^ιb]→L[𝕜] G) (L : E' →L[𝕜] E) : (wedge B a b).compContinuousLinearMap L = wedge B (a.compContinuousLinearMap L) (b.compContinuousLinearMap L)

★ Pullback commutes with the wedge.

theorem ContinuousAlternatingMap.wedge_add_left {𝕜 : 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₁ a₂ : E [⋀^ιa]→L[𝕜] F) (b : E [⋀^ιb]→L[𝕜] G) : wedge B (a₁ + a₂) b = wedge B a₁ b + wedge B a₂ b

theorem ContinuousAlternatingMap.wedge_smul_left {𝕜 : 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) (c : 𝕜) (a : E [⋀^ιa]→L[𝕜] F) (b : E [⋀^ιb]→L[𝕜] G) : wedge B (c • a) b = c • wedge B a b

theorem ContinuousAlternatingMap.wedge_add_right {𝕜 : 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₁ b₂ : E [⋀^ιb]→L[𝕜] G) : wedge B a (b₁ + b₂) = wedge B a b₁ + wedge B a b₂

theorem ContinuousAlternatingMap.wedge_smul_right {𝕜 : 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) (c : 𝕜) (a : E [⋀^ιa]→L[𝕜] F) (b : E [⋀^ιb]→L[𝕜] G) : wedge B a (c • b) = c • wedge B a b

theorem ContinuousAlternatingMap.norm_wedge_le {𝕜 : 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‖ ≤ ↑(Fintype.card (Equiv.Perm.ModSumCongr ιa ιb)) * ‖B‖ * ‖a‖ * ‖b‖

★ The norm bound: the wedge is a bounded bilinear map.

noncomputable def ContinuousAlternatingMap.wedgeL {𝕜 : 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) : E [⋀^ιa]→L[𝕜] F →L[𝕜] E [⋀^ιb]→L[𝕜] G →L[𝕜] E [⋀^ιa ⊕ ιb]→L[𝕜] H

★ The wedge as a continuous bilinear map.

Equations

• ContinuousAlternatingMap.wedgeL B = (LinearMap.mk₂ 𝕜 (ContinuousAlternatingMap.wedge B) ⋯ ⋯ ⋯ ⋯).mkContinuous₂ (↑(Fintype.card (Equiv.Perm.ModSumCongr ιa ιb)) * ‖B‖) ⋯

@[simp]

theorem ContinuousAlternatingMap.wedgeL_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) : ((wedgeL B) a) b = wedge B a b

theorem ContinuousAlternatingMap.contDiff_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) {n : WithTop ℕ∞} : ContDiff 𝕜 n fun (p : E [⋀^ιa]→L[𝕜] F × E [⋀^ιb]→L[𝕜] G) => wedge B p.1 p.2

★ The wedge is C^n in the pair of forms.

theorem ContDiff.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] {X : Type u_8} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (B : F →L[𝕜] G →L[𝕜] H) {n : WithTop ℕ∞} {f : X → E [⋀^ιa]→L[𝕜] F} {g : X → E [⋀^ιb]→L[𝕜] G} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n fun (x : X) => ContinuousAlternatingMap.wedge B (f x) (g x)

theorem ContDiffAt.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] {X : Type u_8} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (B : F →L[𝕜] G →L[𝕜] H) {n : WithTop ℕ∞} {f : X → E [⋀^ιa]→L[𝕜] F} {g : X → E [⋀^ιb]→L[𝕜] G} {x : X} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun (x : X) => ContinuousAlternatingMap.wedge B (f x) (g x)) x

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

Reindexing commutes with pullback.

theorem ContinuousAlternatingMap.norm_domDomCongr_le {𝕜 : 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} [Fintype ι] [Fintype ι'] (σ : ι ≃ ι') (f : E [⋀^ι]→L[𝕜] F) : ‖domDomCongr σ f‖ ≤ ‖f‖

Reindexing is norm-preserving, hence a continuous linear map.

noncomputable def ContinuousAlternatingMap.domDomCongrL {𝕜 : 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} [Fintype ι] [Fintype ι'] (σ : ι ≃ ι') : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι']→L[𝕜] F

Reindexing as a continuous linear map.

Equations

• ContinuousAlternatingMap.domDomCongrL σ = { toFun := ContinuousAlternatingMap.domDomCongr σ, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

@[simp]

theorem ContinuousAlternatingMap.domDomCongrL_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} [Fintype ι] [Fintype ι'] (σ : ι ≃ ι') (f : E [⋀^ι]→L[𝕜] F) : (domDomCongrL σ) f = domDomCongr σ f

theorem ContDiff.domDomCongr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {X : Type u_8} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {ι : Type u_9} {ι' : Type u_10} [Fintype ι] [Fintype ι'] (σ : ι ≃ ι') {n : WithTop ℕ∞} {f : X → E [⋀^ι]→L[𝕜] F} (hf : ContDiff 𝕜 n f) : ContDiff 𝕜 n fun (x : X) => ContinuousAlternatingMap.domDomCongr σ (f x)

theorem ContDiffAt.domDomCongr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {X : Type u_8} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {ι : Type u_9} {ι' : Type u_10} [Fintype ι] [Fintype ι'] (σ : ι ≃ ι') {n : WithTop ℕ∞} {f : X → E [⋀^ι]→L[𝕜] F} {x : X} (hf : ContDiffAt 𝕜 n f x) : ContDiffAt 𝕜 n (fun (x : X) => ContinuousAlternatingMap.domDomCongr σ (f x)) x