The wedge of differential forms on a manifold

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Geometry.Manifold).

With the flat wedge bounded and bilinear (Alternating/WedgeCLM.lean) and the local-representative machinery of ExteriorDerivative.lean, the wedge of two smooth sections of alternating bundles is a smooth section, and so is a reindexing and the constant 0-form. Every smoothness proof is the same three lines: the trivialisation of the new section in the chart at x₀ is the flat operation applied to the local representatives (trivializationAt_*_snd, from trivializationAt_snd and the flat "commutes with pullback" lemma), the flat operation is C^∞ in its arguments, and contMDiffAt_section closes.

• DifferentialForm.wedgeFamily, ★ trivializationAt_wedgeFamily_snd, localRep_wedgeFamily, ★★ contMDiff_wedgeFamily, and the bundled ★★ DifferentialForm.wedge B α β — the wedge of two differential forms, an (ιa ⊕ ιb)-form;
• domDomCongrFamily, trivializationAt_domDomCongrFamily_snd, contMDiff_domDomCongrFamily, and ★ DifferentialForm.domDomCongr σ α — reindexing along an equivalence of index types (what brings ιa ⊕ ιb back to Fin (a + b));
• constZeroFamily, contMDiff_constZeroFamily, DifferentialForm.constZero c — the constant 0-form;
• ★★ DifferentialForm.wedgePow α k — the k-th exterior power of a real 2-form, a 2k-form, by recursion (powEquiv k : Fin (2k) ⊕ Fin 2 ≃ Fin (2(k+1))); its flat twin ContinuousAlternatingMap.wedgePow with ★ wedgePow_compContinuousLinearMap (pullback commutes with the power), wedgePow_smul (homogeneity) and ★ localRep_wedgePow (the local representative of the power is the power of the local representative) — what lifts an invariance of a 2-form to its top power.

Honest scope

⚠️ Only the operations. No algebraic law of the wedge is proved at section level — associativity, graded commutativity, the Leibniz rule with mextDeriv — because none is proved flat (Wedge.lean's honest scope). wedgePow is a definition, and nothing here says it is nonzero.

⚠️ ∞ and 𝓘(ℝ, E) only, inherited from ExteriorDerivative.lean.

Provenance and references. The top-power plan (M2); Alternating/WedgeCLM.lean; Geometry/Manifold/ExteriorDerivative.lean; consumer Geometry/Manifold/Instances/ProjectiveSpaceFubiniStudyForm.lean (fsTopForm); the completed-work ledger.

The wedge of two families

noncomputable def DifferentialForm.wedgeFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} {G : Type u_3} {H : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup H] [NormedSpace ℝ H] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] {ιa : Type u_6} {ιb : Type u_7} [Fintype ιa] [Fintype ιb] [DecidableEq ιa] [DecidableEq ιb] (B : F →L[ℝ] G →L[ℝ] H) (α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ιa]→L[ℝ] Bundle.Trivial M F x) (β : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ιb]→L[ℝ] Bundle.Trivial M G x) (x : M) : TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ιa ⊕ ιb]→L[ℝ] Bundle.Trivial M H x

The wedge of two families of alternating maps on the tangent spaces, fibrewise.

Equations

• DifferentialForm.wedgeFamily B α β x = ContinuousAlternatingMap.wedge B (DifferentialForm.toFlat (α x)) (DifferentialForm.toFlat (β x))

theorem DifferentialForm.toFlat_wedgeFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} {G : Type u_3} {H : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup H] [NormedSpace ℝ H] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] {ιa : Type u_6} {ιb : Type u_7} [Fintype ιa] [Fintype ιb] [DecidableEq ιa] [DecidableEq ιb] (B : F →L[ℝ] G →L[ℝ] H) (α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ιa]→L[ℝ] Bundle.Trivial M F x) (β : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ιb]→L[ℝ] Bundle.Trivial M G x) (x : M) : toFlat (wedgeFamily B α β x) = ContinuousAlternatingMap.wedge B (toFlat (α x)) (toFlat (β x))

theorem DifferentialForm.trivializationAt_wedgeFamily_snd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} {G : Type u_3} {H : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup H] [NormedSpace ℝ H] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ιa : Type u_6} {ιb : Type u_7} [Fintype ιa] [Fintype ιb] [DecidableEq ιa] [DecidableEq ιb] (B : F →L[ℝ] G →L[ℝ] H) (α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ιa]→L[ℝ] Bundle.Trivial M F x) (β : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ιb]→L[ℝ] Bundle.Trivial M G x) (x₀ y : M) (hy : y ∈ (chartAt E x₀).source) : (↑(trivializationAt (E [⋀^ιa ⊕ ιb]→L[ℝ] H) (fun (x : M) => TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ιa ⊕ ιb]→L[ℝ] Bundle.Trivial M H x) x₀) ⟨y, wedgeFamily B α β y⟩).2 = ContinuousAlternatingMap.wedge B (localRep α x₀ (↑(chartAt E x₀) y)) (localRep β x₀ (↑(chartAt E x₀) y))

★ In the chart at x₀, a wedge trivialises to the wedge of the local representatives.

theorem DifferentialForm.localRep_wedgeFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} {G : Type u_3} {H : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup H] [NormedSpace ℝ H] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ιa : Type u_6} {ιb : Type u_7} [Fintype ιa] [Fintype ιb] [DecidableEq ιa] [DecidableEq ιb] (B : F →L[ℝ] G →L[ℝ] H) (α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ιa]→L[ℝ] Bundle.Trivial M F x) (β : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ιb]→L[ℝ] Bundle.Trivial M G x) (x₀ : M) {w : E} (hw : w ∈ (chartAt E x₀).target) : localRep (wedgeFamily B α β) x₀ w = ContinuousAlternatingMap.wedge B (localRep α x₀ w) (localRep β x₀ w)

★ The local representative of a wedge is the wedge of the local representatives.

theorem DifferentialForm.contMDiff_wedgeFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} {G : Type u_3} {H : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup H] [NormedSpace ℝ H] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ιa : Type u_6} {ιb : Type u_7} [Fintype ιa] [Fintype ιb] [DecidableEq ιa] [DecidableEq ιb] (B : F →L[ℝ] G →L[ℝ] H) {α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ιa]→L[ℝ] Bundle.Trivial M F x} {β : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ιb]→L[ℝ] Bundle.Trivial M G x} (hα : ContMDiff (modelWithCornersSelf ℝ E) ((modelWithCornersSelf ℝ E).prod (modelWithCornersSelf ℝ (E [⋀^ιa]→L[ℝ] F))) ↑⊤ fun (x : M) => ⟨x, α x⟩) (hβ : ContMDiff (modelWithCornersSelf ℝ E) ((modelWithCornersSelf ℝ E).prod (modelWithCornersSelf ℝ (E [⋀^ιb]→L[ℝ] G))) ↑⊤ fun (x : M) => ⟨x, β x⟩) : ContMDiff (modelWithCornersSelf ℝ E) ((modelWithCornersSelf ℝ E).prod (modelWithCornersSelf ℝ (E [⋀^ιa ⊕ ιb]→L[ℝ] H))) ↑⊤ fun (x : M) => ⟨x, wedgeFamily B α β x⟩

★★ The wedge of two C^∞ sections is a C^∞ section.

noncomputable def DifferentialForm.wedge {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} {G : Type u_3} {H : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup H] [NormedSpace ℝ H] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ιa : Type u_6} {ιb : Type u_7} [Fintype ιa] [Fintype ιb] [DecidableEq ιa] [DecidableEq ιb] (B : F →L[ℝ] G →L[ℝ] H) (α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) ιa F) (β : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) ιb G) : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) (ιa ⊕ ιb) H

★★ The wedge of two differential forms.

Equations

• DifferentialForm.wedge B α β = { toFun := DifferentialForm.wedgeFamily B (fun (x : M) => α x) fun (x : M) => β x, contMDiff_toFun := ⋯ }

@[simp]

theorem DifferentialForm.wedge_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} {G : Type u_3} {H : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup H] [NormedSpace ℝ H] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ιa : Type u_6} {ιb : Type u_7} [Fintype ιa] [Fintype ιb] [DecidableEq ιa] [DecidableEq ιb] (B : F →L[ℝ] G →L[ℝ] H) (α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) ιa F) (β : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) ιb G) (x : M) : (wedge B α β) x = wedgeFamily B (fun (x : M) => α x) (fun (x : M) => β x) x

Reindexing a family

noncomputable def DifferentialForm.domDomCongrFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] {ι : Type u_8} {ι' : Type u_9} (σ : ι ≃ ι') (α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M F x) (x : M) : TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι']→L[ℝ] Bundle.Trivial M F x

Reindexing a family of alternating maps along an equivalence of index types, fibrewise.

Equations

• DifferentialForm.domDomCongrFamily σ α x = ContinuousAlternatingMap.domDomCongr σ (DifferentialForm.toFlat (α x))

theorem DifferentialForm.toFlat_domDomCongrFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] {ι : Type u_8} {ι' : Type u_9} (σ : ι ≃ ι') (α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M F x) (x : M) : toFlat (domDomCongrFamily σ α x) = ContinuousAlternatingMap.domDomCongr σ (toFlat (α x))

theorem DifferentialForm.trivializationAt_domDomCongrFamily_snd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ι : Type u_8} {ι' : Type u_9} [Fintype ι] [Fintype ι'] (σ : ι ≃ ι') (α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M F x) (x₀ y : M) (hy : y ∈ (chartAt E x₀).source) : (↑(trivializationAt (E [⋀^ι']→L[ℝ] F) (fun (x : M) => TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι']→L[ℝ] Bundle.Trivial M F x) x₀) ⟨y, domDomCongrFamily σ α y⟩).2 = ContinuousAlternatingMap.domDomCongr σ (localRep α x₀ (↑(chartAt E x₀) y))

theorem DifferentialForm.localRep_domDomCongrFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ι : Type u_8} {ι' : Type u_9} [Fintype ι] [Fintype ι'] (σ : ι ≃ ι') (α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M F x) (x₀ : M) {w : E} (hw : w ∈ (chartAt E x₀).target) : localRep (domDomCongrFamily σ α) x₀ w = ContinuousAlternatingMap.domDomCongr σ (localRep α x₀ w)

theorem DifferentialForm.contMDiff_domDomCongrFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ι : Type u_8} {ι' : Type u_9} [Fintype ι] [DecidableEq ι] [Fintype ι'] (σ : ι ≃ ι') {α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M F x} (hα : ContMDiff (modelWithCornersSelf ℝ E) ((modelWithCornersSelf ℝ E).prod (modelWithCornersSelf ℝ (E [⋀^ι]→L[ℝ] F))) ↑⊤ fun (x : M) => ⟨x, α x⟩) : ContMDiff (modelWithCornersSelf ℝ E) ((modelWithCornersSelf ℝ E).prod (modelWithCornersSelf ℝ (E [⋀^ι']→L[ℝ] F))) ↑⊤ fun (x : M) => ⟨x, domDomCongrFamily σ α x⟩

noncomputable def DifferentialForm.domDomCongr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ι : Type u_8} {ι' : Type u_9} [Fintype ι] [DecidableEq ι] [Fintype ι'] (σ : ι ≃ ι') (α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) ι F) : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) ι' F

★ Reindexing a differential form along an equivalence of index types.

Equations

• DifferentialForm.domDomCongr σ α = { toFun := DifferentialForm.domDomCongrFamily σ fun (x : M) => α x, contMDiff_toFun := ⋯ }

@[simp]

theorem DifferentialForm.domDomCongr_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ι : Type u_8} {ι' : Type u_9} [Fintype ι] [DecidableEq ι] [Fintype ι'] (σ : ι ≃ ι') (α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) ι F) (x : M) : (domDomCongr σ α) x = domDomCongrFamily σ (fun (x : M) => α x) x

The constant 0-form

def DifferentialForm.constZeroFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] {ι : Type u_8} [IsEmpty ι] (c : F) (x : M) : TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M F x

The constant 0-form with value c, as a family.

Equations

• DifferentialForm.constZeroFamily c x = ContinuousAlternatingMap.constOfIsEmpty ℝ E ι c

theorem DifferentialForm.trivializationAt_constZeroFamily_snd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ι : Type u_8} [Fintype ι] [IsEmpty ι] (c : F) (x₀ y : M) (hy : y ∈ (chartAt E x₀).source) : (↑(trivializationAt (E [⋀^ι]→L[ℝ] F) (fun (x : M) => TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M F x) x₀) ⟨y, constZeroFamily c y⟩).2 = ContinuousAlternatingMap.constOfIsEmpty ℝ E ι c

theorem DifferentialForm.contMDiff_constZeroFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ι : Type u_8} [Fintype ι] [IsEmpty ι] (c : F) : ContMDiff (modelWithCornersSelf ℝ E) ((modelWithCornersSelf ℝ E).prod (modelWithCornersSelf ℝ (E [⋀^ι]→L[ℝ] F))) ↑⊤ fun (x : M) => ⟨x, constZeroFamily c x⟩

def DifferentialForm.constZero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ι : Type u_8} [Fintype ι] [IsEmpty ι] (c : F) : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) ι F

The constant 0-form with value c.

Equations

• DifferentialForm.constZero c = { toFun := DifferentialForm.constZeroFamily c, contMDiff_toFun := ⋯ }

The iterated power of a real 2-form

def DifferentialForm.powEquiv (k : ℕ) : Fin (2 * k) ⊕ Fin 2 ≃ Fin (2 * (k + 1))

The equivalence Fin (2k) ⊕ Fin 2 ≃ Fin (2(k+1)) the iterated power re-indexes along.

Equations

• DifferentialForm.powEquiv k = finSumFinEquiv.trans (finCongr ⋯)

def DifferentialForm.wedgePow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] (α₂ : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) (Fin 2) ℝ) (k : ℕ) : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) (Fin (2 * k)) ℝ

★★ The k-th exterior power of a real 2-form, as a 2k-form.

Equations

• α₂.wedgePow 0 = DifferentialForm.domDomCongr (finCongr DifferentialForm.wedgePow._proof_3) (DifferentialForm.constZero 1)
• α₂.wedgePow k.succ = DifferentialForm.domDomCongr (DifferentialForm.powEquiv k) (DifferentialForm.wedge (ContinuousLinearMap.mul ℝ ℝ) (α₂.wedgePow k) α₂)

@[simp]

theorem DifferentialForm.wedgePow_succ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] (α₂ : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) (Fin 2) ℝ) (k : ℕ) : α₂.wedgePow (k + 1) = domDomCongr (powEquiv k) (wedge (ContinuousLinearMap.mul ℝ ℝ) (α₂.wedgePow k) α₂)

The flat iterated power, and the local representative of a power

def ContinuousAlternatingMap.wedgePow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (α : E [⋀^Fin 2]→L[ℝ] ℝ) (k : ℕ) : E [⋀^Fin (2 * k)]→L[ℝ] ℝ

The k-th exterior power of a flat real 2-form, as a 2k-form (same recursion as DifferentialForm.wedgePow).

Equations

• α.wedgePow 0 = ContinuousAlternatingMap.domDomCongr (finCongr DifferentialForm.wedgePow._proof_3) (ContinuousAlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
• α.wedgePow k.succ = ContinuousAlternatingMap.domDomCongr (DifferentialForm.powEquiv k) (ContinuousAlternatingMap.wedge (ContinuousLinearMap.mul ℝ ℝ) (α.wedgePow k) α)

theorem ContinuousAlternatingMap.wedgePow_compContinuousLinearMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_10} [NormedAddCommGroup E'] [NormedSpace ℝ E'] (α : E [⋀^Fin 2]→L[ℝ] ℝ) (L : E' →L[ℝ] E) (k : ℕ) : (α.wedgePow k).compContinuousLinearMap L = (α.compContinuousLinearMap L).wedgePow k

Pullback commutes with the iterated power.

theorem ContinuousAlternatingMap.wedgePow_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ) (α : E [⋀^Fin 2]→L[ℝ] ℝ) (k : ℕ) : (c • α).wedgePow k = c ^ k • α.wedgePow k

The iterated power is homogeneous of degree k: (c • α)^{∧k} = c^k • α^{∧k}.

theorem DifferentialForm.localRep_constZeroFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ι : Type u_8} [Fintype ι] [IsEmpty ι] (c : F) (x₀ : M) {w : E} (hw : w ∈ (chartAt E x₀).target) : localRep (constZeroFamily c) x₀ w = ContinuousAlternatingMap.constOfIsEmpty ℝ E ι c

theorem DifferentialForm.localRep_wedgePow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] (α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) (Fin 2) ℝ) (x₀ : M) {w : E} (hw : w ∈ (chartAt E x₀).target) (k : ℕ) : localRep (fun (x : M) => (α.wedgePow k) x) x₀ w = (localRep (fun (x : M) => α x) x₀ w).wedgePow k

★ The local representative of the k-th power is the k-th power of the local representative.