hex

35.12. HexPolySmith: polynomial Smith normal form🔗

35.12.1. Introduction🔗

HexPolySmith computes Smith normal form for dense matrices over F[x]. Its nonzero diagonal entries are monic and form a divisibility chain, so they are the invariant factors of the matrix and describe the module presented by its rows. The algorithm, matrices, and dense polynomials are Mathlib-free.

The companion HexPolySmithMathlib transports the result to Mathlib's Polynomial F, module-basis, quotient, and rational-function rank APIs.

35.12.2. Smith data and entry points🔗

The full record contains the rank, nonzero diagonal, left and right change-of- basis matrices, and explicit inverses for both transformations.

🔗structure
Hex.PolyMatrix.SmithData.{u} (F : Type u) [Zero F] [DecidableEq F]
  (n m : ℕ) : Type u
Hex.PolyMatrix.SmithData.{u} (F : Type u)
  [Zero F] [DecidableEq F] (n m : ℕ) :
  Type u

Executable Smith normal form data over F[x]: the rank, invariant factors, and both change-of-basis matrices with their inverses.

Constructor

Hex.PolyMatrix.SmithData.mk.{u}

Fields

rank : ℕ

Number of nonzero Smith diagonal entries.

diag : Vector (Hex.DensePoly F) self.rank

Monic nonzero invariant factors, in divisibility order.

left : Hex.Matrix (Hex.DensePoly F) n n

Left change-of-basis matrix.

leftInv : Hex.Matrix (Hex.DensePoly F) n n

Explicit inverse of the left change-of-basis matrix.

right : Hex.Matrix (Hex.DensePoly F) m m

Right change-of-basis matrix.

rightInv : Hex.Matrix (Hex.DensePoly F) m m

Explicit inverse of the right change-of-basis matrix.

Use Hex.PolyMatrix.snf when only the diagonal matrix is needed. The transform-free projections Hex.PolyMatrix.snfRank and Hex.PolyMatrix.invariantFactors avoid accumulating the four transformation matrices. Use Hex.PolyMatrix.snfData when a basis change or certificate is required.

🔗def
Hex.PolyMatrix.snf.{u} {F : Type u} [Lean.Grind.Field F] [DecidableEq F]
  {n m : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Hex.Matrix (Hex.DensePoly F) n m
Hex.PolyMatrix.snf.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  {n m : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Hex.Matrix (Hex.DensePoly F) n m

Polynomial Smith normal form. This path does not allocate or update transformation matrices.

🔗def
Hex.PolyMatrix.snfRank.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m) : ℕ
Hex.PolyMatrix.snfRank.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  {n m : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m) :
  ℕ

Rank returned by the same transform-free Smith run.

🔗def
Hex.PolyMatrix.snfData.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Hex.PolyMatrix.SmithData F n m
Hex.PolyMatrix.snfData.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  {n m : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Hex.PolyMatrix.SmithData F n m

Full Smith data, including explicit inverses of both transformations.

🔗def
Hex.PolyMatrix.invariantFactors.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Vector (Hex.DensePoly F) (Hex.PolyMatrix.snfRank A)
Hex.PolyMatrix.invariantFactors.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Vector (Hex.DensePoly F)
    (Hex.PolyMatrix.snfRank A)

The monic invariant factors, computed on the transform-free path.

Diagonal input has convenience wrappers around the same certified reduction.

🔗def
Hex.PolyMatrix.snfDiagonal.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {r : ℕ} (d : Vector (Hex.DensePoly F) r) :
  Hex.Matrix (Hex.DensePoly F) r r
Hex.PolyMatrix.snfDiagonal.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {r : ℕ}
  (d : Vector (Hex.DensePoly F) r) :
  Hex.Matrix (Hex.DensePoly F) r r

Smith-normal matrix for diagonal polynomial input.

🔗def
Hex.PolyMatrix.snfDiagonalData.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {r : ℕ} (d : Vector (Hex.DensePoly F) r) :
  Hex.PolyMatrix.SmithData F r r
Hex.PolyMatrix.snfDiagonalData.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {r : ℕ}
  (d : Vector (Hex.DensePoly F) r) :
  Hex.PolyMatrix.SmithData F r r

Full Smith data for a diagonal polynomial matrix.

35.12.3. Module structure and solving🔗

moduleStructure returns the free rank and the nonunit torsion factors of the presented module. quotientOrder is the monic generator of the zeroth Fitting ideal, or zero when the quotient has a free summand.

🔗def
Hex.PolyMatrix.moduleStructure.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m) :
  ℕ × Array (Hex.DensePoly F)
Hex.PolyMatrix.moduleStructure.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m) :
  ℕ × Array (Hex.DensePoly F)

Free rank and nonunit torsion factors of the presented module.

🔗def
Hex.PolyMatrix.quotientOrder.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Hex.DensePoly F
Hex.PolyMatrix.quotientOrder.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Hex.DensePoly F

Monic generator of the zeroth Fitting ideal, or zero when the quotient has a free summand.

The solver decides and constructs row-vector solutions of x * A = b. It transforms the right-hand side by the right basis change, solves the diagonal system, and maps the solution back with the left basis change.

🔗def
Hex.PolyMatrix.solve.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m)
  (b : Vector (Hex.DensePoly F) m) : Option (Vector (Hex.DensePoly F) n)
Hex.PolyMatrix.solve.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  {n m : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m)
  (b : Vector (Hex.DensePoly F) m) :
  Option (Vector (Hex.DensePoly F) n)

Solve x * A = b by transforming the right-hand side, solving the diagonal system, and mapping the solution back with the left transform.

35.12.4. Worked example🔗

The following example is elaborated with the manual. Its diagonal entries already form the chain x ∣ x², so the Smith form is unchanged.

open Hex Hex.PolyMatrix namespace HexPolySmithChapterExample private def x : DensePoly Rat := DensePoly.ofList [0, 1] private def A : Matrix (DensePoly Rat) 2 2 := #m[x, 0; 0, x * x] #guard snfRank A = 2 #guard snf A == A #guard (invariantFactors A).toList == [x, x * x] #guard quotientOrder A == x * x * x private def witness : Vector (DensePoly Rat) 2 := #v[x + 1, 2] private def b : Vector (DensePoly Rat) 2 := Hex.Matrix.vecMul witness A #guard solve A b == some witness end HexPolySmithChapterExample

35.12.5. Certificates and correctness🔗

The logical contract packages the inverse identities, transformed-input identity, rank bounds, monicity, and divisibility chain.

🔗structure
Hex.PolyMatrix.IsSNF.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m)
  (S : Hex.PolyMatrix.SmithData F n m) : Prop
Hex.PolyMatrix.IsSNF.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  {n m : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m)
  (S : Hex.PolyMatrix.SmithData F n m) :
  Prop

Smith normal form contract over F[x].

Constructor

Hex.PolyMatrix.IsSNF.mk.{u}

Fields

left_inv : S.left * S.leftInv = Hex.Matrix.identity n

The stored left inverse is correct.

right_inv : S.right * S.rightInv = Hex.Matrix.identity m

The stored right inverse is correct.

mul_eq : S.left * A * S.right = Hex.Matrix.diagMatrix S.diag n m

The transformations carry the input to the stored Smith diagonal.

rank_le_n : S.rank ≤ n

The rank does not exceed the row count.

rank_le_m : S.rank ≤ m

The rank does not exceed the column count.

diag_monic : ∀ (i : Fin S.rank), S.diag[i].Monic

Every stored invariant factor is monic.

chain : ∀ (i : ℕ) (h : i + 1 < S.rank), S.diag[i] ∣ S.diag[i + 1]

Consecutive invariant factors form a divisibility chain.

The general algorithm satisfies that contract, and the direct certificate checker is sound for independently supplied data.

🔗theorem
Hex.PolyMatrix.snfData_isSNF.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Hex.PolyMatrix.IsSNF A (Hex.PolyMatrix.snfData A)
Hex.PolyMatrix.snfData_isSNF.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Hex.PolyMatrix.IsSNF A
    (Hex.PolyMatrix.snfData A)

The general Smith algorithm returns data satisfying the full logical Smith-normal-form contract.

🔗def
Hex.PolyMatrix.snfCert.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m)
  (S : Hex.PolyMatrix.SmithData F n m)
  (T : Hex.Matrix (Hex.DensePoly F) n m) : Bool
Hex.PolyMatrix.snfCert.{u} {F : Type u}
  [Lean.Grind.Field F] [DecidableEq F]
  {n m : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m)
  (S : Hex.PolyMatrix.SmithData F n m)
  (T : Hex.Matrix (Hex.DensePoly F) n m) :
  Bool

Accept (S,T) as a Smith form of A, where T = S.left * A.

🔗theorem
Hex.PolyMatrix.snfCert_sound.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m : ℕ} {A : Hex.Matrix (Hex.DensePoly F) n m}
  {S : Hex.PolyMatrix.SmithData F n m}
  {T : Hex.Matrix (Hex.DensePoly F) n m}
  (h : Hex.PolyMatrix.snfCert A S T = true) : Hex.PolyMatrix.IsSNF A S
Hex.PolyMatrix.snfCert_sound.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m : ℕ}
  {A : Hex.Matrix (Hex.DensePoly F) n m}
  {S : Hex.PolyMatrix.SmithData F n m}
  {T : Hex.Matrix (Hex.DensePoly F) n m}
  (h :
    Hex.PolyMatrix.snfCert A S T = true) :
  Hex.PolyMatrix.IsSNF A S

Every accepted direct certificate satisfies the Smith contract.

For large polynomial products, an evaluation certificate can check the identity at scalar points. Its soundness theorem makes the separation and degree hypotheses explicit; small fields do not silently obtain enough points.

🔗def
Hex.PolyMatrix.mulEqCertAt.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m k : ℕ} (pts : Vector F k)
  (U : Hex.Matrix (Hex.DensePoly F) n n)
  (A C : Hex.Matrix (Hex.DensePoly F) n m) : Bool
Hex.PolyMatrix.mulEqCertAt.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m k : ℕ}
  (pts : Vector F k)
  (U : Hex.Matrix (Hex.DensePoly F) n n)
  (A C :
    Hex.Matrix (Hex.DensePoly F) n m) :
  Bool

Check U * A = C at the supplied scalar points. Its soundness theorem requires the usual distinctness and degree-bound hypotheses.

🔗theorem
Hex.PolyMatrix.mulEqCertAt_sound.{u} {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m k D : ℕ} {pts : Vector F k}
  {U : Hex.Matrix (Hex.DensePoly F) n n}
  {A C : Hex.Matrix (Hex.DensePoly F) n m}
  (hsep : Hex.PolyMatrix.EvaluationSeparatesUpTo pts D)
  (hprodDegree :
    ∀ (i : Fin n) (j : Fin m), (U * A)[(i, j)].natDegree ≤ D)
  (hresultDegree : ∀ (i : Fin n) (j : Fin m), C[(i, j)].natDegree ≤ D)
  (h : Hex.PolyMatrix.mulEqCertAt pts U A C = true) : U * A = C
Hex.PolyMatrix.mulEqCertAt_sound.{u}
  {F : Type u} [Lean.Grind.Field F]
  [DecidableEq F] {n m k D : ℕ}
  {pts : Vector F k}
  {U : Hex.Matrix (Hex.DensePoly F) n n}
  {A C : Hex.Matrix (Hex.DensePoly F) n m}
  (hsep :
    Hex.PolyMatrix.EvaluationSeparatesUpTo
      pts D)
  (hprodDegree :
    ∀ (i : Fin n) (j : Fin m),
      (U * A)[(i, j)].natDegree ≤ D)
  (hresultDegree :
    ∀ (i : Fin n) (j : Fin m),
      C[(i, j)].natDegree ≤ D)
  (h :
    Hex.PolyMatrix.mulEqCertAt pts U A C =
      true) :
  U * A = C

An accepted evaluation certificate proves the product identity whenever the checked point set separates all entries in the advertised degree range.

35.12.6. The Mathlib correspondence🔗

The bridge maps entries to Polynomial F and preserves matrix multiplication.

🔗def
HexPolySmithMathlib.polyMatrixEquiv.{u} {F : Type u} [Field F]
  [DecidableEq F] {n m : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Matrix (Fin n) (Fin m) (Polynomial F)
HexPolySmithMathlib.polyMatrixEquiv.{u}
  {F : Type u} [Field F] [DecidableEq F]
  {n m : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Matrix (Fin n) (Fin m) (Polynomial F)

The executable polynomial matrix as a Mathlib matrix over Polynomial F.

🔗theorem
HexPolySmithMathlib.polyMatrixEquiv_mul.{u} {F : Type u} [Field F]
  [DecidableEq F] {n m k : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m)
  (B : Hex.Matrix (Hex.DensePoly F) m k) :
  HexPolySmithMathlib.polyMatrixEquiv (A * B) =
    HexPolySmithMathlib.polyMatrixEquiv A *
      HexPolySmithMathlib.polyMatrixEquiv B
HexPolySmithMathlib.polyMatrixEquiv_mul.{u}
  {F : Type u} [Field F] [DecidableEq F]
  {n m k : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m)
  (B : Hex.Matrix (Hex.DensePoly F) m k) :
  HexPolySmithMathlib.polyMatrixEquiv
      (A * B) =
    HexPolySmithMathlib.polyMatrixEquiv
        A *
      HexPolySmithMathlib.polyMatrixEquiv
        B

Entrywise polynomial transport preserves matrix multiplication.

It constructs Mathlib's simultaneous Smith-basis structure and supplements it with the invariant-factor divisibility chain.

🔗def
HexPolySmithMathlib.smithNormalForm.{u} {F : Type u} [Field F]
  [DecidableEq F] {n m : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Module.Basis.SmithNormalForm
    (Submodule.span (Polynomial F)
      (Set.range (HexPolySmithMathlib.polyMatrixEquiv A)))
    (Fin m) (Hex.PolyMatrix.snfRank A)
HexPolySmithMathlib.smithNormalForm.{u}
  {F : Type u} [Field F] [DecidableEq F]
  {n m : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Module.Basis.SmithNormalForm
    (Submodule.span (Polynomial F)
      (Set.range
        (HexPolySmithMathlib.polyMatrixEquiv
          A)))
    (Fin m) (Hex.PolyMatrix.snfRank A)

The executable polynomial Smith form as Mathlib's simultaneous-basis structure for the submodule spanned by the rows of the input matrix.

🔗theorem
HexPolySmithMathlib.smithNormalForm_chain.{u} {F : Type u} [Field F]
  [DecidableEq F] {n m : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m)
  (i : ℕ) (h : i + 1 < Hex.PolyMatrix.snfRank A) :
  (HexPolySmithMathlib.smithNormalForm A).a ⟨i, ⋯⟩ ∣
    (HexPolySmithMathlib.smithNormalForm A).a ⟨i + 1, h⟩
HexPolySmithMathlib.smithNormalForm_chain.{u}
  {F : Type u} [Field F] [DecidableEq F]
  {n m : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m)
  (i : ℕ)
  (h : i + 1 < Hex.PolyMatrix.snfRank A) :
  (HexPolySmithMathlib.smithNormalForm
          A).a
      ⟨i, ⋯⟩ ∣
    (HexPolySmithMathlib.smithNormalForm
          A).a
      ⟨i + 1, h⟩

The canonical Smith coefficients form a divisibility chain.

The quotient decomposition separates its free coordinates from the cyclic torsion factors, while the rank theorem extends scalars to the fraction field F(x).

🔗def
HexPolySmithMathlib.quotientEquiv.{u} {F : Type u} [Field F]
  [DecidableEq F] {n m : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m) :
  ((Fin m → Polynomial F) ⧸
      Submodule.span (Polynomial F)
        (Set.range
          (HexPolySmithMathlib.polyMatrixEquiv A))) ≃ₗ[Polynomial F]
    (Fin (m - Hex.PolyMatrix.snfRank A) → Polynomial F) ×
      DirectSum (Fin (Hex.PolyMatrix.snfRank A)) fun i =>
        Polynomial F ⧸
          Ideal.span
            {HexPolyMathlib.toPolynomial
                (Hex.PolyMatrix.invariantFactors A)[i]}
HexPolySmithMathlib.quotientEquiv.{u}
  {F : Type u} [Field F] [DecidableEq F]
  {n m : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m) :
  ((Fin m → Polynomial F) ⧸
      Submodule.span (Polynomial F)
        (Set.range
          (HexPolySmithMathlib.polyMatrixEquiv
            A))) ≃ₗ[Polynomial F]
    (Fin (m - Hex.PolyMatrix.snfRank A) →
        Polynomial F) ×
      DirectSum
        (Fin (Hex.PolyMatrix.snfRank A))
        fun i =>
        Polynomial F ⧸
          Ideal.span
            {HexPolyMathlib.toPolynomial
                (Hex.PolyMatrix.invariantFactors
                    A)[i]}

The presented module is the product of its free part and its cyclic torsion summands.

🔗theorem
HexPolySmithMathlib.rank_eq_ratFunc_rank.{u} {F : Type u} [Field F]
  [DecidableEq F] {n m : ℕ} (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Hex.PolyMatrix.snfRank A =
    ((HexPolySmithMathlib.polyMatrixEquiv A).map
        ⇑(algebraMap (Polynomial F) (RatFunc F))).rank
HexPolySmithMathlib.rank_eq_ratFunc_rank.{u}
  {F : Type u} [Field F] [DecidableEq F]
  {n m : ℕ}
  (A : Hex.Matrix (Hex.DensePoly F) n m) :
  Hex.PolyMatrix.snfRank A =
    ((HexPolySmithMathlib.polyMatrixEquiv
            A).map
        ⇑(algebraMap (Polynomial F)
            (RatFunc F))).rank

The executable rank is the rank after extending scalars from F[x] to the field F(x).

35.12.7. Cross-references🔗

HexPolySmith uses HexPoly for dense Euclidean polynomial arithmetic, HexMatrix for matrix operations, and HexDeterminant for determinantal-divisor arguments. The characteristic-matrix application and rational canonical form belong to a separate downstream library.