Dual bases of perfect pairings

DefinitionDual basis with respect to a perfect pairing#✓fully proved

Let \(A\) be a commutative ring, let \(M\) and \(N\) be \(A\)-modules, and let \(B : M \times N \to A\) be a perfect pairing, that is, an \(A\)-bilinear map such that \(x \mapsto B(x, \cdot)\) is a linear isomorphism \(M \to N^*\) and \(y \mapsto B(\cdot, y)\) is a linear isomorphism \(N \to M^*\). Let \(b = (b_i)_{i \in \iota}\) be a basis of \(N\) indexed by a finite type \(\iota\), and let \((b_i^*)_{i \in \iota}\) be its dual basis of \(N^*\), where \(b_i^*(b_j)\) is \(1\) if \(j = i\) and \(0\) otherwise. The dual basis of \(b\) with respect to \(B\) is the basis of \(M\) whose \(i\)-th vector is the image of \(b_i^*\) under the inverse of the isomorphism \(M \to N^*\), \(x \mapsto B(x, \cdot)\).

noncomputable def dualBasis (b : Basis ι A N) : Basis ι A M :=
  b.dualBasis.map B.toPerfPair.symm

Used by 4

Used byEvaluation of the dual basis · Uniqueness of the dual basis · Existence of a dual basis for a perfect pairing · Existence and uniqueness of the dual basis for a perfect pairing

TheoremEvaluation of the dual basis#✓fully proved

Let \(A\) be a commutative ring, let \(M\) and \(N\) be \(A\)-modules, let \(B : M \times N \to A\) be a perfect pairing, and let \(b = (b_i)_{i \in \iota}\) be a basis of \(N\) indexed by a finite type \(\iota\). Write \((b_i^\vee)_{i \in \iota}\) for the dual basis of \(b\) with respect to \(B\), a basis of \(M\). Then for all \(i, j \in \iota\), the value \(B(b_i^\vee, b_j)\) equals \(1\) if \(j = i\) and \(0\) otherwise.

@[simp]
theorem dualBasis_apply (b : Basis ι A N) (i j : ι) :
    B (dualBasis B b i) (b j) = if j = i then 1 else 0

Uses 1 · Used by 2

Statement usesDual basis with respect to a perfect pairing

Used byExistence of a dual basis for a perfect pairing · Existence and uniqueness of the dual basis for a perfect pairing

TheoremUniqueness of the dual basis#✓fully proved

Let \(A\) be a commutative ring, let \(M\) and \(N\) be \(A\)-modules, let \(B : M \times N \to A\) be a perfect pairing, and let \(b = (b_i)_{i \in \iota}\) be a basis of \(N\) indexed by a finite type \(\iota\). If \(b' = (b'_i)_{i \in \iota}\) is a basis of \(M\) such that for all \(i, j \in \iota\) the value \(B(b'_i, b_j)\) equals \(1\) if \(j = i\) and \(0\) otherwise, then \(b'\) is the dual basis of \(b\) with respect to \(B\).

theorem eq_dualBasis_of (b : Basis ι A N) (b' : Basis ι A M)
    (h : ∀ i j, B (b' i) (b j) = if j = i then 1 else 0) :
    b' = dualBasis B b

Uses 1 · Used by 1

Statement usesDual basis with respect to a perfect pairing

Used byExistence and uniqueness of the dual basis for a perfect pairing

TheoremExistence of a dual basis for a perfect pairing#✓fully proved

Let \(A\) be a commutative ring, let \(M\) and \(N\) be \(A\)-modules, let \(B : M \times N \to A\) be a perfect pairing, and let \(b = (b_i)_{i \in \iota}\) be a basis of \(N\) indexed by a finite type \(\iota\). Then there is a basis \((b'_i)_{i \in \iota}\) of \(M\) such that for all \(i, j \in \iota\) the value \(B(b'_i, b_j)\) equals \(1\) if \(j = i\) and \(0\) otherwise.

theorem exists_dualBasis (b : Basis ι A N) :
    ∃ b' : Basis ι A M, ∀ i j, B (b' i) (b j) = if j = i then 1 else 0

Uses 2

Proof usesDual basis with respect to a perfect pairing · Evaluation of the dual basis

TheoremExistence and uniqueness of the dual basis for a perfect pairing#✓fully proved

Let \(A\) be a commutative ring, let \(M\) and \(N\) be \(A\)-modules, let \(B : M \times N \to A\) be a perfect pairing, and let \(b = (b_i)_{i \in \iota}\) be a basis of \(N\) indexed by a finite type \(\iota\). Then there is exactly one basis \((b'_i)_{i \in \iota}\) of \(M\) such that for all \(i, j \in \iota\) the value \(B(b'_i, b_j)\) equals \(1\) if \(j = i\) and \(0\) otherwise.

theorem existsUnique_dualBasis (b : Basis ι A N) :
    ∃! b' : Basis ι A M, ∀ i j, B (b' i) (b j) = if j = i then 1 else 0

Uses 3

Proof usesDual basis with respect to a perfect pairing · Evaluation of the dual basis · Uniqueness of the dual basis

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.