16.5. The Mathlib correspondence🔗

Everything above is executable and Mathlib-free. HexGramSchmidtMathlib connects it to Mathlib's real-valued Gram-Schmidt. The orthogonalized basis agrees, row by row, with Mathlib's InnerProductSpace.gramSchmidt after coercing the rows into a Euclidean space.

theorem

Hex.GramSchmidtMathlib.int_basis_row_eq_gramSchmidt {n m : ℕ}
  (b : Hex.Matrix ℤ n m) (i : Fin n) :
  Hex.GramSchmidtMathlib.rowToEuclidean
      ((Hex.GramSchmidt.Int.basis b).row i) =
    InnerProductSpace.gramSchmidt ℝ
      (Hex.GramSchmidtMathlib.intRowFamily b) i
Hex.GramSchmidtMathlib.int_basis_row_eq_gramSchmidt
  {n m : ℕ} (b : Hex.Matrix ℤ n m)
  (i : Fin n) :
  Hex.GramSchmidtMathlib.rowToEuclidean
      ((Hex.GramSchmidt.Int.basis b).row
        i) =
    InnerProductSpace.gramSchmidt ℝ
      (Hex.GramSchmidtMathlib.intRowFamily
        b)
      i

The integer Gram-Schmidt basis agrees rowwise with Mathlib's real-valued gramSchmidt after coercing coefficients into ℝ.

The exact-integer data is tied back to that real picture too: the leading Gram determinant is the product of the squared Gram-Schmidt norms, and the integer scaled coefficient below the diagonal factors as gramDet (j+1) · μ_{i,j} — the identity that makes the coefficients integral.

theorem

Hex.GramSchmidt.Int.gramDet_eq_prod_normSq {n m : ℕ}
  (b : Hex.Matrix ℤ n m) (hli : Hex.GramSchmidt.Int.independent b)
  (k : ℕ) (hk : k ≤ n) :
  ↑(Hex.GramSchmidt.Int.gramDet b k hk) =
    Hex.GramSchmidt.Int.gramSchmidtNormProduct b k hk
Hex.GramSchmidt.Int.gramDet_eq_prod_normSq
  {n m : ℕ} (b : Hex.Matrix ℤ n m)
  (hli :
    Hex.GramSchmidt.Int.independent b)
  (k : ℕ) (hk : k ≤ n) :
  ↑(Hex.GramSchmidt.Int.gramDet b k hk) =
    Hex.GramSchmidt.Int.gramSchmidtNormProduct
      b k hk

For an independent integer matrix, each leading Gram determinant, cast to Rat, equals the product of the squared norms of its Gram-Schmidt basis rows.

theorem

Hex.GramSchmidt.Int.scaledCoeffs_eq {n m : ℕ} (b : Hex.Matrix ℤ n m)
  (i j : ℕ) (hi : i < n) (hj : j < i) :
  ↑(Hex.GramSchmidt.entry (Hex.GramSchmidt.Int.scaledCoeffs b) ⟨i, hi⟩
        ⟨j, ⋯⟩) =
    ↑(Hex.GramSchmidt.Int.gramDet b (j + 1) ⋯) *
      Hex.GramSchmidt.entry (Hex.GramSchmidt.Int.coeffs b) ⟨i, hi⟩
        ⟨j, ⋯⟩
Hex.GramSchmidt.Int.scaledCoeffs_eq
  {n m : ℕ} (b : Hex.Matrix ℤ n m)
  (i j : ℕ) (hi : i < n) (hj : j < i) :
  ↑(Hex.GramSchmidt.entry
        (Hex.GramSchmidt.Int.scaledCoeffs
          b)
        ⟨i, hi⟩ ⟨j, ⋯⟩) =
    ↑(Hex.GramSchmidt.Int.gramDet b
          (j + 1) ⋯) *
      Hex.GramSchmidt.entry
        (Hex.GramSchmidt.Int.coeffs b)
        ⟨i, hi⟩ ⟨j, ⋯⟩

Below the diagonal, the rational image of the integer scaled Gram-Schmidt coefficient factors as gramDet b (j+1) * coeffs[i,j]. Derived from Hex.GramSchmidt.Int.scaledCoeffs_lower_eq_det_scaledCoeffMatrix and Hex.GramSchmidt.Int.scaledCoeffMatrix_det_eq_gramDet_mul_coeffs.