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))
.
The linear map from the n
th exterior power to the n
th tensor power obtained by
MultilinearMap.alternatization
.
Equations
- exteriorPower.toTensorPower R M n = exteriorPower.alternatingMapLinearEquiv (MultilinearMap.alternatization (PiTensorProduct.tprod R))
Instances For
The canonical n
-alternating map from the dual of the R
-module M
to the dual of ⨂[R]^n M
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The linear map from the exterior power of the dual to the dual of the exterior power.
Equations
- exteriorPower.pairingDual R M n = exteriorPower.alternatingMapLinearEquiv (exteriorPower.alternatingMapToDual R M n)
Instances For
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.)