Finiteness of nonnegative integer vectors in subgroup cosets

Dickson's lemma shows that each coset of a subgroup of ι → ℤ has finitely many nonnegative vectors exactly when the subgroup has no nonzero nonnegative vector. For periodic domains of a pointed Heegaard diagram, this is the algebraic finiteness result used in the admissibility argument of Ozsváth–Szabó, Holomorphic disks and topological invariants for closed three-manifolds, Lemma 4.13. Applying it to Whitney disk classes also requires a geometric correspondence with domain vectors and control of its fibers.

Main result

• AddSubgroup.finite_setOf_nonneg_sub_mem_iff.

theorem AddSubgroup.finite_setOf_nonneg_sub_mem_iff {ι : Type u_1} [Finite ι] (P : AddSubgroup (ι → ℤ)) : (∀ (D₀ : ι → ℤ), {D : ι → ℤ | 0 ≤ D ∧ D - D₀ ∈ P}.Finite) ↔ ∀ p ∈ P, 0 ≤ p → p = 0

A subgroup P of ι → ℤ contains no nonzero nonnegative vector exactly when each coset D₀ + P contains only finitely many nonnegative vectors.