Wedge products of bundle-valued rough differential forms

The paired wedge combines two rough forms with values in topological vector-bundle fibres by a continuous bilinear pairing on each fibre. Its formula is the signed permutation sum divided by the two factorials. This construction uses no norm or trivialization on the tangent fibres. Pullback carries both the forms and their pairing to the source manifold. The output fibres need only continuity of multiplication by each fixed scalar. A pairing that turns multiplication by one scalar into multiplication by another, such as a complex-bilinear pairing or a Hermitian metric, makes the wedge semilinear in the same way.

The normalization follows Lee, Introduction to Smooth Manifolds, second edition, Chapter 14. The algebraic alternatization follows the paired-wedge construction of Yury Kudryashov's DeRhamCohomology project and Mathlib's MultilinearMap.alternatization.

noncomputable def TauCeti.bundleWedgeWith {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → TopologicalSpace (V₃ x)] [∀ (x : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₃ x)] {k l : ℕ} (μ : (x : M) → V₁ x →L[ℝ] V₂ x →L[ℝ] V₃ x) (hμ : ∀ (x : M), Continuous (Function.uncurry fun (a : V₁ x) (b : V₂ x) => ((μ x) a) b)) (φ : RoughBundleForm I M V₁ k) (ψ : RoughBundleForm I M V₂ l) : RoughBundleForm I M V₃ (k + l)

The paired wedge of rough bundle-valued forms, normalized so that one-forms multiply by the usual two-term alternating product.

@[simp]

theorem TauCeti.bundleWedgeWith_apply' {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → TopologicalSpace (V₃ x)] [∀ (x : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₃ x)] {k l : ℕ} (μ : (x : M) → V₁ x →L[ℝ] V₂ x →L[ℝ] V₃ x) (hμ : ∀ (x : M), Continuous (Function.uncurry fun (a : V₁ x) (b : V₂ x) => ((μ x) a) b)) (φ : RoughBundleForm I M V₁ k) (ψ : RoughBundleForm I M V₂ l) (x : M) : bundleWedgeWith μ hμ φ ψ x = ContinuousAlternatingMap.pairedWedge (μ x) ⋯ (φ x) (ψ x)

At each point, the bundle wedge is the paired wedge of the two fibre values.

theorem TauCeti.bundleWedgeWith_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → TopologicalSpace (V₃ x)] [∀ (x : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₃ x)] {k l : ℕ} (μ : (x : M) → V₁ x →L[ℝ] V₂ x →L[ℝ] V₃ x) (hμ : ∀ (x : M), Continuous (Function.uncurry fun (a : V₁ x) (b : V₂ x) => ((μ x) a) b)) (φ : RoughBundleForm I M V₁ k) (ψ : RoughBundleForm I M V₂ l) (x : M) (v : Fin (k + l) → TangentSpace I x) : (bundleWedgeWith μ hμ φ ψ x) v = (↑k.factorial * ↑l.factorial)⁻¹ • ∑ σ : Equiv.Perm (Fin (k + l)), Equiv.Perm.sign σ • ((μ x) ((φ x) fun (i : Fin k) => v (σ (Fin.castAdd l i)))) ((ψ x) fun (j : Fin l) => v (σ (Fin.natAdd k j)))

The fibrewise paired wedge is the signed permutation sum.

theorem TauCeti.bundleWedgeWith_apply_one_one {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → TopologicalSpace (V₃ x)] [∀ (x : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₃ x)] (μ : (x : M) → V₁ x →L[ℝ] V₂ x →L[ℝ] V₃ x) (hμ : ∀ (x : M), Continuous (Function.uncurry fun (a : V₁ x) (b : V₂ x) => ((μ x) a) b)) (φ : RoughBundleForm I M V₁ 1) (ψ : RoughBundleForm I M V₂ 1) (x : M) (v w : TangentSpace I x) : (bundleWedgeWith μ hμ φ ψ x) ![v, w] = ((μ x) ((φ x) ![v])) ((ψ x) ![w]) - ((μ x) ((φ x) ![w])) ((ψ x) ![v])

On two one-forms, the fibrewise wedge is the usual alternating product.

theorem TauCeti.bundleWedgeWith_flip {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → TopologicalSpace (V₃ x)] [∀ (x : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₃ x)] {k l : ℕ} [∀ (x : M), IsTopologicalAddGroup (V₂ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₂ x)] (μ : (x : M) → V₁ x →L[ℝ] V₂ x →L[ℝ] V₃ x) (hμ : ∀ (x : M), Continuous (Function.uncurry fun (a : V₁ x) (b : V₂ x) => ((μ x) a) b)) (φ : RoughBundleForm I M V₁ k) (ψ : RoughBundleForm I M V₂ l) (x : M) (v : Fin (k + l) → TangentSpace I x) : (bundleWedgeWith μ hμ φ ψ x) v = (-1) ^ (k * l) • (bundleWedgeWith (fun (y : M) => (μ y).pairingFlip ⋯) ⋯ ψ φ x) (v ∘ Fin.cast ⋯)

Swapping the factors of a fibrewise paired wedge flips the pairing and contributes the graded sign. This applies to arbitrary value bundles, with no norm on the tangent fibres or values.

@[simp]

theorem TauCeti.bundleWedgeWith_add_left {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → TopologicalSpace (V₃ x)] [∀ (x : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₃ x)] {k l : ℕ} [∀ (x : M), ContinuousAdd (V₁ x)] (μ : (x : M) → V₁ x →L[ℝ] V₂ x →L[ℝ] V₃ x) (hμ : ∀ (x : M), Continuous (Function.uncurry fun (a : V₁ x) (b : V₂ x) => ((μ x) a) b)) (φ φ' : RoughBundleForm I M V₁ k) (ψ : RoughBundleForm I M V₂ l) : bundleWedgeWith μ hμ (φ + φ') ψ = bundleWedgeWith μ hμ φ ψ + bundleWedgeWith μ hμ φ' ψ

The fibrewise paired wedge is additive in its first form.

@[simp]

theorem TauCeti.bundleWedgeWith_add_right {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → TopologicalSpace (V₃ x)] [∀ (x : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₃ x)] {k l : ℕ} [∀ (x : M), ContinuousAdd (V₂ x)] (μ : (x : M) → V₁ x →L[ℝ] V₂ x →L[ℝ] V₃ x) (hμ : ∀ (x : M), Continuous (Function.uncurry fun (a : V₁ x) (b : V₂ x) => ((μ x) a) b)) (φ : RoughBundleForm I M V₁ k) (ψ ψ' : RoughBundleForm I M V₂ l) : bundleWedgeWith μ hμ φ (ψ + ψ') = bundleWedgeWith μ hμ φ ψ + bundleWedgeWith μ hμ φ ψ'

The fibrewise paired wedge is additive in its second form.

@[simp]

theorem TauCeti.bundleWedgeWith_smul_left {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → TopologicalSpace (V₃ x)] [∀ (x : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₃ x)] {k l : ℕ} [∀ (x : M), ContinuousConstSMul ℝ (V₁ x)] (μ : (x : M) → V₁ x →L[ℝ] V₂ x →L[ℝ] V₃ x) (hμ : ∀ (x : M), Continuous (Function.uncurry fun (a : V₁ x) (b : V₂ x) => ((μ x) a) b)) (c : ℝ) (φ : RoughBundleForm I M V₁ k) (ψ : RoughBundleForm I M V₂ l) : bundleWedgeWith μ hμ (c • φ) ψ = c • bundleWedgeWith μ hμ φ ψ

The fibrewise paired wedge respects scalar multiplication in its first form.

@[simp]

theorem TauCeti.bundleWedgeWith_smul_right {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → TopologicalSpace (V₃ x)] [∀ (x : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₃ x)] {k l : ℕ} [∀ (x : M), ContinuousConstSMul ℝ (V₂ x)] (μ : (x : M) → V₁ x →L[ℝ] V₂ x →L[ℝ] V₃ x) (hμ : ∀ (x : M), Continuous (Function.uncurry fun (a : V₁ x) (b : V₂ x) => ((μ x) a) b)) (c : ℝ) (φ : RoughBundleForm I M V₁ k) (ψ : RoughBundleForm I M V₂ l) : bundleWedgeWith μ hμ φ (c • ψ) = c • bundleWedgeWith μ hμ φ ψ

The fibrewise paired wedge respects scalar multiplication in its second form.

theorem TauCeti.bundleWedgeWith_smul_left_of_map_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → TopologicalSpace (V₃ x)] [∀ (x : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₃ x)] {k l : ℕ} {S : Type u_10} {S' : Type u_11} [Monoid S] [(x : M) → DistribMulAction S (V₁ x)] [∀ (x : M), ContinuousConstSMul S (V₁ x)] [∀ (x : M), SMulCommClass ℝ S (V₁ x)] [Monoid S'] [(x : M) → DistribMulAction S' (V₃ x)] [∀ (x : M), ContinuousConstSMul S' (V₃ x)] [∀ (x : M), SMulCommClass ℝ S' (V₃ x)] (μ : (x : M) → V₁ x →L[ℝ] V₂ x →L[ℝ] V₃ x) (hμ : ∀ (x : M), Continuous (Function.uncurry fun (a : V₁ x) (b : V₂ x) => ((μ x) a) b)) {c : S} {d : S'} (hcd : ∀ (x : M) (a : V₁ x) (b : V₂ x), ((μ x) (c • a)) b = d • ((μ x) a) b) (φ : RoughBundleForm I M V₁ k) (ψ : RoughBundleForm I M V₂ l) : bundleWedgeWith μ hμ (c • φ) ψ = d • bundleWedgeWith μ hμ φ ψ

If each fibrewise pairing turns multiplication by c in its first argument into multiplication by d, then so does the fibrewise paired wedge in its first form. This covers complex-bilinear pairings, and pairings that are conjugate-linear in the first argument, such as Hermitian metrics.

theorem TauCeti.bundleWedgeWith_smul_right_of_map_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → TopologicalSpace (V₃ x)] [∀ (x : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₃ x)] {k l : ℕ} {S : Type u_10} {S' : Type u_11} [Monoid S] [(x : M) → DistribMulAction S (V₂ x)] [∀ (x : M), ContinuousConstSMul S (V₂ x)] [∀ (x : M), SMulCommClass ℝ S (V₂ x)] [Monoid S'] [(x : M) → DistribMulAction S' (V₃ x)] [∀ (x : M), ContinuousConstSMul S' (V₃ x)] [∀ (x : M), SMulCommClass ℝ S' (V₃ x)] (μ : (x : M) → V₁ x →L[ℝ] V₂ x →L[ℝ] V₃ x) (hμ : ∀ (x : M), Continuous (Function.uncurry fun (a : V₁ x) (b : V₂ x) => ((μ x) a) b)) {c : S} {d : S'} (hcd : ∀ (x : M) (a : V₁ x) (b : V₂ x), ((μ x) a) (c • b) = d • ((μ x) a) b) (φ : RoughBundleForm I M V₁ k) (ψ : RoughBundleForm I M V₂ l) : bundleWedgeWith μ hμ φ (c • ψ) = d • bundleWedgeWith μ hμ φ ψ

If each fibrewise pairing turns multiplication by c in its second argument into multiplication by d, then so does the fibrewise paired wedge in its second form.

@[simp]

theorem TauCeti.bundleWedgeWith_zero_left {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → TopologicalSpace (V₃ x)] [∀ (x : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₃ x)] {k l : ℕ} (μ : (x : M) → V₁ x →L[ℝ] V₂ x →L[ℝ] V₃ x) (hμ : ∀ (x : M), Continuous (Function.uncurry fun (a : V₁ x) (b : V₂ x) => ((μ x) a) b)) (ψ : RoughBundleForm I M V₂ l) : bundleWedgeWith μ hμ 0 ψ = 0

The fibrewise paired wedge vanishes when its first form is zero.

@[simp]

theorem TauCeti.bundleWedgeWith_zero_right {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → TopologicalSpace (V₃ x)] [∀ (x : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₃ x)] {k l : ℕ} (μ : (x : M) → V₁ x →L[ℝ] V₂ x →L[ℝ] V₃ x) (hμ : ∀ (x : M), Continuous (Function.uncurry fun (a : V₁ x) (b : V₂ x) => ((μ x) a) b)) (φ : RoughBundleForm I M V₁ k) : bundleWedgeWith μ hμ φ 0 = 0

The fibrewise paired wedge vanishes when its second form is zero.

theorem TauCeti.bundleMpullback_wedgeWith {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → TopologicalSpace (V₃ x)] [∀ (x : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₃ x)] {k l : ℕ} (f : M' → M) (μ : (x : M) → V₁ x →L[ℝ] V₂ x →L[ℝ] V₃ x) (hμ : ∀ (x : M), Continuous (Function.uncurry fun (a : V₁ x) (b : V₂ x) => ((μ x) a) b)) (φ : RoughBundleForm I M V₁ k) (ψ : RoughBundleForm I M V₂ l) : bundleMpullback I' I f (bundleWedgeWith μ hμ φ ψ) = bundleWedgeWith (fun (y : M') => μ (f y)) ⋯ (bundleMpullback I' I f φ) (bundleMpullback I' I f ψ)

Pullback of a paired wedge pulls back its fibrewise pairing as well as both forms.

theorem TauCeti.bundleMpullbackWithin_wedgeWith {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {V₁ : M → Type u_7} {V₂ : M → Type u_8} {V₃ : M → Type u_9} [(x : M) → AddCommGroup (V₁ x)] [(x : M) → Module ℝ (V₁ x)] [(x : M) → TopologicalSpace (V₁ x)] [(x : M) → AddCommGroup (V₂ x)] [(x : M) → Module ℝ (V₂ x)] [(x : M) → TopologicalSpace (V₂ x)] [(x : M) → AddCommGroup (V₃ x)] [(x : M) → Module ℝ (V₃ x)] [(x : M) → TopologicalSpace (V₃ x)] [∀ (x : M), IsTopologicalAddGroup (V₃ x)] [∀ (x : M), ContinuousConstSMul ℝ (V₃ x)] {k l : ℕ} (f : M' → M) (s : Set M') (μ : (x : M) → V₁ x →L[ℝ] V₂ x →L[ℝ] V₃ x) (hμ : ∀ (x : M), Continuous (Function.uncurry fun (a : V₁ x) (b : V₂ x) => ((μ x) a) b)) (φ : RoughBundleForm I M V₁ k) (ψ : RoughBundleForm I M V₂ l) : bundleMpullbackWithin I' I f s (bundleWedgeWith μ hμ φ ψ) = bundleWedgeWith (fun (y : M') => μ (f y)) ⋯ (bundleMpullbackWithin I' I f s φ) (bundleMpullbackWithin I' I f s ψ)

Within-set pullback likewise commutes with the paired wedge without regularity assumptions.

noncomputable def TauCeti.RoughForm.wedgeWith {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ l) : RoughForm I M F₃ (k + l)

The paired wedge of fixed-coefficient rough forms. It is the trivial-value-bundle specialization of bundleWedgeWith.

theorem TauCeti.RoughForm.wedgeWith_apply' {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ l) (x : M) : wedgeWith μ φ ψ x = ContinuousAlternatingMap.pairedWedge μ ⋯ (φ x) (ψ x)

A fixed-coefficient wedge evaluates through the pointwise paired wedge.

theorem TauCeti.RoughForm.wedgeWith_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ l) (x : M) (v : Fin (k + l) → TangentSpace I x) : (wedgeWith μ φ ψ x) v = (↑k.factorial * ↑l.factorial)⁻¹ • ∑ σ : Equiv.Perm (Fin (k + l)), Equiv.Perm.sign σ • (μ ((φ x) fun (i : Fin k) => v (σ (Fin.castAdd l i)))) ((ψ x) fun (j : Fin l) => v (σ (Fin.natAdd k j)))

Evaluation of the fixed-coefficient paired wedge.

@[simp]

theorem TauCeti.RoughForm.wedgeWith_apply_zero_right {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ 0) (x : M) (v : Fin k → TangentSpace I x) : (wedgeWith μ φ ψ x) v = (μ ((φ x) v)) ((ψ x) 0)

Pairing a rough form with a degree-zero form pairs its value with the function value.

theorem TauCeti.RoughForm.wedgeWith_apply_one_one {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : RoughForm I M F₁ 1) (ψ : RoughForm I M F₂ 1) (x : M) (v w : TangentSpace I x) : (wedgeWith μ φ ψ x) ![v, w] = (μ ((φ x) ![v])) ((ψ x) ![w]) - (μ ((φ x) ![w])) ((ψ x) ![v])

Evaluation of the paired rough-form wedge on two one-forms.

@[simp]

theorem TauCeti.RoughForm.wedgeWith_add_left {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ φ' : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ l) : wedgeWith μ (φ + φ') ψ = wedgeWith μ φ ψ + wedgeWith μ φ' ψ

The paired rough-form wedge is additive in its first form.

@[simp]

theorem TauCeti.RoughForm.wedgeWith_add_right {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : RoughForm I M F₁ k) (ψ ψ' : RoughForm I M F₂ l) : wedgeWith μ φ (ψ + ψ') = wedgeWith μ φ ψ + wedgeWith μ φ ψ'

The paired rough-form wedge is additive in its second form.

@[simp]

theorem TauCeti.RoughForm.wedgeWith_smul_left {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (c : ℝ) (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ l) : wedgeWith μ (c • φ) ψ = c • wedgeWith μ φ ψ

The paired rough-form wedge respects scalar multiplication in its first form.

@[simp]

theorem TauCeti.RoughForm.wedgeWith_smul_right {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (c : ℝ) (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ l) : wedgeWith μ φ (c • ψ) = c • wedgeWith μ φ ψ

The paired rough-form wedge respects scalar multiplication in its second form.

theorem TauCeti.RoughForm.wedgeWith_smul_left_of_map_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} {S : Type u_10} {S' : Type u_11} [Monoid S] [DistribMulAction S F₁] [ContinuousConstSMul S F₁] [SMulCommClass ℝ S F₁] [Monoid S'] [DistribMulAction S' F₃] [ContinuousConstSMul S' F₃] [SMulCommClass ℝ S' F₃] (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) {c : S} {d : S'} (hcd : ∀ (a : F₁) (b : F₂), (μ (c • a)) b = d • (μ a) b) (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ l) : wedgeWith μ (c • φ) ψ = d • wedgeWith μ φ ψ

If the pairing turns multiplication by c in its first argument into multiplication by d, then so does the paired rough-form wedge in its first form. For a complex-bilinear pairing of complex coefficient spaces this is complex-linearity in the first form.

theorem TauCeti.RoughForm.wedgeWith_smul_right_of_map_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} {S : Type u_10} {S' : Type u_11} [Monoid S] [DistribMulAction S F₂] [ContinuousConstSMul S F₂] [SMulCommClass ℝ S F₂] [Monoid S'] [DistribMulAction S' F₃] [ContinuousConstSMul S' F₃] [SMulCommClass ℝ S' F₃] (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) {c : S} {d : S'} (hcd : ∀ (a : F₁) (b : F₂), (μ a) (c • b) = d • (μ a) b) (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ l) : wedgeWith μ φ (c • ψ) = d • wedgeWith μ φ ψ

If the pairing turns multiplication by c in its second argument into multiplication by d, then so does the paired rough-form wedge in its second form. For a complex-bilinear pairing of complex coefficient spaces this is complex-linearity in the second form.

@[simp]

theorem TauCeti.RoughForm.wedgeWith_zero_left {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (ψ : RoughForm I M F₂ l) : wedgeWith μ 0 ψ = 0

The paired rough-form wedge vanishes when its first form is zero.

@[simp]

theorem TauCeti.RoughForm.wedgeWith_zero_right {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : RoughForm I M F₁ k) : wedgeWith μ φ 0 = 0

The paired rough-form wedge vanishes when its second form is zero.

theorem TauCeti.RoughForm.tsupport_wedgeWith_subset_left {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ l) : tsupport (wedgeWith μ φ ψ) ⊆ tsupport φ

The paired rough-form wedge is supported in the support of its first form.

theorem TauCeti.RoughForm.tsupport_wedgeWith_subset_right {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ l) : tsupport (wedgeWith μ φ ψ) ⊆ tsupport ψ

The paired rough-form wedge is supported in the support of its second form.

theorem TauCeti.RoughForm.wedgeWith_flip {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ l) (x : M) (v : Fin (k + l) → TangentSpace I x) : (wedgeWith μ φ ψ x) v = (-1) ^ (k * l) • (wedgeWith μ.flip ψ φ x) (v ∘ Fin.cast ⋯)

Swapping the factors of a paired rough-form wedge flips the pairing and contributes the graded sign. The argument reindexing is the canonical cast between the two degree sums.

theorem TauCeti.RoughForm.wedgeWith_comm {E : Type u_1} {H : Type u_2} {M : Type u_3} {F₁ : Type u_7} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₁ →L[ℝ] F₃) (hμ : ∀ (a b : F₁), (μ a) b = (μ b) a) (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₁ l) (x : M) (v : Fin (k + l) → TangentSpace I x) : (wedgeWith μ φ ψ x) v = (-1) ^ (k * l) • (wedgeWith μ ψ φ x) (v ∘ Fin.cast ⋯)

A symmetric fibrewise pairing gives the graded-commutativity identity for rough forms.

noncomputable def TauCeti.RoughForm.wedge {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k l : ℕ} (φ : RoughForm I M ℝ k) (ψ : RoughForm I M ℝ l) : RoughForm I M ℝ (k + l)

The real wedge of rough forms uses multiplication as its fibrewise pairing.

theorem TauCeti.RoughForm.wedge_def {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k l : ℕ} (φ : RoughForm I M ℝ k) (ψ : RoughForm I M ℝ l) : φ.wedge ψ = wedgeWith (ContinuousLinearMap.mul ℝ ℝ) φ ψ

The real-valued wedge specializes the paired wedge to multiplication.

theorem TauCeti.RoughForm.wedge_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k l : ℕ} (φ : RoughForm I M ℝ k) (ψ : RoughForm I M ℝ l) (x : M) (v : Fin (k + l) → TangentSpace I x) : (φ.wedge ψ x) v = (↑k.factorial * ↑l.factorial)⁻¹ • ∑ σ : Equiv.Perm (Fin (k + l)), Equiv.Perm.sign σ • (((φ x) fun (i : Fin k) => v (σ (Fin.castAdd l i))) * (ψ x) fun (j : Fin l) => v (σ (Fin.natAdd k j)))

Evaluation of the real-valued rough-form wedge in every degree.

@[simp]

theorem TauCeti.RoughForm.wedge_apply_zero_right {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} (φ : RoughForm I M ℝ k) (ψ : RoughForm I M ℝ 0) (x : M) (v : Fin k → TangentSpace I x) : (φ.wedge ψ x) v = (φ x) v * (ψ x) 0

Wedging a real-valued rough form with a degree-zero form multiplies its value by the function value.

@[simp]

theorem TauCeti.RoughForm.wedge_apply_one_one {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} (φ ψ : RoughForm I M ℝ 1) (x : M) (v w : TangentSpace I x) : (φ.wedge ψ x) ![v, w] = (φ x) ![v] * (ψ x) ![w] - (φ x) ![w] * (ψ x) ![v]

The wedge of real-valued one-forms has the determinant normalization.

theorem TauCeti.RoughForm.ofFunction_wedge_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {l : ℕ} (f : M → ℝ) (φ : RoughForm I M ℝ l) (x : M) (v : Fin (0 + l) → TangentSpace I x) : ((ofFunction I f).wedge φ x) v = f x * (φ x) fun (i : Fin l) => v (Fin.cast ⋯ i)

The wedge of the 0-form of a function f with an l-form φ is the pointwise product f • φ, read in degree 0 + l.

@[simp]

theorem TauCeti.RoughForm.wedge_add_left {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k l : ℕ} (φ φ' : RoughForm I M ℝ k) (ψ : RoughForm I M ℝ l) : (φ + φ').wedge ψ = φ.wedge ψ + φ'.wedge ψ

The real wedge is additive in its first form.

@[simp]

theorem TauCeti.RoughForm.wedge_add_right {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k l : ℕ} (φ : RoughForm I M ℝ k) (ψ ψ' : RoughForm I M ℝ l) : φ.wedge (ψ + ψ') = φ.wedge ψ + φ.wedge ψ'

The real wedge is additive in its second form.

@[simp]

theorem TauCeti.RoughForm.wedge_smul_left {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k l : ℕ} (c : ℝ) (φ : RoughForm I M ℝ k) (ψ : RoughForm I M ℝ l) : (c • φ).wedge ψ = c • φ.wedge ψ

The real wedge respects scalar multiplication in its first form.

@[simp]

theorem TauCeti.RoughForm.wedge_smul_right {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k l : ℕ} (c : ℝ) (φ : RoughForm I M ℝ k) (ψ : RoughForm I M ℝ l) : φ.wedge (c • ψ) = c • φ.wedge ψ

The real wedge respects scalar multiplication in its second form.

@[simp]

theorem TauCeti.RoughForm.wedge_zero_left {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k l : ℕ} (ψ : RoughForm I M ℝ l) : wedge 0 ψ = 0

The real wedge vanishes when its first form is zero.

@[simp]

theorem TauCeti.RoughForm.wedge_zero_right {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k l : ℕ} (φ : RoughForm I M ℝ k) : φ.wedge 0 = 0

The real wedge vanishes when its second form is zero.

theorem TauCeti.RoughForm.wedge_comm {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k l : ℕ} (φ : RoughForm I M ℝ k) (ψ : RoughForm I M ℝ l) (x : M) (v : Fin (k + l) → TangentSpace I x) : (φ.wedge ψ x) v = (-1) ^ (k * l) • (ψ.wedge φ x) (v ∘ Fin.cast ⋯)

Real-valued rough forms commute with the usual graded sign.

@[simp]

theorem TauCeti.RoughForm.wedge_ofFunction {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} (φ : RoughForm I M ℝ k) (f : M → ℝ) : φ.wedge (ofFunction I f) = fun (x : M) => f x • φ x

Wedging with the 0-form of a function on the right multiplies a form pointwise by the function.

theorem TauCeti.bundleWedgeWith_trivial {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k l : ℕ} {F₁ : Type u_10} {F₂ : Type u_11} {F₃ : Type u_12} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ l) : bundleWedgeWith (fun (x : M) => μ) ⋯ φ ψ = RoughForm.wedgeWith μ φ ψ

On a trivial value bundle, the bundle wedge is the fixed-coefficient rough-form wedge.

theorem TauCeti.bundleMpullbackWithin_roughFormWedgeWith {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (f : M' → M) (s : Set M') (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ l) : bundleMpullbackWithin I' I f s (RoughForm.wedgeWith μ φ ψ) = RoughForm.wedgeWith μ (bundleMpullbackWithin I' I f s φ) (bundleMpullbackWithin I' I f s ψ)

Within-set pullback preserves the paired wedge of fixed-coefficient rough forms.

theorem TauCeti.bundleMpullbackWithin_roughFormWedge {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k l : ℕ} (f : M' → M) (s : Set M') (φ : RoughForm I M ℝ k) (ψ : RoughForm I M ℝ l) : bundleMpullbackWithin I' I f s (φ.wedge ψ) = RoughForm.wedge (bundleMpullbackWithin I' I f s φ) (bundleMpullbackWithin I' I f s ψ)

Within-set pullback preserves the real-valued rough-form wedge.

theorem TauCeti.mpullback_wedgeWith {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F₁ : Type u_7} {F₂ : Type u_8} {F₃ : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (f : M' → M) (φ : RoughForm I M F₁ k) (ψ : RoughForm I M F₂ l) : mpullback I' I f (RoughForm.wedgeWith μ φ ψ) = RoughForm.wedgeWith μ (mpullback I' I f φ) (mpullback I' I f ψ)

Pullback preserves the paired wedge of fixed-coefficient rough forms.

theorem TauCeti.mpullback_wedge {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k l : ℕ} (f : M' → M) (φ : RoughForm I M ℝ k) (ψ : RoughForm I M ℝ l) : mpullback I' I f (φ.wedge ψ) = (mpullback I' I f φ).wedge (mpullback I' I f ψ)

Pullback preserves the real-valued rough-form wedge.