The exact annihilator ideal of a one-sided periodic configuration

The normalized lattice-basis form of Theorem 4.1 (thm:exact-ideal) is exact_line_in_basis. A nonzero configuration with a positive period along the first basis vector and vanishing on negative rows has a principal Laurent annihilator ideal. Its generator is a monic nonconstant divisor of the horizontal period polynomial.

First, exists_horizontal_period_generator constructs the exact one-variable generator. On the kernel of an irreducible horizontal polynomial, Bézout's identity makes every coprime coefficient injective. Evaluating a transverse relation at the first nonzero row then proves that the irreducible polynomial divides each transverse coefficient.

The theorem horizontal_generator_dvd_coefficients iterates this argument by degree. If the generator is π * ψ, apply the first-row argument to ψ(T)d, then divide each transverse coefficient by π and apply the induction to π(T)d, whose exact horizontal generator is ψ. Thus the argument accounts for every factor multiplicity. Clearing negative horizontal exponents by a monomial unit extends coefficient divisibility to all Laurent filters. Finally, exponent reindexing transports the equality through the lattice basis.

def Nivat.Algebra.horizontal : Lattice

Auxiliary to Theorem 4.1 (thm:exact-ideal): the first coordinate unit vector in the normalized lattice basis.

Equations

• Nivat.Algebra.horizontal = (1, 0)

def Nivat.Algebra.RowZero (d : Configuration ℚ) (b : ℤ) : Prop

Auxiliary to Theorem 4.1 (thm:exact-ideal): every entry on a specified full integer row vanishes.

Equations

• Nivat.Algebra.RowZero d b = ∀ (a : ℤ), d (a, b) = 0

theorem Nivat.Algebra.exists_monic_horizontal_generator {d : Configuration ℚ} (hex : ∃ (p : Polynomial ℚ), p ≠ 0 ∧ act ((lineEval horizontal) p) d = 0) : ∃ (φ : Polynomial ℚ), φ.Monic ∧ ∀ (p : Polynomial ℚ), act ((lineEval horizontal) p) d = 0 ↔ φ ∣ p

Auxiliary to Theorem 4.1 (thm:exact-ideal): normalize the generator of a nonzero horizontal annihilator ideal to obtain a monic polynomial with exact one-variable divisibility.

theorem Nivat.Algebra.exists_horizontal_period_generator {d : Configuration ℚ} (hd : d ≠ 0) {q : ℕ} (hq : 0 < q) (hperiod : IsPeriod d (↑q, 0)) : ∃ (φ : Polynomial ℚ), φ.Monic ∧ 0 < φ.natDegree ∧ φ ∣ Polynomial.X ^ q - 1 ∧ ∀ (p : Polynomial ℚ), act ((lineEval horizontal) p) d = 0 ↔ φ ∣ p

Auxiliary to Theorem 4.1 (thm:exact-ideal): a positive horizontal period gives a monic, nonconstant exact horizontal generator dividing the period polynomial.

theorem Nivat.Algebra.lineEval_monomial (v : Lattice) (n : ℕ) (a : ℚ) : (lineEval v) ((Polynomial.monomial n) a) = AddMonoidAlgebra.single (n • v) a

Auxiliary to Theorem 4.1 (thm:exact-ideal): evaluation of a polynomial monomial gives its coefficient at the scaled lattice exponent.

theorem Nivat.Algebra.rowZero_horizontal_act (p : Polynomial ℚ) {d : Configuration ℚ} {b : ℤ} (hd : RowZero d b) : RowZero (act ((lineEval horizontal) p) d) b

Auxiliary to Theorem 4.1 (thm:exact-ideal): a horizontal polynomial preserves a zero row because its shifts stay on that row.

theorem Nivat.Algebra.act_comm (f g : Laurent) (d : Configuration ℚ) : act f (act g d) = act g (act f d)

Auxiliary to Theorem 4.1 (thm:exact-ideal): two Laurent operators commute because multiplication in the Laurent ring is commutative.

theorem Nivat.Algebra.act_config_finset_sum {ι : Type u_1} (f : Laurent) (S : Finset ι) (d : ι → Configuration ℚ) : act f (∑ j ∈ S, d j) = ∑ j ∈ S, act f (d j)

Auxiliary to Theorem 4.1 (thm:exact-ideal): a Laurent operator distributes over a finite sum of configurations.

theorem Nivat.Algebra.irreducible_dvd_coefficients_of_sum_eq_zero {π : Polynomial ℚ} (hπ : Irreducible π) {d : Configuration ℚ} (hd : d ≠ 0) (hbelow : ∃ (B : ℤ), ∀ b < B, RowZero d b) (hker : act ((lineEval horizontal) π) d = 0) (S : Finset ℤ) (p : ℤ → Polynomial ℚ) (hsum : ∑ j ∈ S, act ((lineEval horizontal) (p j)) (shift (0, j) d) = 0) (j : ℤ) : j ∈ S → π ∣ p j

Auxiliary to Theorem 4.1 (thm:exact-ideal): on the kernel of an irreducible horizontal polynomial, every coefficient of a vanishing transverse relation is divisible by that polynomial. The greatest nondivisible coefficient is isolated at the first nonzero row, contradicting Bézout.

theorem Nivat.Algebra.horizontal_generator_dvd_coefficients (φ : Polynomial ℚ) (hφ : φ ≠ 0) (d : Configuration ℚ) (hexact : ∀ (p : Polynomial ℚ), act ((lineEval horizontal) p) d = 0 ↔ φ ∣ p) (hbelow : ∃ (B : ℤ), ∀ b < B, RowZero d b) (S : Finset ℤ) (p : ℤ → Polynomial ℚ) (hsum : ∑ j ∈ S, act ((lineEval horizontal) (p j)) (shift (0, j) d) = 0) (j : ℤ) : j ∈ S → φ ∣ p j

Auxiliary to Theorem 4.1 (thm:exact-ideal): every coefficient of a vanishing transverse relation is divisible by the exact horizontal generator. Degree induction removes an irreducible factor from both the generator and the coefficients, including its full multiplicity.

theorem Nivat.Algebra.act_filter_finset_sum {ι : Type u_1} (S : Finset ι) (f : ι → Laurent) (d : Configuration ℚ) : act (∑ j ∈ S, f j) d = ∑ j ∈ S, act (f j) d

Auxiliary to Theorem 4.1 (thm:exact-ideal): the action distributes over a finite sum of Laurent filters.

theorem Nivat.Algebra.horizontal_annihilates_iff (φ : Polynomial ℚ) (hφ : φ ≠ 0) (d : Configuration ℚ) (hexact : ∀ (p : Polynomial ℚ), act ((lineEval horizontal) p) d = 0 ↔ φ ∣ p) (hbelow : ∃ (B : ℤ), ∀ b < B, RowZero d b) (f : Laurent) : act f d = 0 ↔ (lineEval horizontal) φ ∣ f

Auxiliary to Theorem 4.1 (thm:exact-ideal): clearing horizontal exponents and cancelling the monomial unit extends exact coefficient divisibility to every Laurent filter.

theorem Nivat.Algebra.exact_horizontal_line {d : Configuration ℚ} (hd : d ≠ 0) {q : ℕ} (hq : 0 < q) (hperiod : IsPeriod d (↑q, 0)) (hbelow : ∀ b < 0, RowZero d b) : ∃ (φ : Polynomial ℚ), φ.Monic ∧ 0 < φ.natDegree ∧ φ ∣ Polynomial.X ^ q - 1 ∧ ∀ (f : Laurent), act f d = 0 ↔ (lineEval (1, 0)) φ ∣ f

Theorem 4.1 (thm:exact-ideal) in horizontal coordinates: the whole Laurent annihilator ideal of the one-sided periodic configuration has a monic nonconstant horizontal generator dividing the period polynomial.

noncomputable def Nivat.Algebra.laurentReindex (e : Lattice ≃+ Lattice) : Laurent ≃ₐ[ℚ] Laurent

Auxiliary to Theorem 4.1 (thm:exact-ideal): an integer lattice basis reindexes exponents by an algebra equivalence of the Laurent ring.

Equations

• Nivat.Algebra.laurentReindex e = AddMonoidAlgebra.domCongr ℚ ℚ e

theorem Nivat.Algebra.act_reindex_apply (e : Lattice ≃+ Lattice) (f : Laurent) (d : Configuration ℚ) (z : Lattice) : act ((laurentReindex e) f) d (e z) = act f (d ∘ ⇑e) z

Auxiliary to Theorem 4.1 (thm:exact-ideal): exponent reindexing and configuration precomposition give the same operator value at corresponding sites.

theorem Nivat.Algebra.act_reindex_eq_zero_iff (e : Lattice ≃+ Lattice) (f : Laurent) (d : Configuration ℚ) : act ((laurentReindex e) f) d = 0 ↔ act f (d ∘ ⇑e) = 0

Auxiliary to Theorem 4.1 (thm:exact-ideal): annihilator equations are preserved in both directions by a lattice basis change.

theorem Nivat.Algebra.laurentReindex_lineEval (e : Lattice ≃+ Lattice) (v : Lattice) (p : Polynomial ℚ) : (laurentReindex e) ((lineEval v) p) = (lineEval (e v)) p

Auxiliary to Theorem 4.1 (thm:exact-ideal): a basis change takes evaluation along a vector to evaluation along its image.

theorem Nivat.Algebra.exact_line_in_basis (e : Lattice ≃+ Lattice) {d : Configuration ℚ} (hd : d ≠ 0) {q : ℕ} (hq : 0 < q) (hperiod : IsPeriod d (e (↑q, 0))) (hbelow : ∀ b < 0, ∀ (a : ℤ), d (e (a, b)) = 0) : ∃ (φ : Polynomial ℚ), φ.Monic ∧ 0 < φ.natDegree ∧ φ ∣ Polynomial.X ^ q - 1 ∧ ∀ (f : Laurent), act f d = 0 ↔ (lineEval (e (1, 0))) φ ∣ f

Theorem 4.1 (thm:exact-ideal) in an arbitrary integer lattice basis. The first basis vector is the primitive period direction; negative second coordinates lie in the vanishing half-plane. The conclusion identifies every Laurent annihilator in the original lattice coordinates with a multiple of the line generator.