The pairing between the exterior power of the dual and the exterior power

We construct the pairing exteriorPower.pairingDual : ⋀[R]^n (Module.Dual R M) →ₗ[R] (Module.Dual R (⋀[R]^n M)).

noncomputable def exteriorPower.toTensorPower (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) : ↥(⋀[R]^n M) →ₗ[R] TensorPower R n M

The linear map from the nth exterior power to the nth tensor power obtained by MultilinearMap.alternatization.

@[simp]

theorem exteriorPower.toTensorPower_apply_ιMulti (R : Type u_1) {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (v : Fin n → M) : (toTensorPower R M n) ((ιMulti R n) v) = ∑ σ : Equiv.Perm (Fin n), Equiv.Perm.sign σ • (PiTensorProduct.tprod R) fun (i : Fin n) => v (σ i)

noncomputable def exteriorPower.alternatingMapToDual (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) : Module.Dual R M [⋀^Fin n]→ₗ[R] Module.Dual R ↥(⋀[R]^n M)

The canonical n-alternating map from the dual of the R-module M to the dual of ⨂[R]^n M.

@[simp]

theorem exteriorPower.alternatingMapToDual_apply_ιMulti {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (f : Fin n → Module.Dual R M) (v : Fin n → M) : ((alternatingMapToDual R M n) f) ((ιMulti R n) v) = (Matrix.of fun (i j : Fin n) => (f j) (v i)).det

noncomputable def exteriorPower.pairingDual (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) : ↥(⋀[R]^n (Module.Dual R M)) →ₗ[R] Module.Dual R ↥(⋀[R]^n M)

The linear map from the exterior power of the dual to the dual of the exterior power.

@[simp]

theorem exteriorPower.pairingDual_ιMulti_ιMulti {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (f : Fin n → Module.Dual R M) (v : Fin n → M) : ((pairingDual R M n) ((ιMulti R n) f)) ((ιMulti R n) v) = (Matrix.of fun (i j : Fin n) => (f j) (v i)).det

If a R-module M has a family of vectors x : ι → M and linear maps f : ι → M such that f i (x j) is 1 or 0 depending on i = j or i ≠ j, then if ι has a linear order, then a similar property regarding pairingDual R M n applies to the family of vectors indexed by Fin n ↪o ι in ⋀[R]^n M and in ⋀[R]^n (Module.Dual R M) that are obtained by taking exterior products of the x i and the f j. (This shall be used in order to construct a basis of ⋀[R]^n M when M is a free module.)

theorem exteriorPower.pairingDual_apply_apply_eq_one {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [LinearOrder ι] (x : ι → M) (f : ι → Module.Dual R M) (h₁ : ∀ (i : ι), (f i) (x i) = 1) (h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0) (n : ℕ) (a : Fin n ↪o ι) : ((pairingDual R M n) ((ιMulti R n) (f ∘ ⇑a))) ((ιMulti R n) (x ∘ ⇑a)) = 1

theorem exteriorPower.pairingDual_apply_apply_eq_one_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [LinearOrder ι] (x : ι → M) (f : ι → Module.Dual R M) (h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0) (n : ℕ) (a b : Fin n ↪o ι) (h : a ≠ b) : ((pairingDual R M n) ((ιMulti R n) (f ∘ ⇑a))) ((ιMulti R n) (x ∘ ⇑b)) = 0