Counting differences within fibers

The finite-set argument at the end of Theorem 2.2 (thm:descent) in paper/nivat.tex. A fiber with k inputs needs at most k - 1 generators for all of its differences. finite_fiber_budget sums that bound over the fibers.

The argument uses an arbitrary function between sets of vectors. The application to a Laurent filter is in Nivat.Descent.ExactDescent.

def Nivat.Descent.fiberDifferences {V : Type u_2} {W : Type u_3} [AddCommGroup V] (F : V → W) (P : Set V) : Set V

Differences between members of one fiber. This is the generating set in the counting step of Theorem 2.2 (thm:descent).

Equations

• Nivat.Descent.fiberDifferences F P = {d : V | ∃ x ∈ P, ∃ y ∈ P, F x = F y ∧ d = x - y}

theorem Nivat.Descent.finiteDimensional_fiberDifferences {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] (F : V → W) {P : Set V} (hP : P.Finite) : FiniteDimensional K ↥(Submodule.span K (fiberDifferences F P))

A finite input set yields a finite-dimensional space of same-fiber differences. This is the finite-span step in Theorem 2.2 (thm:descent).

theorem Nivat.Descent.finite_fiber_budget {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] (F : V → W) {P : Set V} (hP : P.Finite) : Module.finrank K ↥(Submodule.span K (fiberDifferences F P)) + (F '' P).ncard ≤ P.ncard

The fiber-counting inequality in Theorem 2.2 (thm:descent). It holds for any function on a finite set of vectors; neither linearity nor a finite-dimensional ambient space is needed.