Reduction of Laurent-series subspaces at zero

Subspaces of ι → K⸨X⸩ are reduced to subspaces of ι → K by taking constant coefficients of their integral (power-series) members. Valuation-adapted Gaussian elimination produces an integral frame, which shows that this reduction preserves dimension. Multiplying coordinates by powers of the parameter then gives a rank inequality between filtrations, which is the order reversal step of the small-subspace expansion argument.

Main definitions

• LaurentReduction.F: the Laurent-series field K⸨X⸩ used as coefficient field.
• LaurentReduction.Integral, LaurentReduction.IntegralVector, LaurentReduction.IntegralFunctional: membership in K⟦X⟧, coordinatewise and for linear functionals.
• LaurentReduction.reduction, LaurentReduction.reduce: constant coefficients.
• LaurentReduction.IntegralFrame: an integral spanning family with integral dual coordinates and linearly independent reductions.
• LaurentReduction.reducedSet, LaurentReduction.reducedSubspace: reductions of integral members and their span.
• LaurentReduction.lowProjection, LaurentReduction.lowSupported: low-weight coordinate projection and support subspace.
• LaurentReduction.weightMap, LaurentReduction.liftMap, LaurentReduction.liftEquiv, LaurentReduction.conjugatedWeight: coordinate weights, constant coordinate changes, and their composite.

Main results

• LaurentReduction.exists_integralFrame: every subspace has an integral frame.
• LaurentReduction.finrank_reducedSubspace: reduction preserves dimension.
• LaurentReduction.weighted_filtration_rank, LaurentReduction.conjugated_filtration_rank: the rank form of order reversal.

References

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

@[reducible, inline]

abbrev Cslib.Circuits.Rational.LaurentReduction.F (K : Type u_2) [Field K] : Type u_2

The Laurent-series coefficient field used for reduction at the parameter zero.

def Cslib.Circuits.Rational.LaurentReduction.Integral {K : Type u_1} [Field K] (x : F K) : Prop

Membership in K⟦X⟧, inside K⸨X⸩.

def Cslib.Circuits.Rational.LaurentReduction.reduction {K : Type u_1} [Field K] (x : F K) : K

The constant coefficient of a Laurent series.

def Cslib.Circuits.Rational.LaurentReduction.reduce {K : Type u_1} [Field K] {ι : Type u_2} (x : ι → F K) : ι → K

Take the constant coefficient in each coordinate.

theorem Cslib.Circuits.Rational.LaurentReduction.integral_iff {K : Type u_1} [Field K] (x : F K) : Integral x ↔ Valued.v x ≤ 1

A Laurent series x is integral (x ∈ K⟦X⟧) if and only if its valuation is at most 1.

theorem Cslib.Circuits.Rational.LaurentReduction.integral_zero {K : Type u_1} [Field K] : Integral 0

Zero is an integral Laurent series.

theorem Cslib.Circuits.Rational.LaurentReduction.integral_one {K : Type u_1} [Field K] : Integral 1

One is an integral Laurent series.

theorem Cslib.Circuits.Rational.LaurentReduction.Integral.neg {K : Type u_1} [Field K] {x : F K} (hx : Integral x) : Integral (-x)

Integral Laurent series are closed under negation.

theorem Cslib.Circuits.Rational.LaurentReduction.Integral.mul {K : Type u_1} [Field K] {x y : F K} (hx : Integral x) (hy : Integral y) : Integral (x * y)

Integral Laurent series are closed under multiplication.

@[simp]

theorem Cslib.Circuits.Rational.LaurentReduction.reduction_zero {K : Type u_1} [Field K] : reduction 0 = 0

The constant coefficient of 0 is 0.

@[simp]

theorem Cslib.Circuits.Rational.LaurentReduction.reduction_one {K : Type u_1} [Field K] : reduction 1 = 1

The constant coefficient of 1 is 1.

theorem Cslib.Circuits.Rational.LaurentReduction.reduction_add {K : Type u_1} [Field K] (x y : F K) : reduction (x + y) = reduction x + reduction y

Taking the constant coefficient is additive.

def Cslib.Circuits.Rational.LaurentReduction.IntegralVector {K : Type u_1} [Field K] {ι : Type u_2} (x : ι → F K) : Prop

Coefficientwise integrality, not an arbitrary sublattice.

theorem Cslib.Circuits.Rational.LaurentReduction.IntegralVector.zero {K : Type u_1} [Field K] {ι : Type u_2} : IntegralVector 0

The zero vector has integral coordinates.

theorem Cslib.Circuits.Rational.LaurentReduction.IntegralVector.add {K : Type u_1} [Field K] {ι : Type u_2} {x y : ι → F K} (hx : IntegralVector x) (hy : IntegralVector y) : IntegralVector (x + y)

Vectors with integral coordinates are closed under addition.

theorem Cslib.Circuits.Rational.LaurentReduction.IntegralVector.sub {K : Type u_1} [Field K] {ι : Type u_2} {x y : ι → F K} (hx : IntegralVector x) (hy : IntegralVector y) : IntegralVector (x - y)

Vectors with integral coordinates are closed under subtraction.

theorem Cslib.Circuits.Rational.LaurentReduction.IntegralVector.smul {K : Type u_1} [Field K] {ι : Type u_2} {x : ι → F K} {a : F K} (ha : Integral a) (hx : IntegralVector x) : IntegralVector (a • x)

Vectors with integral coordinates are closed under multiplication by an integral scalar.

def Cslib.Circuits.Rational.LaurentReduction.IntegralFunctional {K : Type u_1} [Field K] {ι : Type u_2} (f : (ι → F K) →ₗ[F K] F K) : Prop

A coordinate functional which is defined integrally on the full ambient integral lattice.

structure Cslib.Circuits.Rational.LaurentReduction.IntegralFrame {K : Type u_1} [Field K] {ι : Type u_2} (U : Submodule (F K) (ι → F K)) : Type (max u_1 u_2)

An integral spanning frame with integral dual coordinates and independent reductions.

• length : ℕ

  Number of frame vectors.

• vector : Fin self.length → ι → F K

  The frame vectors in the ambient Laurent-series space.

• coordinate : Fin self.length → (ι → F K) →ₗ[F K] F K

  Dual coordinate functionals on the full ambient space.

• span_eq : Submodule.span (F K) (Set.range self.vector) = U

  The frame spans the specified subspace.

• vector_integral (j : Fin self.length) : IntegralVector (self.vector j)

  Every frame vector has integral coordinates.

• coordinate_integral (j : Fin self.length) : IntegralFunctional (self.coordinate j)

  The dual coordinates preserve the integral lattice.

• pairing (i j : Fin self.length) : (self.coordinate i) (self.vector j) = if i = j then 1 else 0

  The coordinate functionals are dual to the frame vectors.

• reduced_independent : LinearIndependent K fun (j : Fin self.length) => reduce (self.vector j)

  Reduction at zero preserves independence.

theorem Cslib.Circuits.Rational.LaurentReduction.exists_integralFrame {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] (U : Submodule (F K) (ι → F K)) : Nonempty (IntegralFrame U)

Valuation-adapted Gaussian elimination constructs an integral frame for any Laurent-series subspace. The coordinate functionals guarantee saturation.

theorem Cslib.Circuits.Rational.LaurentReduction.IntegralFrame.vector_mem {K : Type u_1} [Field K] {ι : Type u_2} {U : Submodule (F K) (ι → F K)} (b : IntegralFrame U) (j : Fin b.length) : b.vector j ∈ U

Every vector of an IntegralFrame U belongs to U.

theorem Cslib.Circuits.Rational.LaurentReduction.reduction_C {K : Type u_1} [Field K] (a : K) : reduction (HahnSeries.C a) = a

The constant coefficient of the constant Laurent series HahnSeries.C a is a.

def Cslib.Circuits.Rational.LaurentReduction.reducedSet {K : Type u_1} [Field K] {ι : Type u_2} (U : Submodule (F K) (ι → F K)) : Set (ι → K)

The reduction uses every integral member of U.

def Cslib.Circuits.Rational.LaurentReduction.reducedSubspace {K : Type u_1} [Field K] {ι : Type u_2} (U : Submodule (F K) (ι → F K)) : Submodule K (ι → K)

The subspace spanned by reductions of integral vectors in the original subspace.

theorem Cslib.Circuits.Rational.LaurentReduction.reducedSet_eq_span {K : Type u_1} [Field K] {ι : Type u_2} {U : Submodule (F K) (ι → F K)} (b : IntegralFrame U) : reducedSet U = ↑(Submodule.span K (Set.range fun (j : Fin b.length) => reduce (b.vector j)))

For any integral frame b of U, reducedSet U is the K-span of the reduced frame vectors.

theorem Cslib.Circuits.Rational.LaurentReduction.reducedSubspace_eq_span {K : Type u_1} [Field K] {ι : Type u_2} {U : Submodule (F K) (ι → F K)} (b : IntegralFrame U) : reducedSubspace U = Submodule.span K (Set.range fun (j : Fin b.length) => reduce (b.vector j))

For any integral frame b of U, reducedSubspace U is the K-span of the reduced frame vectors.

theorem Cslib.Circuits.Rational.LaurentReduction.finrank_reducedSubspace {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] (U : Submodule (F K) (ι → F K)) : Module.finrank K ↥(reducedSubspace U) = Module.finrank (F K) ↥U

Full integral reduction preserves dimension.

theorem Cslib.Circuits.Rational.LaurentReduction.Integral.order_nonneg {K : Type u_1} [Field K] {x : F K} (hx : Integral x) : 0 ≤ HahnSeries.order x

An integral Laurent series has nonnegative order.

noncomputable def Cslib.Circuits.Rational.LaurentReduction.weightMap {K : Type u_1} [Field K] {ι : Type u_2} (w : ι → ℕ) : (ι → F K) →ₗ[F K] ι → F K

Multiplication by t^a, written as its identical Laurent monomial.

theorem Cslib.Circuits.Rational.LaurentReduction.weightMap_injective {K : Type u_1} [Field K] {ι : Type u_2} (w : ι → ℕ) : Function.Injective ⇑(weightMap w)

Coordinatewise multiplication weightMap w by Laurent monomials is injective.

theorem Cslib.Circuits.Rational.LaurentReduction.reducedSubspace_mono {K : Type u_1} [Field K] {ι : Type u_2} {U V : Submodule (F K) (ι → F K)} (h : U ≤ V) : reducedSubspace U ≤ reducedSubspace V

reducedSubspace is monotone with respect to submodule inclusion.

def Cslib.Circuits.Rational.LaurentReduction.lowProjection {K : Type u_1} [Field K] {ι : Type u_2} (w : ι → ℕ) (A : ℕ) : (ι → K) →ₗ[K] { i : ι // w i ≤ A } → K

Low coordinate projection and its complementary support subspace.

def Cslib.Circuits.Rational.LaurentReduction.lowSupported {K : Type u_1} [Field K] {ι : Type u_2} (w : ι → ℕ) (A : ℕ) : Submodule K (ι → K)

Vectors whose coordinates vanish above the truncation threshold.

theorem Cslib.Circuits.Rational.LaurentReduction.finrank_map_injective {L : Type u_2} [Field L] {V : Type u_3} {W : Type u_4} [AddCommGroup V] [Module L V] [AddCommGroup W] [Module L W] (f : V →ₗ[L] W) (hf : Function.Injective ⇑f) (U : Submodule L V) : Module.finrank L ↥(Submodule.map f U) = Module.finrank L ↥U

Mapping a submodule by an injective linear map preserves finrank.

theorem Cslib.Circuits.Rational.LaurentReduction.weighted_filtration_rank {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] (w : ι → ℕ) (A : ℕ) (U W : Submodule (F K) (ι → F K)) (hW : Submodule.map (weightMap w) U ≤ W) : Module.finrank K ↥(Submodule.map (lowProjection w A) (reducedSubspace U)) ≤ Module.finrank K ↥(reducedSubspace W ⊓ lowSupported w A)

Filtration version of order reversal, before a constant coordinate change. This uses the whole integral lattice on both sides.

noncomputable def Cslib.Circuits.Rational.LaurentReduction.liftMap {K : Type u_1} [Field K] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] (P : (ι → K) →ₗ[K] κ → K) : (ι → F K) →ₗ[F K] κ → F K

Extend a linear map to Laurent-series vectors using its constant coefficient matrix.

theorem Cslib.Circuits.Rational.LaurentReduction.liftMap_apply {K : Type u_1} [Field K] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] (P : (ι → K) →ₗ[K] κ → K) (x : ι → F K) (j : κ) : (liftMap P) x j = ∑ i : ι, HahnSeries.C (LinearMap.toMatrix' P j i) * x i

Coordinate j of liftMap P x is the matrix-vector product with the constant coefficients of P.

noncomputable def Cslib.Circuits.Rational.LaurentReduction.liftEquiv {K : Type u_1} [Field K] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (E : (ι → K) ≃ₗ[K] κ → K) : (ι → F K) ≃ₗ[F K] κ → F K

Extend a linear equivalence to Laurent-series vectors.

@[simp]

theorem Cslib.Circuits.Rational.LaurentReduction.liftEquiv_toLinearMap {K : Type u_1} [Field K] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (E : (ι → K) ≃ₗ[K] κ → K) : ↑(liftEquiv E) = liftMap ↑E

The underlying linear map of liftEquiv E is liftMap E.toLinearMap.

theorem Cslib.Circuits.Rational.LaurentReduction.liftEquiv_symm {K : Type u_1} [Field K] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (E : (ι → K) ≃ₗ[K] κ → K) : (liftEquiv E).symm = liftEquiv E.symm

The inverse of liftEquiv E is liftEquiv E.symm.

theorem Cslib.Circuits.Rational.LaurentReduction.integral_liftEquiv_iff {K : Type u_1} [Field K] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (E : (ι → K) ≃ₗ[K] κ → K) (x : ι → F K) : IntegralVector ((liftEquiv E) x) ↔ IntegralVector x

liftEquiv E preserves and reflects IntegralVector.

noncomputable def Cslib.Circuits.Rational.LaurentReduction.conjugatedWeight {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Ein Eout : (ι → K) ≃ₗ[K] ι → K) (w : ι → ℕ) : (ι → F K) →ₗ[F K] ι → F K

Constant coordinates on the input and output may differ (Taylor on the input, reverse Taylor on the output in the application).

theorem Cslib.Circuits.Rational.LaurentReduction.conjugatedWeight_injective {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Ein Eout : (ι → K) ≃ₗ[K] ι → K) (w : ι → ℕ) : Function.Injective ⇑(conjugatedWeight Ein Eout w)

The conjugated weight map conjugatedWeight Ein Eout w is injective.

theorem Cslib.Circuits.Rational.LaurentReduction.conjugated_filtration_rank {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Ein Eout : (ι → K) ≃ₗ[K] ι → K) (w : ι → ℕ) (A : ℕ) (U W : Submodule (F K) (ι → F K)) (hW : Submodule.map (conjugatedWeight Ein Eout w) U ≤ W) : Module.finrank K ↥(Submodule.map (lowProjection w A) (Submodule.map (↑Ein) (reducedSubspace U))) ≤ Module.finrank K ↥(Submodule.map (↑Eout) (reducedSubspace W) ⊓ lowSupported w A)

Filtration rank inequality for conjugatedWeight Ein Eout w after reduction at zero.

theorem Cslib.Circuits.Rational.LaurentReduction.finrank_map_add_finrank_inf_ker {L : Type u_2} [Field L] {V : Type u_3} {W : Type u_4} [AddCommGroup V] [Module L V] [AddCommGroup W] [Module L W] (f : V →ₗ[L] W) (U : Submodule L V) [FiniteDimensional L ↥U] : Module.finrank L ↥(Submodule.map f U) + Module.finrank L ↥(U ⊓ f.ker) = Module.finrank L ↥U

Rank-nullity for the restriction of a linear map f to a finite-dimensional submodule U.