Perfect pairings from Gram matrices

Let b be a finite basis of a module M over a commutative ring and σ a permutation of its index set. A bilinear form B with B (b i) (b j) = 1 when j = σ i and 0 otherwise sends each b i to the dual basis vector at σ i, so it is the linear equivalence of M onto its dual obtained by reindexing the dual basis along σ. No scalar is inverted, so B is a perfect pairing over every commutative ring.

More generally, a bilinear form whose Gram matrix G in a finite basis has unit determinant is a perfect pairing: in coordinates it is the invertible map x ↦ Gᵀ x followed by the identification of M with its dual given by the dual basis. Conversely, the Gram matrix of a perfect pairing in every finite basis has unit determinant.

Main results

• Module.Basis.isPerfPair_of_apply_eq_ite: a bilinear form whose Gram matrix in a finite basis is a permutation matrix is a perfect pairing.
• Module.Basis.isPerfPair_of_isUnit_det: a bilinear form whose Gram matrix in a finite basis has unit determinant is a perfect pairing.
• Module.Basis.isUnit_det_of_isPerfPair: the Gram matrix of a perfect pairing in a finite basis has unit determinant.

theorem Module.Basis.isPerfPair_of_apply_eq_ite {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Finite ι] [DecidableEq ι] [CommRing R] [AddCommGroup M] [Module R M] (b : Basis ι R M) (B : M →ₗ[R] M →ₗ[R] R) (σ : Equiv.Perm ι) (h : ∀ (i j : ι), (B (b i)) (b j) = if j = σ i then 1 else 0) : B.IsPerfPair

A bilinear form whose Gram matrix in a finite basis is a permutation matrix is a perfect pairing. It is the linear equivalence of M onto its dual sending b i to the dual basis vector at σ i.

theorem Module.Basis.isPerfPair_of_isUnit_det {ι : Type u_1} {R : Type u_2} {M : Type u_3} [DecidableEq ι] [CommRing R] [AddCommGroup M] [Module R M] [Fintype ι] (b : Basis ι R M) (B : M →ₗ[R] M →ₗ[R] R) (h : IsUnit ((LinearMap.toMatrix₂ b b) B).det) : B.IsPerfPair

A bilinear form whose Gram matrix in a finite basis has unit determinant is a perfect pairing.

theorem Module.Basis.isUnit_det_of_isPerfPair {ι : Type u_1} {R : Type u_2} {M : Type u_3} [DecidableEq ι] [CommRing R] [AddCommGroup M] [Module R M] [Fintype ι] (b : Basis ι R M) (B : M →ₗ[R] M →ₗ[R] R) (h : B.IsPerfPair) : IsUnit ((LinearMap.toMatrix₂ b b) B).det

The Gram matrix of a perfect pairing in a finite basis has unit determinant. In the basis b and its dual basis, the matrix of the equivalence M ≃ Dual R M given by B is the transpose of the Gram matrix of B.