A pair of rectangles returning to its source covers an annulus #
A term in the square of a grid differential is a pair of composable oriented rectangles. This
file treats the annular case, in which the second rectangle returns to the source of the
first: R runs from a grid state x to a grid state y and S runs from y back to x.
Such a pair is rigid. Both rectangles must use the same two side columns, because those columns
are exactly the columns in which x and y differ. There are therefore only two shapes. If S
starts on the same side column as R, then the two rectangles have the same columns and
complementary rows, and together they cover every square in a full vertical band. If S starts
on the other side column, then they have the same rows and complementary columns, and together
they cover every square in a full horizontal band. Either way the union of the covered squares is
a toroidal annulus, GridRectangleBetween.coveredSquares_union_coveredSquares.
A grid state occupies one square in every column and one square in every row, so it meets every
nonempty vertical band and every nonempty horizontal band
(GridState.not_disjoint_product_univ_pointSet and GridState.not_disjoint_univ_product_pointSet
of Diagram/Basic.lean). Consequently a grid state always meets the union of the squares covered
by a returning pair
(GridRectangleBetween.not_disjoint_coveredSquares_or_not_disjoint_coveredSquares).
The region a marking is tested against here is GridRectangle.coveredSquares: markings sit at the
centres of their squares, the convention fixed in Rectangle/Squares.lean and used by the gradings
and by the unblocked complex GC⁻. Applied to the O- or the X-markings of a grid diagram, both
of which are grid states, the last lemma therefore says that a returning pair of rectangles can
never consist of two rectangles disjoint from the markings' squares, so the annular terms vanish
for any grid differential whose marking-free test is that disjointness — in particular for the
X-test of the unblocked differential ∂⁻. The marking-avoidance predicate
GridRectangle.AvoidsMarkings tests that same region, coveredSquares, so the lemma serves
TauCeti.GridDiagram.fullyBlockedDifferential unchanged.
Main results #
TauCeti.GridRectangleBetween.sideColumns_eq_sideColumns: a returning pair of rectangles uses the same two side columns.TauCeti.GridRectangleBetween.left_right_eq_cases: the returning rectangle either has the same ordered side columns or the reversed ones.TauCeti.GridRectangleBetween.coveredSquares_union_coveredSquares: the squares covered by a returning pair are a full vertical band or a full horizontal band.TauCeti.GridRectangleBetween.disjoint_coveredSquares: the two rectangles of a returning pair cover disjoint squares.TauCeti.GridRectangleBetween.not_disjoint_coveredSquares_or_not_disjoint_coveredSquares: at least one rectangle of a returning pair covers a square occupied by any given grid state.
References #
This supplies the annular case split for
TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.3, "The complexes and ∂² = 0",
whose juxtaposition argument distinguishes disjoint, overlapping and annular pairs of empty
rectangles. The annular case follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and
Links, Chapter 4.6.
If a returning rectangle starts on the same side column as the outgoing one, then it also ends on the same side column.
If a returning rectangle starts on the terminal side column of the outgoing one, then it ends on the initial one.
The returning rectangle has either the same ordered side columns as the outgoing rectangle or the reversed ordered side columns.
A returning pair of rectangles uses the same unordered pair of side columns.
A returning rectangle starting on the initial side column starts on the terminal side row: its two rows are those of the outgoing rectangle, in the opposite order.
A returning rectangle starting on the initial side column ends on the initial side row.
A returning rectangle starting on the same side column covers the outgoing column arc and the complementary row arc.
A returning rectangle starting on the terminal side column has the same two side rows, in the same order, as the outgoing one.
A returning rectangle starting on the terminal side column ends on the terminal side row.
A returning rectangle starting on the terminal side column covers the complementary column arc and the outgoing row arc.
A returning pair whose two rectangles start on the same side column covers a full vertical band: the same columns as the outgoing rectangle, and every row.
A returning pair whose second rectangle starts on the other side column covers a full horizontal band: every column, and the same rows as the outgoing rectangle.
The squares covered by a returning pair of rectangles form a toroidal annulus: either a full vertical band or a full horizontal band.
The two rectangles of a returning pair cover disjoint sets of squares: they have the same columns and complementary rows, or the same rows and complementary columns.
A grid state meets the squares covered by a returning pair of rectangles.
At least one rectangle of a returning pair covers a square occupied by any given grid state.
Applied to the O- or X-markings of a grid diagram, this is the vanishing of the annular terms
in the square of a grid differential that tests markings by disjointness from
GridRectangle.coveredSquares, such as the unblocked differential ∂⁻: two rectangles that return
to their source can never both avoid the markings in that sense.
TauCeti.GridDiagram.fullyBlockedDifferential is such a differential too: its
GridRectangle.AvoidsMarkings predicate tests coveredSquares.