Hodge star on exterior powers

This file contains a definition of the Hodge star on exterior powers.

Main definitions / results:

• exteriorPower.hodgeStar: the Hodge star on exterior powers associated to a choice of bilinear form and volume element.

TODO

• Add API to obviate the need to supply the volume element in the presence of Module.Oriented.
• Prove
  • Δ * B.exteriorPower l (hodgeStar B hB vol hkl x) (hodgeStar B hB vol hkl y) = B.exteriorPower k x y
  • Δ • hodgeStar B hB vol hlk (hodgeStar B hB vol hkl x) = (-1 : R) ^ (k * l) • x where Δ := B.exteriorPower (finrank R M) (vol.symm 1) (vol.symm 1)
• Develop further theory in the common case that the determinant identity: B.exteriorPower (finrank R M) (vol.symm 1) (vol.symm 1) = 1 holds.

noncomputable def exteriorPower.hodgeStar {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] (B : LinearMap.BilinForm R M) (hB : Function.Bijective ⇑B) (vol : ↥(⋀[R]^(Module.finrank R M) M) ≃ₗ[R] R) {k l : ℕ} (hkl : k + l = Module.finrank R M) : ↥(⋀[R]^k M) ≃ₗ[R] ↥(⋀[R]^l M)

The Hodge star associated to B and vol.

Equations

• exteriorPower.hodgeStar B hB vol hkl = (exteriorPower.wedgePairing vol hkl).toPerfPair.trans (LinearEquiv.ofBijective (B.exteriorPower l) ⋯).symm

@[simp]

theorem exteriorPower.hodgeStar_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] (B : LinearMap.BilinForm R M) (hB : Function.Bijective ⇑B) (vol : ↥(⋀[R]^(Module.finrank R M) M) ≃ₗ[R] R) {k l : ℕ} (hkl : k + l = Module.finrank R M) (x : ↥(⋀[R]^k M)) : (hodgeStar B hB vol hkl) x = (LinearEquiv.ofBijective (B.exteriorPower l) ⋯).symm ((wedgePairing vol hkl) x)

@[simp]

theorem exteriorPower.hodgeStar_symm_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] (B : LinearMap.BilinForm R M) (hB : Function.Bijective ⇑B) (vol : ↥(⋀[R]^(Module.finrank R M) M) ≃ₗ[R] R) {k l : ℕ} (hkl : k + l = Module.finrank R M) (a✝ : ↥(⋀[R]^l M)) : (hodgeStar B hB vol hkl).symm a✝ = (wedgePairing vol hkl).toPerfPair.symm ((B.exteriorPower l) a✝)