English
The canonical pairing from the exterior power of the dual to the dual of the exterior power is given by alternatingMapLinearEquiv applied to alternatingMapToDual.
Русский
Каноническое парирование между ∧^n(M^*) и (∧^n M)^* задаётся через чередование линейных отображений, применяемое к alternatingMapToDual.
LaTeX
$$$ pairingDual(R\, M\, n) : ⋀[R]^n (Module.Dual R M) \rightarrowₗ[R] Module.Dual R (⋀[R]^n M) = \ alternatingMapLinearEquiv (alternatingMapToDual R M n) $$$
Lean4
/-- The canonical `n`-alternating map from the dual of the `R`-module `M`
to the dual of `⨂[R]^n M`. -/
noncomputable def alternatingMapToDual (n : ℕ) : AlternatingMap R (Module.Dual R M) (Module.Dual R (⋀[R]^n M)) (Fin n)
where
toMultilinearMap := (toTensorPower R M n).dualMap.compMultilinearMap (TensorPower.multilinearMapToDual R M n)
map_eq_zero_of_eq' f i j hf
hij := by
ext v
suffices Matrix.det (n := Fin n) (.of (fun i j ↦ f j (v i))) = 0 by simpa [Matrix.det_apply] using this
exact Matrix.det_zero_of_column_eq hij (by simp [hf])
