Side-column overlap in two-step rectangle decompositions

A term in the square of the grid differential is a pair of composable rectangles. The juxtaposition proof of ∂² = 0 splits according to how the two pairs of vertical sides meet. This file makes that split exact: the pairs are disjoint, have one common column, or coincide. The last case occurs exactly when the two rectangle moves return to the source state.

The finite set GridRectangleDecomposition.commonSideColumns is the intersection of the two two-element side sets. Its cardinality is therefore at most two. Cardinality zero is the predicate HasDisjointSides; cardinality one is named HasOneCommonSide; and cardinality two is equivalent to equality of the source and target states. Consequently a nondiagonal coefficient of the differential square has precisely the two geometric cases of the rectangle pairing: disjoint rectangles or rectangles sharing exactly one side column.

Main definitions

• TauCeti.GridRectangleDecomposition.commonSideColumns: the side columns used by both rectangles in a decomposition.
• TauCeti.GridRectangleDecomposition.HasOneCommonSide: the two rectangles share exactly one side column.
• TauCeti.GridRectangleDecomposition.HasSameSideOverlap and TauCeti.GridRectangleDecomposition.HasMixedSideOverlap: the common column has the same or opposite orientation in the two rectangles.

Main results

• TauCeti.GridRectangleDecomposition.card_commonSideColumns_le_two: at most two side columns are common.
• TauCeti.GridRectangleDecomposition.card_commonSideColumns_eq_two_iff: both side columns are common exactly for a diagonal two-step path.
• TauCeti.GridRectangleDecomposition.hasOneCommonSide_iff_sameSideOverlap_or_mixedSideOverlap: the same-side and mixed-side orientations exhaust the one-common-side case.
• TauCeti.GridRectangleDecomposition.sum_filter_not_hasDisjointSides_eq_sameSide_add_mixedSide: off the diagonal, any weighted family splits into its two overlap orientations.
• TauCeti.GridRectangleDecomposition.hasDisjointSides_or_hasOneCommonSide_or_eq: every decomposition belongs to one of the three cases.
• TauCeti.GridRectangleDecomposition.hasDisjointSides_of_disjoint: a decomposition whose target applies two disjoint column transpositions has disjoint side pairs.
• TauCeti.GridRectangleDecomposition.target_ne_source_iff: a decomposition is nondiagonal exactly when its sides are disjoint or have exactly one column in common.
• TauCeti.GridRectangleDecomposition.sideColumns_ne_of_hasOneCommonSide: sharing exactly one side column means the two side pairs differ.
• TauCeti.GridRectangleDecomposition.hasOneCommonSide_of_mem_commonSideColumns: a nondiagonal decomposition with a common side column has exactly one.
• TauCeti.GridRectangleDecomposition.hasOneCommonSide_of_right_eq_left_of_ne and TauCeti.GridRectangleDecomposition.hasOneCommonSide_of_left_eq_right_of_ne: off the diagonal, two rectangles sharing a grid line with opposite orientations share no other side.
• TauCeti.GridRectangleDecomposition.target_apply_ne_iff_mem_sideColumns_union: when exactly one side is common, the three side columns are precisely the columns moved between the endpoint states.
• TauCeti.GridRectangleDecomposition.sideColumns_union_eq_of_hasOneCommonSide: two decompositions between the same endpoint states, one of which has one common side, use the same three columns.

References

The split is the opening bookkeeping of the juxtaposition proof in Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.6.

def TauCeti.GridRectangleDecomposition.commonSideColumns {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : Finset (Fin n)

The columns which are sides of both rectangles in a two-step decomposition.

@[simp]

theorem TauCeti.GridRectangleDecomposition.mem_commonSideColumns {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (c : Fin n) : c ∈ D.commonSideColumns ↔ c ∈ D.first.sideColumns ∧ c ∈ D.second.sideColumns

A column is common to the two rectangles exactly when it is a side of each one.

theorem TauCeti.GridRectangleDecomposition.card_commonSideColumns_le_two {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.commonSideColumns.card ≤ 2

At most two columns are sides of both rectangles in a decomposition.

def TauCeti.GridRectangleDecomposition.HasOneCommonSide {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : Prop

Two rectangles in a decomposition share exactly one side column.

def TauCeti.GridRectangleDecomposition.HasSameSideOverlap {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : Prop

Two rectangles share exactly one side column, with that column initial for both rectangles or terminal for both rectangles.

def TauCeti.GridRectangleDecomposition.HasMixedSideOverlap {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : Prop

Two rectangles share exactly one side column, with that column initial for one rectangle and terminal for the other.

theorem TauCeti.GridRectangleDecomposition.hasSameSideOverlap_iff {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.HasSameSideOverlap ↔ D.HasOneCommonSide ∧ (D.first.left = D.second.left ∨ D.first.right = D.second.right)

The defining alternatives for a same-side overlap.

theorem TauCeti.GridRectangleDecomposition.hasMixedSideOverlap_iff {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.HasMixedSideOverlap ↔ D.HasOneCommonSide ∧ (D.first.left = D.second.right ∨ D.first.right = D.second.left)

The defining alternatives for a mixed-side overlap.

theorem TauCeti.GridRectangleDecomposition.hasOneCommonSide_iff_existsUnique {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.HasOneCommonSide ↔ ∃! c : Fin n, c ∈ D.first.sideColumns ∧ c ∈ D.second.sideColumns

Having one common side means that there is a unique column which is a side of both rectangles.

theorem TauCeti.GridRectangleDecomposition.hasOneCommonSide_of_left_eq_left {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hcommon : D.first.left = D.second.left) (hother : D.first.right ≠ D.second.right) : D.HasOneCommonSide

Two rectangles sharing their initial side and having distinct terminal sides share exactly one side column.

theorem TauCeti.GridRectangleDecomposition.hasOneCommonSide_of_right_eq_right {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hcommon : D.first.right = D.second.right) (hother : D.first.left ≠ D.second.left) : D.HasOneCommonSide

Two rectangles sharing their terminal side and having distinct initial sides share exactly one side column.

theorem TauCeti.GridRectangleDecomposition.hasOneCommonSide_of_left_eq_left_of_mem_cIoo {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hcommon : D.first.left = D.second.left) (hcol : D.second.right ∈ Grid.cIoo D.first.left D.first.right) : D.HasOneCommonSide

Two rectangles sharing their initial side, the second ending strictly inside the first's column interval, share exactly one side column.

theorem TauCeti.GridRectangleDecomposition.hasOneCommonSide_of_right_eq_left {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hcommon : D.first.right = D.second.left) (hother : D.first.left ≠ D.second.right) : D.HasOneCommonSide

Two rectangles, the first ending where the second starts, whose other sides differ share exactly one side column.

theorem TauCeti.GridRectangleDecomposition.hasOneCommonSide_of_left_eq_right {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hcommon : D.first.left = D.second.right) (hother : D.first.right ≠ D.second.left) : D.HasOneCommonSide

Two rectangles, the first starting where the second ends, whose other sides differ share exactly one side column.

theorem TauCeti.GridRectangleDecomposition.side_eq_cases_of_hasOneCommonSide {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasOneCommonSide) : D.first.left = D.second.left ∧ D.first.right ≠ D.second.right ∨ D.first.left = D.second.right ∧ D.first.right ≠ D.second.left ∨ D.first.right = D.second.left ∧ D.first.left ≠ D.second.right ∨ D.first.right = D.second.right ∧ D.first.left ≠ D.second.left

If two rectangles share exactly one side column, that column occurs in one of the four possible ordered-side positions, and the two noncommon sides are distinct.

theorem TauCeti.GridRectangleDecomposition.hasSameSideOverlap_or_hasMixedSideOverlap {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasOneCommonSide) : D.HasSameSideOverlap ∨ D.HasMixedSideOverlap

An overlap of exactly one side is either same-side or mixed-side.

theorem TauCeti.GridRectangleDecomposition.hasOneCommonSide_iff_sameSideOverlap_or_mixedSideOverlap {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.HasOneCommonSide ↔ D.HasSameSideOverlap ∨ D.HasMixedSideOverlap

Sharing exactly one side is equivalent to having a same-side or mixed-side overlap.

theorem TauCeti.GridRectangleDecomposition.not_hasMixedSideOverlap_of_hasSameSideOverlap {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasSameSideOverlap) : ¬D.HasMixedSideOverlap

Same-side and mixed-side overlaps are mutually exclusive.

theorem TauCeti.GridRectangleDecomposition.card_sideColumns_union_eq_three {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasOneCommonSide) : (D.first.sideColumns ∪ D.second.sideColumns).card = 3

If two rectangles share exactly one side column, their union of side columns has cardinality three.

theorem TauCeti.GridRectangleDecomposition.target_apply_ne_iff_mem_sideColumns_union {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasOneCommonSide) (c : Fin n) : z.toPerm c ≠ x.toPerm c ↔ c ∈ D.first.sideColumns ∪ D.second.sideColumns

When two rectangles share exactly one side column, their three side columns are precisely the columns on which the target state differs from the source state.

@[simp]

theorem TauCeti.GridRectangleDecomposition.commonSideColumns_eq_empty_iff {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.commonSideColumns = ∅ ↔ D.HasDisjointSides

The two side pairs are disjoint exactly when their common-side set is empty.

theorem TauCeti.GridRectangleDecomposition.card_commonSideColumns_eq_zero_iff {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.commonSideColumns.card = 0 ↔ D.HasDisjointSides

The common-side set has cardinality zero exactly when the side pairs are disjoint.

This is not a separate simp lemma: Finset.card_eq_zero followed by commonSideColumns_eq_empty_iff already gives the same normal form.

theorem TauCeti.GridRectangleDecomposition.target_eq_source_iff_sideColumns_eq {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : z = x ↔ D.first.sideColumns = D.second.sideColumns

A two-step rectangle path returns to its source exactly when its two rectangles use the same unordered pair of side columns.

@[simp]

theorem TauCeti.GridRectangleDecomposition.card_commonSideColumns_eq_two_iff {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.commonSideColumns.card = 2 ↔ z = x

Both side columns are common exactly when the two-step rectangle path returns to its source.

theorem TauCeti.GridRectangleDecomposition.hasDisjointSides_or_hasOneCommonSide_or_eq {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.HasDisjointSides ∨ D.HasOneCommonSide ∨ z = x

Every two-step rectangle decomposition has disjoint sides, exactly one common side, or equal source and target.

theorem TauCeti.GridRectangleDecomposition.hasDisjointSides_of_disjoint {n : ℕ} (x : GridState n) {a b c d : Fin n} (hab : a ≠ b) (hcd : c ≠ d) (hdisjoint : Disjoint {a, b} {c, d}) (D : GridRectangleDecomposition x (GridState.swapColumns c d (GridState.swapColumns a b x))) : D.HasDisjointSides

Two disjoint column transpositions move four columns, so no two-step rectangle decomposition of the resulting state can share a side column.

This is the entry point that puts a two-step term over such a target in the disjoint-side case of hasDisjointSides_or_hasOneCommonSide_or_eq.

theorem TauCeti.GridRectangleDecomposition.hasDisjointSides_or_hasOneCommonSide_of_ne {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hzx : z ≠ x) : D.HasDisjointSides ∨ D.HasOneCommonSide

In a nondiagonal two-step rectangle decomposition, the side pairs are disjoint or share exactly one column. This is the two-case split used by the nondiagonal juxtaposition pairing.

theorem TauCeti.GridRectangleDecomposition.hasOneCommonSide_of_mem_commonSideColumns {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) {c : Fin n} (hc : c ∈ D.commonSideColumns) (hzx : z ≠ x) : D.HasOneCommonSide

A nondiagonal decomposition whose two rectangles have a common side column has exactly one common side column.

theorem TauCeti.GridRectangleDecomposition.hasOneCommonSide_of_right_eq_left_of_ne {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hcommon : D.first.right = D.second.left) (hzx : z ≠ x) : D.HasOneCommonSide

Off the diagonal, when the terminal side of the first rectangle is the initial side of the second, this grid line is their unique common side.

theorem TauCeti.GridRectangleDecomposition.hasOneCommonSide_of_left_eq_right_of_ne {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hcommon : D.first.left = D.second.right) (hzx : z ≠ x) : D.HasOneCommonSide

Off the diagonal, when the initial side of the first rectangle is the terminal side of the second, this grid line is their unique common side.

theorem TauCeti.GridRectangleDecomposition.target_ne_source_iff {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : z ≠ x ↔ D.HasDisjointSides ∨ D.HasOneCommonSide

A two-step rectangle decomposition is nondiagonal exactly when its side pairs are disjoint or share exactly one column.

theorem TauCeti.GridRectangleDecomposition.target_ne_source_of_hasDisjointSides {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : z ≠ x

A decomposition with disjoint side pairs is necessarily nondiagonal.

theorem TauCeti.GridRectangleDecomposition.target_ne_source_of_hasOneCommonSide {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasOneCommonSide) : z ≠ x

A decomposition with one common side is necessarily nondiagonal.

theorem TauCeti.GridRectangleDecomposition.sideColumns_ne_of_hasOneCommonSide {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hone : D.HasOneCommonSide) : D.first.sideColumns ≠ D.second.sideColumns

A decomposition sharing exactly one side column does not use the same unordered pair of side columns twice: coinciding side pairs are the diagonal case.

theorem TauCeti.GridRectangleDecomposition.not_hasDisjointSides_of_hasOneCommonSide {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasOneCommonSide) : ¬D.HasDisjointSides

The disjoint-side and one-common-side cases are mutually exclusive.

theorem TauCeti.GridRectangleDecomposition.sideColumns_union_eq_of_hasOneCommonSide {n : ℕ} {x z : GridState n} (D E : GridRectangleDecomposition x z) (hD : D.HasOneCommonSide) : D.first.sideColumns ∪ D.second.sideColumns = E.first.sideColumns ∪ E.second.sideColumns

Two decompositions between the same endpoint states use the same three side columns when one of them has one common side: the other cannot have disjoint sides, which would move four columns, nor equal source and target.

theorem TauCeti.GridRectangleDecomposition.not_hasDisjointSides_iff_sameSideOverlap_or_mixedSideOverlap_of_ne {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (hzx : z ≠ x) : ¬D.HasDisjointSides ↔ D.HasSameSideOverlap ∨ D.HasMixedSideOverlap

Off the diagonal, failing to have disjoint side pairs is equivalent to having a same-side or mixed-side overlap.

@[simp]

theorem TauCeti.GridRectangleDecomposition.filter_not_hasDisjointSides_eq_self {n : ℕ} {x : GridState n} {α : Type u_1} (S : Finset α) (underlying : α → GridRectangleDecomposition x x) : {D ∈ S | ¬(underlying D).HasDisjointSides} = S

Every two-step rectangle domain in a diagonal family has nondisjoint side pairs.

theorem TauCeti.GridRectangleDecomposition.sum_filter_not_hasDisjointSides_eq_sameSide_add_mixedSide {n : ℕ} {x z : GridState n} {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (S : Finset α) (underlying : α → GridRectangleDecomposition x z) (w : α → M) (hzx : z ≠ x) : ∑ D ∈ S with ¬(underlying D).HasDisjointSides, w D = ∑ D ∈ S with (underlying D).HasSameSideOverlap, w D + ∑ D ∈ S with (underlying D).HasMixedSideOverlap, w D

For an off-diagonal family of two-step rectangle domains, the sum over nondisjoint side pairs splits into the same-side and mixed-side overlap sums.