English
For a nondegenerate bilinear form B on V and a finite basis b of V with index set ι, the B-dual basis is defined as the image of the dual basis of b under the inverse of the isomorphism B.toDual hB. This provides a basis of V with the defining property that B(dual_i, b_j) = δ_{ij} and B(b_i, dualBasis_j) = δ_{ij}.
Русский
Для невырожденной билинейной формы B на V и конечного базиса b с индексационным множеством ι, B-двойственная база определяется как образ двойственной базы b под обратным отображением B.toDual hB. Это даёт базис V с свойствами B(dual_i, b_j) = δ_{ij} и B(b_i, dualBasis_j) = δ_{ij}.
LaTeX
$$$\\text{dualBasis}(B,hB,b) = b.dualBasis.map\\big( (B.toDual hB)^{-1} \\big).$$$
Lean4
/-- The `B`-dual basis `B.dualBasis hB b` to a finite basis `b` satisfies
`B (B.dualBasis hB b i) (b j) = B (b i) (B.dualBasis hB b j) = if i = j then 1 else 0`,
where `B` is a nondegenerate (symmetric) bilinear form and `b` is a finite basis. -/
noncomputable def dualBasis (B : BilinForm K V) (hB : B.Nondegenerate) (b : Basis ι K V) : Basis ι K V :=
haveI := FiniteDimensional.of_fintype_basis b
b.dualBasis.map (B.toDual hB).symm
