Link components under grid commutation

An elementary grid commutation exchanges two adjacent, non-interleaving rows or columns. It does not change the represented link, and the first combinatorial shadow of this fact is that it preserves the component traversal. A row commutation leaves the component permutation unchanged. A column commutation conjugates it by the transposition of the exchanged columns. Consequently both moves preserve the multiset of component sizes, the number of components, and whether the diagram represents a knot.

These results deliberately concern only component combinatorics. The later invariance proof for grid homology attaches pentagon-counting chain maps to the same elementary commutations.

Main results

• TauCeti.GridDiagram.IsRowCommutation.componentPerm_eq: row commutation leaves the component permutation unchanged.
• TauCeti.GridDiagram.IsColumnCommutation.componentPerm_eq_conj: column commutation conjugates the component permutation.
• TauCeti.GridDiagram.IsCommutation.componentCycleType_eq: every commutation preserves the multiset of component sizes.
• TauCeti.GridDiagram.IsCommutation.componentCount_eq and TauCeti.GridDiagram.IsCommutation.isKnot_iff: every commutation preserves component count and the knot predicate.

References

This advances TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.5, "Invariance over 𝔽₂. Grid moves = commutation + (de)stabilization", by establishing that the already-defined elementary commutations preserve the link-component data from Lane G.1. The grid-move convention follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

theorem TauCeti.GridDiagram.IsRowCommutation.componentPerm_eq {n : ℕ} {G G' : GridDiagram n} (h : G.IsRowCommutation G') : G'.componentPerm = G.componentPerm

A row commutation leaves the component traversal permutation unchanged.

theorem TauCeti.GridDiagram.IsColumnCommutation.componentPerm_eq_conj {n : ℕ} {G G' : GridDiagram n} (h : G.IsColumnCommutation G') : ∃ (a : Fin n), G'.componentPerm = Equiv.swap a ((finRotate n) a) * G.componentPerm * (Equiv.swap a ((finRotate n) a))⁻¹

A column commutation conjugates the component traversal permutation by the transposition of the exchanged columns.

theorem TauCeti.GridDiagram.IsRowCommutation.componentCycleType_eq {n : ℕ} {G G' : GridDiagram n} (h : G.IsRowCommutation G') : G'.componentCycleType = G.componentCycleType

A row commutation preserves the multiset of component sizes.

theorem TauCeti.GridDiagram.IsColumnCommutation.componentCycleType_eq {n : ℕ} {G G' : GridDiagram n} (h : G.IsColumnCommutation G') : G'.componentCycleType = G.componentCycleType

A column commutation preserves the multiset of component sizes.

theorem TauCeti.GridDiagram.IsCommutation.componentCycleType_eq {n : ℕ} {G G' : GridDiagram n} (h : G.IsCommutation G') : G'.componentCycleType = G.componentCycleType

Every elementary commutation preserves the multiset of component sizes.

theorem TauCeti.GridDiagram.IsCommutation.componentCount_eq {n : ℕ} {G G' : GridDiagram n} (h : G.IsCommutation G') : G'.componentCount = G.componentCount

Every elementary commutation preserves the number of represented link components.

theorem TauCeti.GridDiagram.IsRowCommutation.componentCount_eq {n : ℕ} {G G' : GridDiagram n} (h : G.IsRowCommutation G') : G'.componentCount = G.componentCount

A row commutation preserves the number of represented link components.

theorem TauCeti.GridDiagram.IsColumnCommutation.componentCount_eq {n : ℕ} {G G' : GridDiagram n} (h : G.IsColumnCommutation G') : G'.componentCount = G.componentCount

A column commutation preserves the number of represented link components.

theorem TauCeti.GridDiagram.IsCommutation.isKnot_iff {n : ℕ} {G G' : GridDiagram n} (h : G.IsCommutation G') : G'.IsKnot ↔ G.IsKnot

Every elementary commutation preserves whether a grid diagram represents a knot.

theorem TauCeti.GridDiagram.IsRowCommutation.isKnot_iff {n : ℕ} {G G' : GridDiagram n} (h : G.IsRowCommutation G') : G'.IsKnot ↔ G.IsKnot

A row commutation preserves whether a grid diagram represents a knot.

theorem TauCeti.GridDiagram.IsColumnCommutation.isKnot_iff {n : ℕ} {G G' : GridDiagram n} (h : G.IsColumnCommutation G') : G'.IsKnot ↔ G.IsKnot

A column commutation preserves whether a grid diagram represents a knot.