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: membership in K⟦X⟧, coordinatewise.
• LaurentReduction.reduction, LaurentReduction.reduce: constant coefficients.
• LaurentReduction.IntegralFrame: an integral spanning family with integral dual coordinates and linearly independent reductions.
• LaurentReduction.reducedSubspace: the span of reductions of integral members.
• LaurentReduction.weightMap, LaurentReduction.liftMap, 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

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

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

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

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

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

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)

@[simp]

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

@[simp]

theorem Cslib.Circuits.Rational.LaurentReduction.reduction_one {K : Type u_1} [Field K] : reduction 1 = 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

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

theorem Cslib.Circuits.Rational.LaurentReduction.normalize_vector {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] (x : ι → F K) (hx : x ≠ 0) : ∃ (c : ι) (u : F K), u ≠ 0 ∧ (∀ (i : ι), Integral (u * x i)) ∧ u * x c = 1

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

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)

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)

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)

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.linearIndependent {K : Type u_1} [Field K] {ι : Type u_2} {U : Submodule (F K) (ι → F K)} (b : IntegralFrame U) : LinearIndependent (F K) b.vector

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

theorem Cslib.Circuits.Rational.LaurentReduction.IntegralFrame.integral_coordinates {K : Type u_1} [Field K] {ι : Type u_2} {U : Submodule (F K) (ι → F K)} (b : IntegralFrame U) (x : ι → F K) (hx : IntegralVector x) (j : Fin b.length) : Integral ((b.coordinate j) x)

Full integral-lattice saturation: every integral member has integral basis coordinates, explicitly given by the constructed functionals.

theorem Cslib.Circuits.Rational.LaurentReduction.IntegralFrame.sum_coordinates {K : Type u_1} [Field K] {ι : Type u_2} {U : Submodule (F K) (ι → F K)} (b : IntegralFrame U) (x : ι → F K) (hx : x ∈ U) : ∑ j : Fin b.length, (b.coordinate j) x • b.vector j = x

theorem Cslib.Circuits.Rational.LaurentReduction.IntegralFrame.length_eq_finrank {K : Type u_1} [Field K] {ι : Type u_2} {U : Submodule (F K) (ι → F K)} (b : IntegralFrame U) : b.length = Module.finrank (F K) ↥U

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

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

theorem Cslib.Circuits.Rational.LaurentReduction.reduce_sum {K : Type u_1} [Field K] {ι : Type u_2} {τ : Type u_3} (s : Finset τ) (v : τ → ι → F K) : reduce (∑ j ∈ s, v j) = ∑ j ∈ s, reduce (v j)

theorem Cslib.Circuits.Rational.LaurentReduction.reduce_smul {K : Type u_1} [Field K] {ι : Type u_2} {a : F K} {v : ι → F K} (ha : Integral a) (hv : IntegralVector v) : reduce (a • v) = reduction a • reduce v

theorem Cslib.Circuits.Rational.LaurentReduction.reduce_C_smul {K : Type u_1} [Field K] {ι : Type u_2} (a : K) (v : ι → F K) : reduce (HahnSeries.C a • v) = a • reduce v

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)))

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))

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

theorem Cslib.Circuits.Rational.LaurentReduction.Integral.order_eq_zero {K : Type u_1} [Field K] {x : F K} (hx : Integral x) (hr : reduction x ≠ 0) : HahnSeries.order x = 0

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)

theorem Cslib.Circuits.Rational.LaurentReduction.weighted_high_reduction_zero {K : Type u_1} [Field K] {ι : Type u_2} (w : ι → ℕ) (A : ℕ) (x : ι → F K) (hx : IntegralVector x) (hlow : ∃ (j : ι), w j ≤ A ∧ reduction (x j) ≠ 0) (c : F K) (hc : c ≠ 0) (hy : IntegralVector (c • (weightMap w) x)) (i : ι) : A < w i → reduction ((c • (weightMap w) x) i) = 0

The key valuation step of order reversal: an integral normalized input having a nonzero low reduction cannot give a high leading output coefficient.

theorem Cslib.Circuits.Rational.LaurentReduction.reduction_weighted_supported {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] (w : ι → ℕ) (A : ℕ) (U : Submodule (F K) (ι → F K)) (hdetect : ∀ x ∈ U, IntegralVector x → (∀ (i : ι), w i ≤ A → reduction (x i) = 0) → reduce x = 0) (y : ι → F K) (hyU : y ∈ Submodule.map (weightMap w) U) (hyI : IntegralVector y) (i : ι) : A < w i → reduction (y i) = 0

Low coordinates detect reduction throughout U. This controls its full integral image lattice, not only the images of an arbitrary integral basis.

theorem Cslib.Circuits.Rational.LaurentReduction.exists_independent_subfamily {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {h : ℕ} (v : Fin h → V) : ∃ (k : ℕ) (a : Fin k → Fin h), Function.Injective a ∧ Submodule.span K (Set.range (v ∘ a)) = Submodule.span K (Set.range v) ∧ LinearIndependent K (v ∘ a)

def Cslib.Circuits.Rational.LaurentReduction.IntegralFrame.subframe {K : Type u_1} [Field K] {ι : Type u_2} {U : Submodule (F K) (ι → F K)} (b : IntegralFrame U) {k : ℕ} (a : Fin k → Fin b.length) (ha : Function.Injective a) : IntegralFrame (Submodule.span (F K) (Set.range (b.vector ∘ a)))

Restrict an integral frame to a selected family of basis vectors.

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

theorem Cslib.Circuits.Rational.LaurentReduction.exists_projection_subspace {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] {V : Type u_3} [AddCommGroup V] [Module K V] (U : Submodule (F K) (ι → F K)) (P : (ι → K) →ₗ[K] V) : ∃ U' ≤ U, Module.finrank (F K) ↥U' = Module.finrank K ↥(Submodule.map P (reducedSubspace U)) ∧ ∀ x ∈ U', IntegralVector x → P (reduce x) = 0 → reduce x = 0

Choose an integral-lattice subspace on whose reduction a specified projection is injective, of dimension equal to that projection's rank.

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

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

theorem Cslib.Circuits.Rational.LaurentReduction.liftMap_comp {K : Type u_1} [Field K] {ι : Type u_2} {κ : Type u_3} {τ : Type u_4} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (P : (κ → K) →ₗ[K] τ → K) (Q : (ι → K) →ₗ[K] κ → K) : liftMap (P ∘ₗ Q) = liftMap P ∘ₗ liftMap Q

theorem Cslib.Circuits.Rational.LaurentReduction.liftMap_id {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] : liftMap LinearMap.id = LinearMap.id

theorem Cslib.Circuits.Rational.LaurentReduction.liftMap_integral {K : Type u_1} [Field K] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] (P : (ι → K) →ₗ[K] κ → K) {x : ι → F K} (hx : IntegralVector x) : IntegralVector ((liftMap P) x)

theorem Cslib.Circuits.Rational.LaurentReduction.reduction_liftMap {K : Type u_1} [Field K] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] (P : (ι → K) →ₗ[K] κ → K) (x : ι → F K) : reduce ((liftMap P) x) = P (reduce x)

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

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

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

theorem Cslib.Circuits.Rational.LaurentReduction.reducedSubspace_liftEquiv {K : Type u_1} [Field K] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (E : (ι → K) ≃ₗ[K] κ → K) (U : Submodule (F K) (ι → F K)) : reducedSubspace (Submodule.map (↑(liftEquiv E)) U) = Submodule.map (↑E) (reducedSubspace U)

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)

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)

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