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)