Exterior squares and skew-adjoint endomorphisms

A perfect symmetric bilinear form on a finite free module identifies the second exterior power with its skew-adjoint endomorphisms, provided 2 is invertible. The construction factors through alternating bilinear forms and Mathlib's dual pairing for exterior powers.

Over a field, a nondegenerate form on a finite-dimensional vector space is perfect, as witnessed by LinearMap.BilinForm.toDual. Over a commutative ring, perfection means that the linear map from the module to its dual is bijective.

Main definitions

• LinearMap.BilinForm.exteriorSquareEquivSkewAdjoint: the linear equivalence from the second exterior power to the skew-adjoint endomorphisms.

Main results

• LinearMap.BilinForm.exteriorSquareEquivSkewAdjoint_apply_ιMulti_apply: the action of a decomposable bivector.

noncomputable def LinearMap.BilinForm.exteriorSquareEquivSkewAdjoint {R : Type u} [CommRing R] {V : Type v} [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] (B : LinearMap.BilinForm R V) (hB : Function.Bijective ⇑B) (hBsymm : B.IsSymm) [Invertible 2] : ↥(⋀[R]^2 V) ≃ₗ[R] ↥(skewAdjointLieSubalgebra B)

A perfect symmetric bilinear form on a finite free module identifies the second exterior power with its skew-adjoint endomorphisms. The sign is chosen to agree with the normalized Clifford bivector action.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearMap.BilinForm.exteriorSquareEquivSkewAdjoint_apply_ιMulti_apply {R : Type u} [CommRing R] {V : Type v} [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] (B : LinearMap.BilinForm R V) (hB : Function.Bijective ⇑B) (hBsymm : B.IsSymm) [Invertible 2] (u v x : V) : ↑((B.exteriorSquareEquivSkewAdjoint hB hBsymm) ((exteriorPower.ιMulti R 2) ![u, v])) x = (B v) x • u - (B u) x • v

A decomposable bivector acts by the standard skew-adjoint rank-two endomorphism.