Cancelling recut partners in a family of two-step domains

The recut (TauCeti.GridRectangleDecomposition.recut) pairs a decomposition by two empty rectangles sharing exactly one side column with a second such decomposition of the same domain. Juxtaposition arguments apply it to families of two-step domains whose members carry more data than their rectangles: a hexagon and a rectangle, say, counted with a weight. This file isolates the cancellation step shared by these arguments.

Let S be a finite family of domains from x to z ≠ x, each with an underlying decomposition by two empty rectangles, such that a member is determined by its decomposition and members repartitioning the same squares have the same weight. A member whose rectangles share a side column and whose recut is again the decomposition of a member has a unique such partner, which has the member as its own partner, and the two weights agree. If the weights lie in an additive monoid in which every element is its own negative, as in characteristic two, these pairs cancel, so the members whose rectangles share a side column have the total weight of the unpaired ones.

Main results

• GridRectangleDecomposition.sum_filter_not_hasDisjointSides_eq_sum_filter_forall_not_isRecut: the recut cancellation in a family of two-step domains.

References

This is the cancellation of juxtaposed domains in Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, AMS Mathematical Surveys and Monographs 208, 2015, Sections 4.6 and 5.1.

theorem TauCeti.GridRectangleDecomposition.sum_filter_not_hasDisjointSides_eq_sum_filter_forall_not_isRecut {n : ℕ} {x z : GridState n} {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (S : Finset α) (f : α → GridRectangleDecomposition x z) (w : α → M) (hM : ∀ (m : M), m + m = 0) (hzx : z ≠ x) (hempty : ∀ D ∈ S, (f D).first.IsEmpty ∧ (f D).second.IsEmpty) (hinj : Set.InjOn f ↑S) (hw : ∀ D ∈ S, ∀ E ∈ S, (f D).IsRepartition (f E) → w D = w E) : ∑ D ∈ S with ¬(f D).HasDisjointSides, w D = ∑ D ∈ S with ¬(f D).HasDisjointSides ∧ ∀ E ∈ S, ¬(f D).IsRecut (f E), w D

Recut cancellation. Let S be a finite family of domains from x to z ≠ x, with underlying decompositions f D by two empty rectangles, such that f is injective on S and the weight w agrees on members whose decompositions repartition the same squares. If m + m = 0 for every weight m, as in characteristic two, the members whose rectangles share a side column have the total weight of those among them whose recut is the decomposition of no member.