pairingDual — Mathlib

English

The exterior power dual can be identified with the dual of the exterior power via the pairingDual map.

Русский

Через отображение pairingDual можно идентифицировать двойственное пространство ∧^n(M^*) с двойственным пространством ∧^n M.

LaTeX

$$$ pairingDual(R\, M\, n) : ⋀[R]^n (Module.Dual R M) \rightarrowₗ[R] Module.Dual R (⋀[R]^n M) $$$

Lean4

/-- The linear map from the exterior power of the dual to the dual of the exterior power. -/
noncomputable def pairingDual (n : ℕ) : ⋀[R]^n (Module.Dual R M) →ₗ[R] Module.Dual R (⋀[R]^n M) :=
  alternatingMapLinearEquiv (alternatingMapToDual R M n)

Похожие утверждения