Multiples supported in a rectangle

The support equality in Lemma 2.1 (lem:supported) is support_mul_subset_rectangle_iff. Coordinate extrema of a nonzero product add: lexicographic refinement gives an extreme support pair whose sum has a unique representation and therefore a nonzero coefficient.

The definitions erosion and erodedWindow express containment of every translated filter-support point. The equality holds for empty erosion as well as for positive rectangles. The injective finite multiplier map and the associated dimension calculation from Lemma 2.1 are constructed in Nivat.Descent.ExactDescent, where they enter Theorem 2.2 (thm:descent).

def Nivat.Algebra.erosion (Φ : Laurent) (R : Finset Lattice) : Set Lattice

The eroded support window in Section 1.2, equation (eq:erosion-definition), and Lemma 2.1 (lem:supported): all translates of the filter support contained in the target.

Equations

• Nivat.Algebra.erosion Φ R = {z : Nivat.Lattice | ∀ a ∈ Φ.coeff.support, z + a ∈ R}

theorem Nivat.Algebra.erosion_finite (Φ : Laurent) (hΦ : Φ ≠ 0) (R : Finset Lattice) : (erosion Φ R).Finite

Auxiliary to Lemma 2.1 (lem:supported): erosion by a nonzero filter is finite because any one support point embeds it into a translate of the finite target window.

noncomputable def Nivat.Algebra.erodedWindow (Φ : Laurent) (hΦ : Φ ≠ 0) (R : Finset Lattice) : Finset Lattice

The finite-set form of the erosion in Lemma 2.1 (lem:supported), including empty erosion.

Equations

• Nivat.Algebra.erodedWindow Φ hΦ R = ⋯.toFinset

@[simp]

theorem Nivat.Algebra.mem_erodedWindow (Φ : Laurent) (hΦ : Φ ≠ 0) (R : Finset Lattice) (z : Lattice) : z ∈ erodedWindow Φ hΦ R ↔ ∀ a ∈ Φ.coeff.support, z + a ∈ R

The membership condition for the eroded window of Lemma 2.1 (lem:supported).

theorem Nivat.Algebra.support_mul_subset_rectangle_iff (Φ : Laurent) (hΦ : Φ ≠ 0) (g : Laurent) (m n : ℕ) : (Φ * g).coeff.support ⊆ rectangle m n ↔ g.coeff.support ⊆ erodedWindow Φ hΦ (rectangle m n)

The support equality in Lemma 2.1 (lem:supported): a multiple is supported in an axis-aligned rectangle exactly when its multiplier is supported in the erosion. The statement also covers zero side lengths and empty erosion.