Documentation

LeanPool.Nivat.Algebra.RationalScaling

Integer scaling for the product-annihilator theorem #

Appendix A (app:product), proving Proposition 3.3 (prop:product), begins by scaling the finite rational alphabet and the finite filter coefficients separately. finiteRange_integer_scale and integer_filter_scale provide the two nonzero multipliers. The map intLaurentCast changes only the coefficient ring, so the resulting equations still concern the full integer lattice.

source
@[reducible, inline]
abbrev Nivat.Algebra.IntegerLaurent :
Type

The integer-coefficient Laurent ring used in Appendix A (app:product) to prove Proposition 3.3 (prop:product).

Equations
Instances For
    source
    noncomputable def Nivat.Algebra.intLaurentCast :
    IntegerLaurent →+* Laurent

    The coefficient embedding from integer to rational Laurent polynomials in Appendix A (app:product), preserving every lattice exponent.

    Equations
    Instances For
      source
      @[simp]
      theorem Nivat.Algebra.intLaurentCast_coeff (F : IntegerLaurent) (h : Lattice) :
      (intLaurentCast F).coeff h = ↑(F.coeff h)

      Auxiliary to the scaling step of Appendix A (app:product): coefficient embedding acts pointwise by the integer-to-rational cast.

      source
      theorem Nivat.Algebra.finite_set_integer_scale (S : Set ℚ) (hS : S.Finite) :
      ∃ (n : ℤ), n ≠ 0 ∧ ∀ x ∈ S, ∃ (a : ℤ), ↑n * x = ↑a

      The common-denominator step in Appendix A (app:product): one nonzero integer multiplier makes every element of a finite rational set integral.

      source
      theorem Nivat.Algebra.finiteRange_integer_scale {c : Configuration ℚ} (hc : FiniteRange c) :
      ∃ (n : ℤ), n ≠ 0 ∧ ∃ (C : Configuration ℤ), FiniteRange C ∧ ∀ (z : Lattice), ↑n * c z = ↑(C z)

      The configuration scaling step of Appendix A (app:product): a nonzero integer multiple of a finite-range rational configuration has finite integer range.

      source
      theorem Nivat.Algebra.integer_filter_scale (f : Laurent) :
      ∃ (n : ℤ), n ≠ 0 ∧ ∃ (F : IntegerLaurent), intLaurentCast F = ↑n • f

      The filter scaling step of Appendix A (app:product): a rational Laurent polynomial has a nonzero integer multiple represented by an integer-coefficient filter.