Bilinear forms on exterior powers #
The file is a home for results about the bilinear forms on exterior powers of a module.
Main definitions / results: #
LinearMap.BilinForm.exteriorPower: a bilinear form on a module induces a bilinear form on its exterior powers.LinearMap.BilinForm.bijective_exteriorPower: if a module carries a bijective bilinear form, the induced bilinear forms on its exterior powers is also bijective.
noncomputable def
LinearMap.BilinForm.exteriorPower
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(B : LinearMap.BilinForm R M)
(n : ℕ)
:
LinearMap.BilinForm R ↥(⋀[R]^n M)
A bilinear form on M induces a bilinear form on each exterior power.
Equations
- B.exteriorPower n = exteriorPower.pairingDual R M n ∘ₗ exteriorPower.map n B
Instances For
theorem
LinearMap.BilinForm.bijective_exteriorPower
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(B : LinearMap.BilinForm R M)
(n : ℕ)
[Module.Free R M]
[Module.Finite R M]
(hB : Function.Bijective ⇑B)
:
Function.Bijective ⇑(B.exteriorPower n)