Documentation

LeanPool.Nivat.Algebra.Action

Laurent polynomial operators #

This module implements the notation of Section 1.1. Laurent is the rational Laurent ring, act is its forward-shift action, and lineEval substitutes a lattice monomial into an ordinary polynomial.

The principal identities are act_apply, act_mul, act_difference, and act_lineEval_X_pow_sub_one. The theorem finiteRange_act verifies that the class of finite-range rational configurations is closed under every operator.

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

Section 1.1 (Notation): the rational Laurent polynomial ring on the full integer lattice.

Equations
Instances For
    source
    def Nivat.Algebra.shiftLinear (h : Lattice) :
    Module.End ℚ (Configuration ℚ)

    Section 1.1 (Notation): a forward lattice translation as a rational linear endomorphism.

    Equations
    Instances For
      source
      @[simp]
      theorem Nivat.Algebra.shiftLinear_apply (h : Lattice) (c : Configuration ℚ) :
      (shiftLinear h) c = shift h c

      Section 1.1 (Notation): the bundled translation evaluates to the forward shift.

      source
      def Nivat.Algebra.shiftRepresentation :
      Multiplicative Lattice →* Module.End ℚ (Configuration ℚ)

      Section 1.1 (Notation): the additive lattice acts on configurations by commuting forward shifts.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Nivat.Algebra.actionHom :
        Laurent →ₐ[ℚ] Module.End ℚ (Configuration ℚ)

        Section 1.1 (Notation): the algebra homomorphism extending lattice translations to Laurent filters.

        Equations
        Instances For
          source
          noncomputable def Nivat.Algebra.act (f : Laurent) (c : Configuration ℚ) :
          Configuration ℚ

          Section 1.1 (Notation): the finite Laurent polynomial operator applied to a rational configuration.

          Equations
          Instances For
            source
            theorem Nivat.Algebra.act_apply (f : Laurent) (c : Configuration ℚ) (z : Lattice) :
            act f c z = f.coeff.sum fun (h : Lattice) (a : ℚ) => a * c (z + h)

            Section 1.1 (Notation): the operator is the finite sum of coefficients times forward-shifted values.

            source
            @[simp]
            theorem Nivat.Algebra.act_zero (c : Configuration ℚ) :
            act 0 c = 0

            Section 1.1 (Notation): the zero filter sends every configuration to zero.

            source
            @[simp]
            theorem Nivat.Algebra.act_one (c : Configuration ℚ) :
            act 1 c = c

            Section 1.1 (Notation): the constant filter one acts as the identity.

            source
            theorem Nivat.Algebra.act_add (f g : Laurent) (c : Configuration ℚ) :
            act (f + g) c = act f c + act g c

            Section 1.1 (Notation): adding filters adds their outputs.

            source
            theorem Nivat.Algebra.act_mul (f g : Laurent) (c : Configuration ℚ) :
            act (f * g) c = act f (act g c)

            Section 1.1 (Notation): multiplying filters composes their operators.

            source
            theorem Nivat.Algebra.act_sub (f g : Laurent) (c : Configuration ℚ) :
            act (f - g) c = act f c - act g c

            Section 1.1 (Notation): subtracting filters subtracts their outputs.

            source
            theorem Nivat.Algebra.act_neg (f : Laurent) (c : Configuration ℚ) :
            act (-f) c = -act f c

            Section 1.1 (Notation): negating a filter negates its output.

            source
            @[simp]
            theorem Nivat.Algebra.act_config_zero (f : Laurent) :
            act f 0 = 0

            Section 1.1 (Notation): every Laurent filter annihilates the zero configuration.

            source
            theorem Nivat.Algebra.act_config_add (f : Laurent) (c d : Configuration ℚ) :
            act f (c + d) = act f c + act f d

            Section 1.1 (Notation): each Laurent operator preserves sums of configurations.

            source
            theorem Nivat.Algebra.act_config_sub (f : Laurent) (c d : Configuration ℚ) :
            act f (c - d) = act f c - act f d

            Section 1.1 (Notation): each Laurent operator preserves differences of configurations.

            source
            theorem Nivat.Algebra.act_config_smul (f : Laurent) (a : ℚ) (c : Configuration ℚ) :
            act f (a • c) = a • act f c

            Section 1.1 (Notation): each Laurent operator commutes with rational scaling of the configuration.

            source
            theorem Nivat.Algebra.act_smul (a : ℚ) (f : Laurent) (c : Configuration ℚ) :
            act (a • f) c = a • act f c

            Section 1.1 (Notation): rational scaling of the filter scales its output.

            source
            @[simp]
            theorem Nivat.Algebra.act_single (h : Lattice) (a : ℚ) (c : Configuration ℚ) :
            act (AddMonoidAlgebra.single h a) c = a • shift h c

            Section 1.1 (Notation): a single supported coefficient acts by scaling a forward shift.

            source
            noncomputable def Nivat.Algebra.monomial (h : Lattice) :
            Laurent

            Section 1.1 (Notation): the lattice monomial with exponent h and coefficient one.

            Equations
            Instances For
              source
              @[simp]
              theorem Nivat.Algebra.monomial_zero :
              monomial 0 = 1

              Section 1.1 (Notation): the zero-exponent monomial is the multiplicative identity.

              source
              @[simp]
              theorem Nivat.Algebra.monomial_mul (h t : Lattice) :
              monomial h * monomial t = monomial (h + t)

              Section 1.1 (Notation): multiplication of lattice monomials adds their exponents.

              source
              @[simp]
              theorem Nivat.Algebra.monomial_pow (h : Lattice) (q : ℕ) :
              monomial h ^ q = monomial (q • h)

              Section 1.1 (Notation): a natural power of a monomial scales its exponent.

              source
              theorem Nivat.Algebra.monomial_isUnit (h : Lattice) :
              IsUnit (monomial h)

              Section 1.1 (Notation): every lattice monomial is a unit, with inverse at the negated exponent.

              source
              theorem Nivat.Algebra.monomial_ne_zero (h : Lattice) :
              monomial h ≠ 0

              Section 1.1 (Notation): a lattice monomial has a nonzero coefficient and is nonzero.

              source
              theorem Nivat.Algebra.monomial_injective :
              Function.Injective monomial

              Section 1.1 (Notation): distinct lattice exponents give distinct monomials.

              source
              theorem Nivat.Algebra.monomial_sub_one_ne_zero {h : Lattice} (hh : h ≠ 0) :
              monomial h - 1 ≠ 0

              Section 1.1 (Notation): a nonzero direction gives a nonzero difference polynomial.

              source
              @[simp]
              theorem Nivat.Algebra.act_monomial (h : Lattice) (c : Configuration ℚ) :
              act (monomial h) c = shift h c

              Section 1.1 (Notation): a lattice monomial acts by its forward shift.

              source
              theorem Nivat.Algebra.act_difference (h : Lattice) (c : Configuration ℚ) :
              act (monomial h - 1) c = difference h c

              Section 1.1 (Notation): the polynomial monomial h - 1 acts by the difference operator in direction h.

              source
              theorem Nivat.Algebra.act_shift (f : Laurent) (h : Lattice) (c : Configuration ℚ) :
              act f (shift h c) = shift h (act f c)

              Section 1.1 (Notation): every Laurent operator commutes with lattice translations.

              source
              theorem Nivat.Algebra.act_difference_comm (f : Laurent) (h : Lattice) (c : Configuration ℚ) :
              act f (difference h c) = difference h (act f c)

              Section 1.1 (Notation): every Laurent operator commutes with lattice differences.

              source
              theorem Nivat.Algebra.finiteRange_const (a : ℚ) :
              FiniteRange fun (x : Lattice) => a

              Section 1.1 (Notation): a constant rational configuration has finite range.

              source
              theorem Nivat.Algebra.finiteRange_add {c d : Configuration ℚ} (hc : FiniteRange c) (hd : FiniteRange d) :
              FiniteRange (c + d)

              Section 1.1 (Notation): the sum of two finite-range rational configurations has finite range.

              source
              theorem Nivat.Algebra.finiteRange_smul {c : Configuration ℚ} (hc : FiniteRange c) (a : ℚ) :
              FiniteRange (a • c)

              Section 1.1 (Notation): rational scaling preserves finite range.

              source
              theorem Nivat.Algebra.finiteRange_act (f : Laurent) {c : Configuration ℚ} (hc : FiniteRange c) :
              FiniteRange (act f c)

              Section 1.1 (Notation): the finite sum defining a Laurent operator preserves finite rational range.

              source
              noncomputable def Nivat.Algebra.lineEval (v : Lattice) :
              Polynomial ℚ →+* Laurent

              Section 1.1 (Notation): substitute the lattice monomial in direction v for a polynomial variable.

              Equations
              Instances For
                source
                @[simp]
                theorem Nivat.Algebra.lineEval_X (v : Lattice) :
                (lineEval v) Polynomial.X = monomial v

                Section 1.1 (Notation): the polynomial variable evaluates to the monomial in direction v.

                source
                @[simp]
                theorem Nivat.Algebra.lineEval_C (v : Lattice) (a : ℚ) :
                (lineEval v) (Polynomial.C a) = AddMonoidAlgebra.single 0 a

                Section 1.1 (Notation): a constant polynomial evaluates to the corresponding zero-exponent Laurent coefficient.

                source
                theorem Nivat.Algebra.lineEval_dvd (v : Lattice) {f g : Polynomial ℚ} (h : f ∣ g) :
                (lineEval v) f ∣ (lineEval v) g

                Section 1.1 (Notation): substitution along a lattice direction preserves polynomial divisibility.

                source
                @[simp]
                theorem Nivat.Algebra.lineEval_X_pow (v : Lattice) (q : ℕ) :
                (lineEval v) (Polynomial.X ^ q) = monomial (q • v)

                Section 1.1 (Notation): a power of the polynomial variable evaluates to a scaled lattice exponent.

                source
                theorem Nivat.Algebra.lineEval_X_pow_sub_one (v : Lattice) (q : ℕ) :
                (lineEval v) (Polynomial.X ^ q - 1) = monomial (q • v) - 1

                Section 1.1 (Notation): the period polynomial evaluates to the difference polynomial in direction q • v.

                source
                theorem Nivat.Algebra.act_lineEval_X_pow_sub_one (v : Lattice) (q : ℕ) (c : Configuration ℚ) :
                act ((lineEval v) (Polynomial.X ^ q - 1)) c = difference (q • v) c

                Section 1.1 (Notation): the evaluated period polynomial acts as the difference in direction q • v.