Evaluation formulas for wedge products and pairings

Inside the exterior algebra, the wedge product of exterior powers is the algebra product, and the wedge product of pure exterior products concatenates their vector families. Pairing g₀ ∧ ⋯ ∧ gₙ with θ ∧ v expands along the last vector v (pairingDual_ιMulti_wedge). A trivialisation in a specified top degree gives the wedge pairing by composing the wedge product with that trivialisation; the degree transports disappear after identifying the degree with the finrank, and a wedge pairing is the trivialisation of the exterior-algebra product of its arguments. On the exterior-power bases induced by a basis b, the wedge pairing of e_s and e_t is the shuffle sign of s times the volume of b when s and t are disjoint, and zero otherwise. The top exterior product Module.Basis.topVector of a basis indexed by Fin n is the wedge of the basis vectors, and the shuffle signs of a set of k indices and of its complement of l indices multiply to (-1) ^ (k * l). Composing a complementary-degree wedge pairing, trivialised by a linear map on the top exterior power, with the exterior powers of an endomorphism scales it by the determinant of that endomorphism.

@[simp]

theorem exteriorPower.coe_wedge {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {k l : ℕ} (x : ↥(⋀[R]^k M)) (y : ↥(⋀[R]^l M)) : ↑(((wedge R M k l) x) y) = ↑x * ↑y

Inside the exterior algebra, the wedge product of exterior powers is the algebra product.

@[simp]

theorem exteriorPower.wedge_ιMulti {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {k l : ℕ} (u : Fin k → M) (v : Fin l → M) : ((wedge R M k l) ((ιMulti R k) u)) ((ιMulti R l) v) = (ιMulti R (k + l)) (Fin.append u v)

The wedge product of pure exterior products concatenates their vector families.

theorem exteriorPower.pairingDual_ιMulti_wedge {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (g : Fin (n + 1) → Module.Dual R M) (θ : ↥(⋀[R]^n M)) (v : M) : ((pairingDual R M (n + 1)) ((ιMulti R (n + 1)) g)) (((wedge R M n 1) θ) ((oneEquiv R M).symm v)) = ∑ j : Fin (n + 1), (-1) ^ (n + ↑j) * (g j) v * ((pairingDual R M n) ((ιMulti R n) (g ∘ j.succAbove))) θ

Laplace expansion along the last vector: the pairing of g₀ ∧ ⋯ ∧ gₙ with θ ∧ v is ∑ⱼ (-1) ^ (n + j) gⱼ(v) ⟨g₀ ∧ ⋯ ∧ ĝⱼ ∧ ⋯ ∧ gₙ, θ⟩.

theorem exteriorPower.wedge_map {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {k l : ℕ} {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : (wedge R N k l).compl₁₂ (map k f) (map l f) = (wedge R M k l).compr₂ (map (k + l) f)

The wedge product commutes with applying a linear map to both factors.

theorem exteriorPower.wedge_map_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {k l : ℕ} {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (x : ↥(⋀[R]^k M)) (y : ↥(⋀[R]^l M)) : ((wedge R N k l) ((map k f) x)) ((map l f) y) = (map (k + l) f) (((wedge R M k l) x) y)

Pointwise form of wedge_map for rewriting evaluations of wedge products.

theorem exteriorPower.wedgePairing_eq_compr₂_of_finrank_eq {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {k l : ℕ} (n : ℕ) (hfin : Module.finrank R M = n) (hdeg : k + l = n) (vol : ↥(⋀[R]^n M) ≃ₗ[R] R) : wedgePairing (LinearEquiv.ofEq (⋀[R]^(Module.finrank R M) M) (⋀[R]^n M) ⋯ ≪≫ₗ vol) ⋯ = (wedge R M k l).compr₂ (⋯ ▸ ↑vol)

A wedge pairing transported from a specified top degree is the wedge product followed by the trivialisation in that degree.

theorem exteriorPower.wedgePairing_apply_eq_of_coe_mul_eq {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {k l : ℕ} (vol : ↥(⋀[R]^(Module.finrank R M) M) ≃ₗ[R] R) (hkl : k + l = Module.finrank R M) (x : ↥(⋀[R]^k M)) (y : ↥(⋀[R]^l M)) (z : ↥(⋀[R]^(Module.finrank R M) M)) (h : ↑x * ↑y = ↑z) : ((wedgePairing vol hkl) x) y = vol z

The wedge pairing of x and y is vol of their product in the exterior algebra, read as an element z of the top exterior power. This removes the degree transport k + l = finrank R M built into exteriorPower.wedgePairing, so pairings with different splittings of the top degree can be compared through the exterior algebra.

theorem exteriorPower.wedge_compr₂_compl₁₂_exteriorPower_map_eq_det_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {k l n : ℕ} [Module.Free R M] (hn : Module.finrank R M = n) (hkl : k + l = n) (vol : ↥(⋀[R]^n M) →ₗ[R] R) (f : M →ₗ[R] M) : ((wedge R M k l).compr₂ (⋯ ▸ vol)).compl₁₂ (map k f) (map l f) = LinearMap.det f • (wedge R M k l).compr₂ (⋯ ▸ vol)

For a free module of finrank n = k + l and any linear functional vol on ⋀^n M, precomposing wedge followed by vol with the exterior powers of an endomorphism f scales it by det f.

theorem exteriorPower.wedgePairing_exteriorPower_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {k l : ℕ} [Nontrivial R] (vol : ↥(⋀[R]^(Module.finrank R M) M) ≃ₗ[R] R) (hkl : k + l = Module.finrank R M) {ι : Type u_3} [LinearOrder ι] [Fintype ι] (b : Module.Basis ι R M) (s : ↑(Set.powersetCard ι k)) (t : ↑(Set.powersetCard ι l)) : ((wedgePairing vol hkl) ((Module.Basis.exteriorPower k b) s)) ((Module.Basis.exteriorPower l b) t) = Set.powersetCard.sign s • vol b.topVector • if Disjoint ↑s ↑t then 1 else 0

The wedge pairing on exterior-power basis vectors: e_s and e_t pair to the shuffle sign of s times the volume vol b.topVector when s and t are disjoint, and to zero otherwise. This is the entrywise form of Mathlib's exteriorPower.wedgePairing_eq_apply_topVector_smul.

theorem Module.Basis.topVector_eq_ιMulti {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial R] {n : ℕ} (h : finrank R M = n) (b : Basis (Fin n) R M) : b.topVector = (exteriorPower.ιMulti R (finrank R M)) (⇑b ∘ ⇑(finCongr h))

The top exterior product of a basis indexed by Fin n is the wedge of the basis vectors in their given order, read in the degree finrank R M = n.

theorem Set.powersetCard.sign_mul_sign_compl {I : Type u_1} [LinearOrder I] [Fintype I] {k l : ℕ} (h : l + k = Fintype.card I) (s : ↑(powersetCard I k)) : powersetCard.sign s * powersetCard.sign ((compl h) s) = (-1) ^ (k * l)

The shuffle signs of complementary index sets: for a set s of k indices whose complement has l indices, sign s * sign sᶜ = (-1) ^ (k * l). The two shuffles differ by moving the block sᶜ past the block s.