Wedge pairing on exterior powers

Given a trivialisation of the top exterior power, the wedge pairing in complementary degrees is a scalar-valued bilinear map. We construct this here and prove that it is a perfect pairing.

Main definitions / results:

• exteriorPower.wedge: the bilinear map ∧^k × ∧^l → ∧^(k + l)
• exteriorPower.wedgePairing: the bilinear map ∧^k × ∧^l → R when k + l = top degree
• exteriorPower.instIsPerfPairWedgePairing: the proof that exteriorPower.wedgePairing is perfect.

@[reducible, inline]

abbrev exteriorPower.wedge (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (k l : ℕ) : ↥(⋀[R]^k M) →ₗ[R] ↥(⋀[R]^l M) →ₗ[R] ↥(⋀[R]^(k + l) M)

The wedge product as an operation on exterior powers.

Equations

• exteriorPower.wedge R M k l = DirectSum.gMulLHom R fun (d : ℕ) => ↥(⋀[R]^d M)

@[reducible, inline]

abbrev exteriorPower.wedgePairing {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) : ↥(⋀[R]^k M) →ₗ[R] ↥(⋀[R]^l M) →ₗ[R] R

The wedge product in complementary degrees as a scalar-valued bilinear map (for a choice of trivialisation of the top exterior power).

Equations

• exteriorPower.wedgePairing vol hkl = (exteriorPower.wedge R M k l).compr₂ (⋯ ▸ ↑vol)

theorem exteriorPower.wedge_apply_of_not_disjoint {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {k l : ℕ} {ι : Type u_3} [LinearOrder ι] (b : Module.Basis ι R M) {I : ↑(Set.powersetCard ι k)} {J : ↑(Set.powersetCard ι l)} (h : ¬Disjoint ↑I ↑J) : ((wedge R M k l) ((Module.Basis.exteriorPower k b) I)) ((Module.Basis.exteriorPower l b) J) = 0

theorem exteriorPower.wedge_apply_of_disjoint {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {k l : ℕ} {ι : Type u_3} [LinearOrder ι] (b : Module.Basis ι R M) [Fintype ι] (hkl : k + l = Fintype.card ι) {I : ↑(Set.powersetCard ι k)} {J : ↑(Set.powersetCard ι l)} (h : Disjoint ↑I ↑J) : ↑(((wedge R M k l) ((Module.Basis.exteriorPower k b) I)) ((Module.Basis.exteriorPower l b) J)) = Set.powersetCard.sign I • b.ExteriorAlgebra (↑I ∪ ↑J)

noncomputable def Module.Basis.topVector {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [LinearOrder ι] (b : Basis ι R M) [Fintype ι] [Nontrivial R] : ↥(⋀[R]^(finrank R M) M)

The wedge product of all the elements of the basis b, in increasing order.

Equations

• b.topVector = (Module.Basis.exteriorPower (Module.finrank R M) b) ⟨Finset.univ, ⋯⟩

@[simp]

theorem Module.Basis.coe_topVector {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [LinearOrder ι] (b : Basis ι R M) [Fintype ι] [Nontrivial R] : ↑b.topVector = b.ExteriorAlgebra Finset.univ

@[simp]

theorem Module.Basis.topVector_eq_exteriorPower {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [LinearOrder ι] (b : Basis ι R M) [Fintype ι] [Nontrivial R] (s : ↑(Set.powersetCard ι (finrank R M))) : (exteriorPower (finrank R M) b) s = b.topVector

theorem exteriorPower.isUnit_apply_topVector {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (vol : ↥(⋀[R]^(Module.finrank R M) M) ≃ₗ[R] R) {ι : Type u_3} [LinearOrder ι] (b : Module.Basis ι R M) [Fintype ι] [Nontrivial R] : IsUnit (vol b.topVector)

theorem exteriorPower.wedgePairing_eq_apply_topVector_smul {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) {ι : Type u_3} [LinearOrder ι] (b : Module.Basis ι R M) [Fintype ι] [Nontrivial R] : wedgePairing vol hkl = vol b.topVector • ↑((Module.Basis.exteriorPower k b).repr ≪≫ₗ (((Module.Basis.exteriorPower l b).dualBasis.reindex (Set.powersetCard.compl ⋯)).groupSMul Set.powersetCard.sign).repr.symm)

instance exteriorPower.instIsPerfPairWedgePairing {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) [Module.Finite R M] [Module.Free R M] : (wedgePairing vol hkl).IsPerfPair