Scalar and algebra-valued wedge products

The ordinary wedge of real-valued forms and the wedge of forms valued in a normed real algebra are the multiplication specializations of the paired wedge. They use its determinant normalization: the wedge of two one-forms evaluates as a two-term determinant. The scalar product is graded commutative, while the algebra-valued product is graded commutative when the algebra is commutative.

The convention follows John M. Lee, Introduction to Smooth Manifolds, second edition, Chapter 14. The underlying paired construction is ContinuousAlternatingMap.pairedWedge.

noncomputable def ContinuousAlternatingMap.wedge {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} (φ : E [⋀^Fin k]→L[ℝ] ℝ) (ψ : E [⋀^Fin l]→L[ℝ] ℝ) : E [⋀^Fin (k + l)]→L[ℝ] ℝ

The real-valued wedge product, normalized so that the wedge of two covectors is their two-term determinant.

theorem ContinuousAlternatingMap.wedge_def {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} (φ : E [⋀^Fin k]→L[ℝ] ℝ) (ψ : E [⋀^Fin l]→L[ℝ] ℝ) : φ.wedge ψ = pairedWedge (ContinuousLinearMap.mul ℝ ℝ) ⋯ φ ψ

The real wedge is the paired wedge for multiplication.

@[simp]

theorem ContinuousAlternatingMap.wedge_apply_one_one {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (φ ψ : E [⋀^Fin 1]→L[ℝ] ℝ) (v w : E) : (φ.wedge ψ) ![v, w] = φ ![v] * ψ ![w] - φ ![w] * ψ ![v]

The wedge of two real one-forms evaluates as a determinant.

@[simp]

theorem ContinuousAlternatingMap.wedge_add_left {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} (φ φ' : E [⋀^Fin k]→L[ℝ] ℝ) (ψ : E [⋀^Fin l]→L[ℝ] ℝ) : (φ + φ').wedge ψ = φ.wedge ψ + φ'.wedge ψ

The real wedge is additive in its first argument.

@[simp]

theorem ContinuousAlternatingMap.wedge_add_right {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} (φ : E [⋀^Fin k]→L[ℝ] ℝ) (ψ ψ' : E [⋀^Fin l]→L[ℝ] ℝ) : φ.wedge (ψ + ψ') = φ.wedge ψ + φ.wedge ψ'

The real wedge is additive in its second argument.

@[simp]

theorem ContinuousAlternatingMap.wedge_smul_left {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} (c : ℝ) (φ : E [⋀^Fin k]→L[ℝ] ℝ) (ψ : E [⋀^Fin l]→L[ℝ] ℝ) : (c • φ).wedge ψ = c • φ.wedge ψ

The real wedge respects scalar multiplication in its first argument.

@[simp]

theorem ContinuousAlternatingMap.wedge_smul_right {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} (c : ℝ) (φ : E [⋀^Fin k]→L[ℝ] ℝ) (ψ : E [⋀^Fin l]→L[ℝ] ℝ) : φ.wedge (c • ψ) = c • φ.wedge ψ

The real wedge respects scalar multiplication in its second argument.

theorem ContinuousAlternatingMap.norm_wedge_le {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} (φ : E [⋀^Fin k]→L[ℝ] ℝ) (ψ : E [⋀^Fin l]→L[ℝ] ℝ) : ‖φ.wedge ψ‖ ≤ ↑((k + l).choose k) * ‖φ‖ * ‖ψ‖

The real wedge obeys the binomial operator-norm bound.

@[simp]

theorem ContinuousAlternatingMap.wedge_compContinuousLinearMap {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} {E' : Type u_2} [SeminormedAddCommGroup E'] [NormedSpace ℝ E'] (f : E' →L[ℝ] E) (φ : E [⋀^Fin k]→L[ℝ] ℝ) (ψ : E [⋀^Fin l]→L[ℝ] ℝ) : (φ.compContinuousLinearMap f).wedge (ψ.compContinuousLinearMap f) = (φ.wedge ψ).compContinuousLinearMap f

Pulling both real forms back along a continuous linear map commutes with wedge.

theorem ContinuousAlternatingMap.wedge_comm {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} (φ : E [⋀^Fin k]→L[ℝ] ℝ) (ψ : E [⋀^Fin l]→L[ℝ] ℝ) (v : Fin (k + l) → E) : (φ.wedge ψ) v = (-1) ^ (k * l) • (ψ.wedge φ) (v ∘ Fin.cast ⋯)

The real wedge is graded commutative.

theorem ContinuousAlternatingMap.wedge_assoc {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l m : ℕ} (φ : E [⋀^Fin k]→L[ℝ] ℝ) (ψ : E [⋀^Fin l]→L[ℝ] ℝ) (χ : E [⋀^Fin m]→L[ℝ] ℝ) (v : Fin (k + l + m) → E) : ((φ.wedge ψ).wedge χ) v = (φ.wedge (ψ.wedge χ)) (v ∘ Fin.cast ⋯)

The real wedge is associative, up to the canonical reassociation of its degree.

noncomputable def ContinuousAlternatingMap.wedgeMul {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} {A : Type u_2} [NormedRing A] [NormedAlgebra ℝ A] (φ : E [⋀^Fin k]→L[ℝ] A) (ψ : E [⋀^Fin l]→L[ℝ] A) : E [⋀^Fin (k + l)]→L[ℝ] A

The wedge of forms valued in a normed real algebra, using multiplication in the algebra.

theorem ContinuousAlternatingMap.wedgeMul_def {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} {A : Type u_2} [NormedRing A] [NormedAlgebra ℝ A] (φ : E [⋀^Fin k]→L[ℝ] A) (ψ : E [⋀^Fin l]→L[ℝ] A) : φ.wedgeMul ψ = pairedWedge (ContinuousLinearMap.mul ℝ A) ⋯ φ ψ

The algebra-valued wedge is the paired wedge for multiplication.

@[simp]

theorem ContinuousAlternatingMap.wedgeMul_apply_one_one {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {A : Type u_2} [NormedRing A] [NormedAlgebra ℝ A] (φ ψ : E [⋀^Fin 1]→L[ℝ] A) (v w : E) : (φ.wedgeMul ψ) ![v, w] = φ ![v] * ψ ![w] - φ ![w] * ψ ![v]

The algebra-valued wedge of two one-forms is the antisymmetrized product.

@[simp]

theorem ContinuousAlternatingMap.wedgeMul_add_left {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} {A : Type u_2} [NormedRing A] [NormedAlgebra ℝ A] (φ φ' : E [⋀^Fin k]→L[ℝ] A) (ψ : E [⋀^Fin l]→L[ℝ] A) : (φ + φ').wedgeMul ψ = φ.wedgeMul ψ + φ'.wedgeMul ψ

The algebra-valued wedge is additive in its first argument.

@[simp]

theorem ContinuousAlternatingMap.wedgeMul_add_right {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} {A : Type u_2} [NormedRing A] [NormedAlgebra ℝ A] (φ : E [⋀^Fin k]→L[ℝ] A) (ψ ψ' : E [⋀^Fin l]→L[ℝ] A) : φ.wedgeMul (ψ + ψ') = φ.wedgeMul ψ + φ.wedgeMul ψ'

The algebra-valued wedge is additive in its second argument.

@[simp]

theorem ContinuousAlternatingMap.wedgeMul_smul_left {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} {A : Type u_2} [NormedRing A] [NormedAlgebra ℝ A] (c : ℝ) (φ : E [⋀^Fin k]→L[ℝ] A) (ψ : E [⋀^Fin l]→L[ℝ] A) : (c • φ).wedgeMul ψ = c • φ.wedgeMul ψ

The algebra-valued wedge respects real scalar multiplication in its first argument.

@[simp]

theorem ContinuousAlternatingMap.wedgeMul_smul_right {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} {A : Type u_2} [NormedRing A] [NormedAlgebra ℝ A] (c : ℝ) (φ : E [⋀^Fin k]→L[ℝ] A) (ψ : E [⋀^Fin l]→L[ℝ] A) : φ.wedgeMul (c • ψ) = c • φ.wedgeMul ψ

The algebra-valued wedge respects real scalar multiplication in its second argument.

theorem ContinuousAlternatingMap.norm_wedgeMul_le {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} {A : Type u_2} [NormedRing A] [NormedAlgebra ℝ A] (φ : E [⋀^Fin k]→L[ℝ] A) (ψ : E [⋀^Fin l]→L[ℝ] A) : ‖φ.wedgeMul ψ‖ ≤ ↑((k + l).choose k) * ‖φ‖ * ‖ψ‖

The algebra-valued wedge obeys the binomial operator-norm bound.

@[simp]

theorem ContinuousAlternatingMap.wedgeMul_compContinuousLinearMap {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} {A : Type u_2} [NormedRing A] [NormedAlgebra ℝ A] {E' : Type u_3} [SeminormedAddCommGroup E'] [NormedSpace ℝ E'] (f : E' →L[ℝ] E) (φ : E [⋀^Fin k]→L[ℝ] A) (ψ : E [⋀^Fin l]→L[ℝ] A) : (φ.compContinuousLinearMap f).wedgeMul (ψ.compContinuousLinearMap f) = (φ.wedgeMul ψ).compContinuousLinearMap f

Pulling both algebra-valued forms back along a continuous linear map commutes with wedge.

theorem ContinuousAlternatingMap.wedgeMul_assoc {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l m : ℕ} {A : Type u_2} [NormedRing A] [NormedAlgebra ℝ A] (φ : E [⋀^Fin k]→L[ℝ] A) (ψ : E [⋀^Fin l]→L[ℝ] A) (χ : E [⋀^Fin m]→L[ℝ] A) (v : Fin (k + l + m) → E) : ((φ.wedgeMul ψ).wedgeMul χ) v = (φ.wedgeMul (ψ.wedgeMul χ)) (v ∘ Fin.cast ⋯)

The algebra-valued wedge is associative, up to reassociation of its degree.

theorem ContinuousAlternatingMap.wedgeMul_comm {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} {A : Type u_2} [NormedCommRing A] [NormedAlgebra ℝ A] (φ : E [⋀^Fin k]→L[ℝ] A) (ψ : E [⋀^Fin l]→L[ℝ] A) (v : Fin (k + l) → E) : (φ.wedgeMul ψ) v = (-1) ^ (k * l) • (ψ.wedgeMul φ) (v ∘ Fin.cast ⋯)

For a commutative normed algebra, the algebra-valued wedge is graded commutative.