Block division and rank specialization

Three algebraic tools for the rational hitting lists. Bivariate polynomials embed injectively into Hahn series over the lexicographically ordered group QuantumLift.Exponents = ℤ ×ₗ ℤ. A square block matrix over a division ring D, flattened through a faithful matrix representation D →+* Matrix κ κ E, is either invertible or loses at least |κ| in rank (block elimination). Finally, specializing the entries of a matrix along a K-algebra map P →ₐ[K] K cannot raise its rank over any field into which P embeds.

Main definitions

• Rational.PolynomialHahn.embed: bivariate polynomials as Hahn series over ℤ ×ₗ ℤ.
• Rational.BlockDivision.blockEmbedding: the entrywise extension of a matrix representation of D to square block matrices over D.

Main results

• Rational.PolynomialHahn.charZero: Hahn series over a characteristic-zero ring have characteristic zero (a scoped instance, available after open Rational.PolynomialHahn).
• Rational.PolynomialHahn.embed_injective: the Hahn-series embedding is injective.
• Rational.BlockDivision.rank_gap: a block-embedded matrix is invertible or has rank at most (|m| - 1) * |κ|.
• Rational.BlockDivision.isUnit_of_rank_gt: rank above (|m| - 1) * |κ| forces invertibility.
• Rational.RankSpecialization.rank_le: specialization cannot raise the generic rank.

References

• Adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Computability/RationalHitting/BlockDivision.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

theorem Cslib.Circuits.Rational.PolynomialHahn.charZero {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonAssocSemiring R] [CharZero R] : CharZero (HahnSeries Γ R)

Hahn series over a coefficient ring of characteristic zero have characteristic zero. It is scoped, since both the class and the type are Mathlib's.

def Cslib.Circuits.Rational.PolynomialHahn.exponent (m : Fin 2 →₀ ℕ) : QuantumLift.Exponents

Embed a two-variable natural exponent vector into the ordered exponent group.

theorem Cslib.Circuits.Rational.PolynomialHahn.exponent_injective : Function.Injective exponent

noncomputable def Cslib.Circuits.Rational.PolynomialHahn.variableSeries {K : Type u_1} [Field K] (i : Fin 2) : HahnSeries QuantumLift.Exponents K

The Hahn monomial corresponding to a polynomial variable.

noncomputable def Cslib.Circuits.Rational.PolynomialHahn.embed {K : Type u_1} [Field K] : MvPolynomial (Fin 2) K →+* HahnSeries QuantumLift.Exponents K

Embed bivariate polynomials into the Hahn-series ring.

theorem Cslib.Circuits.Rational.PolynomialHahn.embed_monomial {K : Type u_1} [Field K] (m : Fin 2 →₀ ℕ) (a : K) : embed ((MvPolynomial.monomial m) a) = (HahnSeries.single (exponent m)) a

theorem Cslib.Circuits.Rational.PolynomialHahn.embed_coeff {K : Type u_1} [Field K] (p : MvPolynomial (Fin 2) K) (m : Fin 2 →₀ ℕ) : (embed p).coeff (exponent m) = p.coeff m

theorem Cslib.Circuits.Rational.PolynomialHahn.embed_injective {K : Type u_1} [Field K] : Function.Injective ⇑embed

def Cslib.Circuits.Rational.BlockDivision.blockEmbedding {D : Type u_1} {E : Type u_2} [DivisionRing D] [Field E] {m : Type u_3} {κ : Type u_4} [Fintype m] [DecidableEq m] [Fintype κ] [DecidableEq κ] (φ : D →+* Matrix κ κ E) : Matrix m m D →+* Matrix (m × κ) (m × κ) E

Extend a matrix representation entrywise to block matrices.

theorem Cslib.Circuits.Rational.BlockDivision.unit_of_vecMul_injective {D : Type u_1} [DivisionRing D] {m : Type u_3} [Fintype m] [DecidableEq m] (A : Matrix m m D) (hA : Function.Injective ⇑A.vecMulLinear) : IsUnit A

def Cslib.Circuits.Rational.BlockDivision.kernelRows {D : Type u_1} {E : Type u_2} [DivisionRing D] [Field E] {m : Type u_3} {κ : Type u_4} [Fintype κ] [DecidableEq κ] (φ : D →+* Matrix κ κ E) (v : m → D) : (κ → E) →ₗ[E] m × κ → E

A nonzero row of a division-ring kernel expands into d independent ordinary kernel rows after a faithful d-dimensional representation.

theorem Cslib.Circuits.Rational.BlockDivision.kernelRows_injective {D : Type u_1} {E : Type u_2} [DivisionRing D] [Field E] {m : Type u_3} {κ : Type u_4} [Fintype κ] [DecidableEq κ] (φ : D →+* Matrix κ κ E) (v : m → D) (hv : v ≠ 0) : Function.Injective ⇑(kernelRows φ v)

theorem Cslib.Circuits.Rational.BlockDivision.kernelRows_mem {D : Type u_1} {E : Type u_2} [DivisionRing D] [Field E] {m : Type u_3} {κ : Type u_4} [Fintype m] [DecidableEq m] [Fintype κ] [DecidableEq κ] (φ : D →+* Matrix κ κ E) (A : Matrix m m D) (v : m → D) (hv : Matrix.vecMul v A = 0) (x : κ → E) : (kernelRows φ v) x ∈ ((blockEmbedding φ) A).vecMulLinear.ker

theorem Cslib.Circuits.Rational.BlockDivision.rank_gap {D : Type u_1} {E : Type u_2} [DivisionRing D] [Field E] {m : Type u_3} {κ : Type u_4} [Fintype m] [DecidableEq m] [Fintype κ] [DecidableEq κ] (φ : D →+* Matrix κ κ E) (A : Matrix m m D) : IsUnit ((blockEmbedding φ) A) ∨ ((blockEmbedding φ) A).rank + Fintype.card κ ≤ Fintype.card m * Fintype.card κ

The rank gap obtained by block elimination over a division ring: a block-embedded matrix is invertible or has rank at most (|m| - 1) * |κ|.

theorem Cslib.Circuits.Rational.BlockDivision.isUnit_of_rank_gt {D : Type u_1} {E : Type u_2} [DivisionRing D] [Field E] {m : Type u_3} {κ : Type u_4} [Fintype m] [DecidableEq m] [Fintype κ] [DecidableEq κ] (φ : D →+* Matrix κ κ E) (A : Matrix m m D) (hq : 1 ≤ Fintype.card m) (h : (Fintype.card m - 1) * Fintype.card κ < ((blockEmbedding φ) A).rank) : IsUnit ((blockEmbedding φ) A)

A block-embedded matrix of rank above (|m| - 1) * |κ| is invertible.

theorem Cslib.Circuits.Rational.RankSpecialization.rank_le {K : Type u_1} {P : Type u_2} {E : Type u_3} {ι : Type u_4} [Field K] [CommRing P] [Field E] [Algebra K P] [Fintype ι] [DecidableEq ι] (ev : P →ₐ[K] K) (inclusion : P →+* E) (hinj : Function.Injective ⇑inclusion) (A : Matrix ι ι P) : (ev.mapMatrix A).rank ≤ (inclusion.mapMatrix A).rank

Specialization cannot raise the generic rank. This version requires no unstated minor criterion: a rank normal form supplies a nonzero minor after constant row and column changes.