Hexagons of a column commutation, and the commutation homotopy

Let b = finRotate n a and draw a column commutation of G as in Commutation/Pentagon.lean: the vertical grid line β with index b is replaced by a curve γ meeting it in two points. At the turn point, in square row t = C.turnRow, the curve γ crosses from the left of β to its right going upwards; at the other point, in square row t' = C.oppositeTurnRow, it crosses back. Going up from t' to t the curve γ runs to the left of β, and this bigon contains both markings of column a; going up from t to t' it runs to the right of β, and this bigon contains both markings of column b.

The commutation map Φ : GC⁻(G) → GC⁻(G') counts pentagons turning at t, and the reverse map Ψ : GC⁻(G') → GC⁻(G) counts pentagons turning at t'. The composite Ψ ∘ Φ is compared with the identity by a homotopy H : GC⁻(G) → GC⁻(G) counting hexagons: embedded disks from a state x of G to a state y of G bounded by arcs of horizontal circles, vertical circles, β and γ, with convex corners at the four points of x and y and at both intersection points of β and γ.

Convexity at the two intersection points leaves two kinds of hexagon.

• A hexagon whose terminal side runs up β to t', up γ to t and up β again (TauCeti.GridHexagonBetween). It is the oriented rectangle from x to y with terminal side b, with the bigon from t' to t cut away; its rows must contain both intersection points, t' below t.
• A hexagon whose initial side runs up β to t, up γ to t' and up β again (TauCeti.GridInitialHexagonBetween). It is the oriented rectangle from x to y with initial side b, with the bigon from t to t' cut away; its rows must contain t below t'.

Both shapes are parametrised by the column a and the square rows s, s' of the lower and upper ends of the bigon that is cut away. The interior lattice points of a hexagon are those of the rectangle, so emptiness is GridRectangleBetween.IsEmpty. The markings a hexagon carries are those of the rectangle except in the one column of the rectangle next to β: a hexagon of the first kind carries no marking of column a, since the bigon it cuts away contains them all, and one of the second kind carries no marking of column b. Its weight is the product of the variables of the O-markings it carries; unlike for pentagons both states lie in G, so no renaming of variables occurs.

Both kinds are needed, just as both kinds of pentagon are. For example, take the 5 × 5 diagram with O = (0, 3, 2, 1, 4) and X = (3, 0, 4, 2, 1), commute columns 2 and 3, and use turn row 4 with the other intersection in row 2. Counting only hexagons of the first kind, the identity state has diagonal coefficient 1 in ∂⁻ ∘ H + H ∘ ∂⁻ + 1 + Ψ ∘ Φ over 𝔽₂; counting both kinds it vanishes.

GridDiagram.hexagonMap and GridDiagram.initialHexagonMap count the empty hexagons of the two kinds carrying no X-marking, and GridDiagram.commutationHomotopy is their sum, the map H above. That ∂⁻ ∘ H + H ∘ ∂⁻ is the identity plus Ψ ∘ Φ is not proved here; GridDiagram.unblockedDifferential_commutationHomotopy_add_eq_iff writes it as an identity between matrix coefficients, and GridDiagram.unblockedDifferential_commutationHomotopy_add_eq proves it.

Main definitions

• TauCeti.GridHexagonBetween, TauCeti.GridInitialHexagonBetween: the combinatorial shapes of the two kinds of hexagon.
• TauCeti.GridHexagonBetween.coveredSquares, TauCeti.GridInitialHexagonBetween.coveredSquares: the squares of G whose marking lies inside such a hexagon.
• TauCeti.GridDiagram.hexagons, TauCeti.GridDiagram.initialHexagons: the empty hexagons carrying no X-marking.
• TauCeti.GridDiagram.hexagonWeight, TauCeti.GridDiagram.hexagonCoefficient and their initial versions: the monomial weights and the matrix coefficients.
• TauCeti.GridDiagram.hexagonMap, TauCeti.GridDiagram.initialHexagonMap: the maps GC⁻(G) → GC⁻(G) counting each kind.
• TauCeti.GridDiagram.commutationHomotopy: their sum, with matrix coefficients TauCeti.GridDiagram.commutationHexagonCoefficient.

Main results

• TauCeti.GridHexagonBetween.nonempty_iff, TauCeti.GridInitialHexagonBetween.nonempty_iff: a hexagon from x to y exists exactly when y is x with column b swapped against another column and the rows of x on the two columns enclose the bigon in the right order; Subsingleton records that it is then unique.
• TauCeti.GridDiagram.OColumns_toGridRectangle_eq_insert_of_hexagon and its initial version: the rectangle under a hexagon carries one more O-marking, that of the cut-off column.
• TauCeti.GridDiagram.XSet_inter_toGridRectangle_coveredSquares_of_disjoint_hexagon and its initial version: the rectangle under a hexagon carrying no X-marking carries exactly one X-marking, that of the cut-off column.
• TauCeti.GridDiagram.commutationHomotopy_single_apply and TauCeti.GridDiagram.commutationHomotopy_apply_apply: the matrix coefficients of the commutation homotopy.

References

The hexagons are those of the homotopy H_{βγβ} of Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.1 (arXiv:math/0610559), and of the homotopy of Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.1. The orientation convention matches the rectangles of TauCeti.GridRectangleBetween: the source state occupies the lower-left and upper-right corners.

structure TauCeti.GridHexagonBetween {n : ℕ} (a s s' : Fin n) (x y : GridState n) extends TauCeti.GridRectangleBetween x y : Type

The combinatorial shape of a hexagon whose terminal side turns at both intersection points, for columns a and finRotate n a, cutting away the bigon from square row s up to square row s', from a grid state x to a grid state y.

It is recorded by the oriented rectangle from x to y with the same corners, whose terminal side is the grid line finRotate n a; the rows that side spans must contain the lower intersection row s and, above it, the upper intersection row s'. The shape records only the corners and the two turn rows. Its coveredSquares describe the squares of the hexagon when GridDiagram.ColumnCommutationData places the column-a markings in the bigon; the crossing change counts the same shapes for interleaving columns, with crossingCoveredSquares instead.

• left : Fin n
• right : Fin n
• left_ne_right : self.left ≠ self.right
• map_left : y.toPerm self.left = x.toPerm self.right
• map_right : y.toPerm self.right = x.toPerm self.left
• map_of_ne (c : Fin n) : c ≠ self.left → c ≠ self.right → y.toPerm c = x.toPerm c
• right_eq : self.right = (finRotate n) a

  The terminal side lies on the grid line between column a and the next column.

• lower_mem : s ∈ Grid.cIco (x.toPerm self.left) (x.toPerm self.right)

  The lower intersection point lies on the terminal side.

• upper_mem : s' ∈ Grid.cIoo s (x.toPerm self.right)

  The upper intersection point lies on the terminal side, above the lower one.

theorem TauCeti.GridHexagonBetween.left_ne {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridHexagonBetween a s s' x y) : P.left ≠ (finRotate n) a

The initial side of a hexagon is not the line replaced by γ.

theorem TauCeti.GridHexagonBetween.insert_cIco_subset_cIco_bottom_top {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridHexagonBetween a s s' x y) : insert s' (Grid.cIco s s') ⊆ Grid.cIco P.bottom P.top

The rows of the bigon cut away by a hexagon, from its lower intersection row up to and including its upper one, lie among the rows of the hexagon.

theorem TauCeti.GridHexagonBetween.left_injective {n : ℕ} {a s s' : Fin n} {x y : GridState n} : Function.Injective fun (P : GridHexagonBetween a s s' x y) => P.left

A hexagon is determined by its initial side.

instance TauCeti.GridHexagonBetween.instSubsingleton {n : ℕ} {a s s' : Fin n} {x y : GridState n} : Subsingleton (GridHexagonBetween a s s' x y)

There is at most one hexagon between two grid states: its initial side is the unique column other than finRotate n a at which the two states differ.

@[instance_reducible]

noncomputable instance TauCeti.GridHexagonBetween.instFintype {n : ℕ} {a s s' : Fin n} {x y : GridState n} : Fintype (GridHexagonBetween a s s' x y)

There are finitely many hexagons between two grid states.

theorem TauCeti.GridHexagonBetween.target_eq_swapColumns {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridHexagonBetween a s s' x y) : y = GridState.swapColumns P.left ((finRotate n) a) x

The target of a hexagon is its source with the initial side swapped against the line replaced by γ.

def TauCeti.GridHexagonBetween.ofSwapColumns {n : ℕ} {a s s' : Fin n} (x : GridState n) (j : Fin n) (hj : j ≠ (finRotate n) a) (hs : s ∈ Grid.cIco (x.toPerm j) (x.toPerm ((finRotate n) a))) (hs' : s' ∈ Grid.cIoo s (x.toPerm ((finRotate n) a))) : GridHexagonBetween a s s' x (GridState.swapColumns j ((finRotate n) a) x)

The hexagon with initial side j from x to x.swapColumns j (finRotate n a), when the rows of x on the two sides enclose the bigon from s up to s'.

@[simp]

theorem TauCeti.GridHexagonBetween.ofSwapColumns_left {n : ℕ} {a s s' : Fin n} (x : GridState n) (j : Fin n) (hj : j ≠ (finRotate n) a) (hs : s ∈ Grid.cIco (x.toPerm j) (x.toPerm ((finRotate n) a))) (hs' : s' ∈ Grid.cIoo s (x.toPerm ((finRotate n) a))) : (ofSwapColumns x j hj hs hs').left = j

The initial side of the hexagon built from a column swap.

theorem TauCeti.GridHexagonBetween.nonempty_iff {n : ℕ} {a s s' : Fin n} {x y : GridState n} : Nonempty (GridHexagonBetween a s s' x y) ↔ ∃ (j : Fin n), j ≠ (finRotate n) a ∧ s ∈ Grid.cIco (x.toPerm j) (x.toPerm ((finRotate n) a)) ∧ s' ∈ Grid.cIoo s (x.toPerm ((finRotate n) a)) ∧ y = GridState.swapColumns j ((finRotate n) a) x

A hexagon from x to y exists exactly when y is x with some column j swapped against the line replaced by γ, and the rows of x on j and on that line enclose the bigon from s up to s'.

noncomputable def TauCeti.GridHexagonBetween.coveredSquares {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridHexagonBetween a s s' x y) : Finset (Fin n × Fin n)

The squares of the original diagram whose marking lies inside a hexagon: the squares of the underlying rectangle outside column a.

The hexagon agrees with the rectangle away from the bigon it cuts away, which lies in column a between the rows s and s'. When the column-a markings lie in that bigon, as GridDiagram.ColumnCommutationData guarantees, the hexagon carries none of them, so only the marked squares matter and these are the correct squares for them.

theorem TauCeti.GridHexagonBetween.mem_coveredSquares {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridHexagonBetween a s s' x y) (p : Fin n × Fin n) : p ∈ P.coveredSquares ↔ p.1 ≠ a ∧ p ∈ P.toGridRectangle.coveredSquares

A hexagon covers the squares of its underlying rectangle outside column a.

theorem TauCeti.GridHexagonBetween.mem_toGridRectangle_coveredSquares {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridHexagonBetween a s s' x y) (p : Fin n × Fin n) : p ∈ P.toGridRectangle.coveredSquares ↔ p.1 ∈ Grid.cIco P.left ((finRotate n) a) ∧ p.2 ∈ Grid.cIco P.bottom P.top

The underlying rectangle of a hexagon covers the squares from its left column up to column finRotate n a, in its rows.

theorem TauCeti.GridHexagonBetween.mk_mem_toGridRectangle_coveredSquares_of_mem {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridHexagonBetween a s s' x y) {r : Fin n} (hr : r ∈ insert s' (Grid.cIco s s')) : (a, r) ∈ P.toGridRectangle.coveredSquares

The rectangle underlying a hexagon covers every square of column a in the rows of the bigon it cuts away.

theorem TauCeti.GridHexagonBetween.disjoint_coveredSquares_XSet_iff {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridHexagonBetween a s s' x y) (G : GridDiagram n) : Disjoint P.coveredSquares G.XSet ↔ ∀ (c : Fin n), c ≠ a → c ∈ Grid.cIco P.left ((finRotate n) a) → G.X.toPerm c ∉ Grid.cIco P.bottom P.top

A hexagon carries no X-marking exactly when its underlying rectangle carries none outside column a.

def TauCeti.GridHexagonBetween.ofToGridRectangleEq {n : ℕ} {a s s' : Fin n} {x y u v : GridState n} (r : GridRectangleBetween u v) (P : GridHexagonBetween a s s' x y) (h : r.toGridRectangle = P.toGridRectangle) : GridHexagonBetween a s s' u v

Transfer a hexagon to new endpoint states when its underlying toroidal rectangle is unchanged. The turn side and both intersection rows are preserved.

@[simp]

theorem TauCeti.GridHexagonBetween.ofToGridRectangleEq_toGridRectangleBetween {n : ℕ} {a s s' : Fin n} {x y u v : GridState n} (r : GridRectangleBetween u v) (P : GridHexagonBetween a s s' x y) (h : r.toGridRectangle = P.toGridRectangle) : (ofToGridRectangleEq r P h).toGridRectangleBetween = r

The rectangle underlying the transferred hexagon is the supplied rectangle.

theorem TauCeti.GridHexagonBetween.coveredSquares_eq_of_toGridRectangle_eq {n : ℕ} {a s s' : Fin n} {x y u v : GridState n} (P : GridHexagonBetween a s s' x y) (Q : GridHexagonBetween a s s' u v) (h : P.toGridRectangle = Q.toGridRectangle) : P.coveredSquares = Q.coveredSquares

The squares covered by a hexagon depend only on its underlying toroidal rectangle.

structure TauCeti.GridInitialHexagonBetween {n : ℕ} (a s s' : Fin n) (x y : GridState n) extends TauCeti.GridRectangleBetween x y : Type

The combinatorial shape of a hexagon whose initial side turns at both intersection points, for columns a and finRotate n a, cutting away the bigon from square row s up to square row s', from a grid state x to a grid state y.

It is recorded by the oriented rectangle from x to y with the same corners, whose initial side is the grid line finRotate n a; the rows that side spans must contain the lower intersection row s and, above it, the upper intersection row s'. The shape records only the corners and the two turn rows. Its coveredSquares describe the squares of the hexagon when GridDiagram.ColumnCommutationData places the column-finRotate n a markings in the bigon; the crossing change counts the same shapes for interleaving columns, with crossingCoveredSquares instead.

• left : Fin n
• right : Fin n
• left_ne_right : self.left ≠ self.right
• map_left : y.toPerm self.left = x.toPerm self.right
• map_right : y.toPerm self.right = x.toPerm self.left
• map_of_ne (c : Fin n) : c ≠ self.left → c ≠ self.right → y.toPerm c = x.toPerm c
• left_eq : self.left = (finRotate n) a

  The initial side lies on the grid line between column a and the next column.

• lower_mem : s ∈ Grid.cIco (x.toPerm self.left) (x.toPerm self.right)

  The lower intersection point lies on the initial side.

• upper_mem : s' ∈ Grid.cIoo s (x.toPerm self.right)

  The upper intersection point lies on the initial side, above the lower one.

theorem TauCeti.GridInitialHexagonBetween.right_ne {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridInitialHexagonBetween a s s' x y) : P.right ≠ (finRotate n) a

The terminal side of a hexagon turning on its initial side is not the line replaced by γ.

theorem TauCeti.GridInitialHexagonBetween.insert_cIco_subset_cIco_bottom_top {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridInitialHexagonBetween a s s' x y) : insert s' (Grid.cIco s s') ⊆ Grid.cIco P.bottom P.top

The rows of the bigon cut away by a hexagon turning on its initial side lie among its rows.

theorem TauCeti.GridInitialHexagonBetween.toGridRectangleBetween_injective {n : ℕ} {a s s' : Fin n} {x y : GridState n} : Function.Injective toGridRectangleBetween

A hexagon turning on its initial side is determined by its underlying rectangle.

instance TauCeti.GridInitialHexagonBetween.instSubsingleton {n : ℕ} {a s s' : Fin n} {x y : GridState n} : Subsingleton (GridInitialHexagonBetween a s s' x y)

There is at most one hexagon turning on its initial side between two grid states: its initial side is the replaced line, which determines the underlying rectangle.

@[instance_reducible]

noncomputable instance TauCeti.GridInitialHexagonBetween.instFintype {n : ℕ} {a s s' : Fin n} {x y : GridState n} : Fintype (GridInitialHexagonBetween a s s' x y)

There are finitely many hexagons turning on their initial side between two grid states.

theorem TauCeti.GridInitialHexagonBetween.target_eq_swapColumns {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridInitialHexagonBetween a s s' x y) : y = GridState.swapColumns ((finRotate n) a) P.right x

The target of a hexagon turning on its initial side is its source with the line replaced by γ swapped against the terminal side.

def TauCeti.GridInitialHexagonBetween.ofSwapColumns {n : ℕ} {a s s' : Fin n} (x : GridState n) (j : Fin n) (hj : j ≠ (finRotate n) a) (hs : s ∈ Grid.cIco (x.toPerm ((finRotate n) a)) (x.toPerm j)) (hs' : s' ∈ Grid.cIoo s (x.toPerm j)) : GridInitialHexagonBetween a s s' x (GridState.swapColumns ((finRotate n) a) j x)

The hexagon turning on its initial side from x to x.swapColumns (finRotate n a) j, when the rows of x on the two sides enclose the bigon from s up to s'.

@[simp]

theorem TauCeti.GridInitialHexagonBetween.ofSwapColumns_right {n : ℕ} {a s s' : Fin n} (x : GridState n) (j : Fin n) (hj : j ≠ (finRotate n) a) (hs : s ∈ Grid.cIco (x.toPerm ((finRotate n) a)) (x.toPerm j)) (hs' : s' ∈ Grid.cIoo s (x.toPerm j)) : (ofSwapColumns x j hj hs hs').right = j

The terminal side of the hexagon built from a column swap.

theorem TauCeti.GridInitialHexagonBetween.nonempty_iff {n : ℕ} {a s s' : Fin n} {x y : GridState n} : Nonempty (GridInitialHexagonBetween a s s' x y) ↔ ∃ (j : Fin n), j ≠ (finRotate n) a ∧ s ∈ Grid.cIco (x.toPerm ((finRotate n) a)) (x.toPerm j) ∧ s' ∈ Grid.cIoo s (x.toPerm j) ∧ y = GridState.swapColumns ((finRotate n) a) j x

A hexagon turning on its initial side from x to y exists exactly when y is x with the line replaced by γ swapped against some other column j, and the rows of x on that line and on j enclose the bigon from s up to s'.

noncomputable def TauCeti.GridInitialHexagonBetween.coveredSquares {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridInitialHexagonBetween a s s' x y) : Finset (Fin n × Fin n)

The squares of the original diagram whose marking lies inside a hexagon turning on its initial side: the squares of the underlying rectangle outside column finRotate n a.

As for GridHexagonBetween.coveredSquares, the bigon cut away lies in column finRotate n a between the rows s and s', and when the markings of that column lie in it the hexagon carries none of them.

theorem TauCeti.GridInitialHexagonBetween.mem_coveredSquares {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridInitialHexagonBetween a s s' x y) (p : Fin n × Fin n) : p ∈ P.coveredSquares ↔ p.1 ≠ (finRotate n) a ∧ p ∈ P.toGridRectangle.coveredSquares

A hexagon turning on its initial side covers the squares of its underlying rectangle outside column finRotate n a.

theorem TauCeti.GridInitialHexagonBetween.mem_toGridRectangle_coveredSquares {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridInitialHexagonBetween a s s' x y) (p : Fin n × Fin n) : p ∈ P.toGridRectangle.coveredSquares ↔ p.1 ∈ Grid.cIco ((finRotate n) a) P.right ∧ p.2 ∈ Grid.cIco P.bottom P.top

The underlying rectangle of a hexagon turning on its initial side covers the squares from column finRotate n a up to its right column, in its rows.

theorem TauCeti.GridInitialHexagonBetween.mk_mem_toGridRectangle_coveredSquares_of_mem {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridInitialHexagonBetween a s s' x y) {r : Fin n} (hr : r ∈ insert s' (Grid.cIco s s')) : ((finRotate n) a, r) ∈ P.toGridRectangle.coveredSquares

The rectangle underlying a hexagon turning on its initial side covers every square of the column after a in the rows of the bigon it cuts away.

theorem TauCeti.GridInitialHexagonBetween.disjoint_coveredSquares_XSet_iff {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridInitialHexagonBetween a s s' x y) (G : GridDiagram n) : Disjoint P.coveredSquares G.XSet ↔ ∀ (c : Fin n), c ≠ (finRotate n) a → c ∈ Grid.cIco ((finRotate n) a) P.right → G.X.toPerm c ∉ Grid.cIco P.bottom P.top

A hexagon turning on its initial side carries no X-marking exactly when its underlying rectangle carries none outside column finRotate n a.

def TauCeti.GridInitialHexagonBetween.ofToGridRectangleEq {n : ℕ} {a s s' : Fin n} {x y u v : GridState n} (r : GridRectangleBetween u v) (P : GridInitialHexagonBetween a s s' x y) (h : r.toGridRectangle = P.toGridRectangle) : GridInitialHexagonBetween a s s' u v

Transfer a hexagon to new endpoint states when its underlying toroidal rectangle is unchanged. The turn side and both intersection rows are preserved.

@[simp]

theorem TauCeti.GridInitialHexagonBetween.ofToGridRectangleEq_toGridRectangleBetween {n : ℕ} {a s s' : Fin n} {x y u v : GridState n} (r : GridRectangleBetween u v) (P : GridInitialHexagonBetween a s s' x y) (h : r.toGridRectangle = P.toGridRectangle) : (ofToGridRectangleEq r P h).toGridRectangleBetween = r

The rectangle underlying the transferred hexagon is the supplied rectangle.

theorem TauCeti.GridInitialHexagonBetween.coveredSquares_eq_of_toGridRectangle_eq {n : ℕ} {a s s' : Fin n} {x y u v : GridState n} (P : GridInitialHexagonBetween a s s' x y) (Q : GridInitialHexagonBetween a s s' u v) (h : P.toGridRectangle = Q.toGridRectangle) : P.coveredSquares = Q.coveredSquares

The squares covered by a hexagon depend only on its underlying toroidal rectangle.

The hexagons counted by the commutation homotopy

noncomputable def TauCeti.GridDiagram.hexagons {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x y : GridState n) : Finset (GridHexagonBetween C.column C.oppositeTurnRow C.turnRow x y)

The hexagons turning on their terminal side from x to y counted by a validated column commutation: the empty ones carrying no X-marking, cutting away the bigon from the opposite turn row up to the turn row, which contains the markings of C.column.

@[simp]

theorem TauCeti.GridDiagram.mem_hexagons {n : ℕ} (G : GridDiagram n) {C : G.ColumnCommutationData} {x y : GridState n} (P : GridHexagonBetween C.column C.oppositeTurnRow C.turnRow x y) : P ∈ G.hexagons C x y ↔ P.IsEmpty ∧ Disjoint P.coveredSquares G.XSet

Membership in the counted hexagons is emptiness together with X-avoidance.

noncomputable def TauCeti.GridDiagram.initialHexagons {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x y : GridState n) : Finset (GridInitialHexagonBetween C.column C.turnRow C.oppositeTurnRow x y)

The hexagons turning on their initial side from x to y counted by a validated column commutation: the empty ones carrying no X-marking, cutting away the bigon from the turn row up to the opposite turn row, which contains the markings of the column after C.column.

@[simp]

theorem TauCeti.GridDiagram.mem_initialHexagons {n : ℕ} (G : GridDiagram n) {C : G.ColumnCommutationData} {x y : GridState n} (P : GridInitialHexagonBetween C.column C.turnRow C.oppositeTurnRow x y) : P ∈ G.initialHexagons C x y ↔ P.IsEmpty ∧ Disjoint P.coveredSquares G.XSet

Membership in the counted hexagons turning on their initial side is emptiness together with X-avoidance.

The markings of the cut-off column

theorem TauCeti.GridDiagram.OColumns_toGridRectangle_eq_insert_of_hexagon {n : ℕ} (G : GridDiagram n) {C : G.ColumnCommutationData} {x y : GridState n} (P : GridHexagonBetween C.column C.oppositeTurnRow C.turnRow x y) : G.OColumns P.toGridRectangle = insert C.column (G.OColumnsOfSquares P.coveredSquares)

The rectangle underlying a hexagon carries the O-markings of the hexagon together with the O-marking of C.column, which the hexagon cuts away.

theorem TauCeti.GridDiagram.OColumns_toGridRectangle_eq_insert_of_initialHexagon {n : ℕ} (G : GridDiagram n) {C : G.ColumnCommutationData} {x y : GridState n} (P : GridInitialHexagonBetween C.column C.turnRow C.oppositeTurnRow x y) : G.OColumns P.toGridRectangle = insert ((finRotate n) C.column) (G.OColumnsOfSquares P.coveredSquares)

The rectangle underlying a hexagon turning on its initial side carries the O-markings of the hexagon together with the O-marking of the column after C.column, which the hexagon cuts away.

theorem TauCeti.GridDiagram.XSet_inter_toGridRectangle_coveredSquares_of_disjoint_hexagon {n : ℕ} (G : GridDiagram n) {C : G.ColumnCommutationData} {x y : GridState n} {P : GridHexagonBetween C.column C.oppositeTurnRow C.turnRow x y} (hP : Disjoint P.coveredSquares G.XSet) : G.XSet ∩ P.toGridRectangle.coveredSquares = {(C.column, G.X.toPerm C.column)}

The rectangle underlying a hexagon carrying no X-marking carries exactly one X-marking, that of C.column.

theorem TauCeti.GridDiagram.XSet_inter_toGridRectangle_coveredSquares_of_disjoint_initialHexagon {n : ℕ} (G : GridDiagram n) {C : G.ColumnCommutationData} {x y : GridState n} {P : GridInitialHexagonBetween C.column C.turnRow C.oppositeTurnRow x y} (hP : Disjoint P.coveredSquares G.XSet) : G.XSet ∩ P.toGridRectangle.coveredSquares = {((finRotate n) C.column, G.X.toPerm ((finRotate n) C.column))}

The rectangle underlying a hexagon turning on its initial side and carrying no X-marking carries exactly one X-marking, that of the column after C.column.

The hexagon maps

noncomputable def TauCeti.GridDiagram.hexagonWeight {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {a s s' : Fin n} {x y : GridState n} (P : GridHexagonBetween a s s' x y) : MvPolynomial (Fin n) R

The weight of a hexagon: the product of the variables of the O-markings it carries.

theorem TauCeti.GridDiagram.hexagonWeight_eq_OMonomialOfSquares {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {a s s' : Fin n} {x y : GridState n} (P : GridHexagonBetween a s s' x y) : G.hexagonWeight R P = G.OMonomialOfSquares R P.coveredSquares

The weight of a hexagon is the monomial of the squares it covers.

theorem TauCeti.GridDiagram.hexagonWeight_eq_monomial {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {a s s' : Fin n} {x y : GridState n} (P : GridHexagonBetween a s s' x y) : G.hexagonWeight R P = (MvPolynomial.monomial (∑ c ∈ G.OColumnsOfSquares P.coveredSquares, Finsupp.single c 1)) 1

The weight of a hexagon is the squarefree monomial of the O-markings it carries.

theorem TauCeti.GridDiagram.hexagonWeight_eq_prod_coveredSquares {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {a s s' : Fin n} {x y : GridState n} (P : GridHexagonBetween a s s' x y) : G.hexagonWeight R P = ∏ p ∈ P.coveredSquares, if p ∈ G.OSet then MvPolynomial.X p.1 else 1

The weight of a hexagon is the product, over the squares it covers, of the variable of the square's column at the O-marked squares and of 1 elsewhere.

theorem TauCeti.GridDiagram.X_mul_hexagonWeight {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {C : G.ColumnCommutationData} {x y : GridState n} (P : GridHexagonBetween C.column C.oppositeTurnRow C.turnRow x y) : MvPolynomial.X C.column * G.hexagonWeight R P = G.OMonomial R P.toGridRectangle

The weight of a hexagon of a validated column commutation times the variable of C.column is the weight of its underlying rectangle.

noncomputable def TauCeti.GridDiagram.initialHexagonWeight {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {a s s' : Fin n} {x y : GridState n} (P : GridInitialHexagonBetween a s s' x y) : MvPolynomial (Fin n) R

The weight of a hexagon turning on its initial side: the product of the variables of the O-markings it carries.

theorem TauCeti.GridDiagram.initialHexagonWeight_eq_OMonomialOfSquares {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {a s s' : Fin n} {x y : GridState n} (P : GridInitialHexagonBetween a s s' x y) : G.initialHexagonWeight R P = G.OMonomialOfSquares R P.coveredSquares

The weight of a hexagon turning on its initial side is the monomial of the squares it covers.

theorem TauCeti.GridDiagram.initialHexagonWeight_eq_monomial {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {a s s' : Fin n} {x y : GridState n} (P : GridInitialHexagonBetween a s s' x y) : G.initialHexagonWeight R P = (MvPolynomial.monomial (∑ c ∈ G.OColumnsOfSquares P.coveredSquares, Finsupp.single c 1)) 1

The weight of a hexagon turning on its initial side is the squarefree monomial of the O-markings it carries.

theorem TauCeti.GridDiagram.initialHexagonWeight_eq_prod_coveredSquares {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {a s s' : Fin n} {x y : GridState n} (P : GridInitialHexagonBetween a s s' x y) : G.initialHexagonWeight R P = ∏ p ∈ P.coveredSquares, if p ∈ G.OSet then MvPolynomial.X p.1 else 1

The weight of a hexagon turning on its initial side is the product, over the squares it covers, of the variable of the square's column at the O-marked squares and of 1 elsewhere.

theorem TauCeti.GridDiagram.X_mul_initialHexagonWeight {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {C : G.ColumnCommutationData} {x y : GridState n} (P : GridInitialHexagonBetween C.column C.turnRow C.oppositeTurnRow x y) : MvPolynomial.X ((finRotate n) C.column) * G.initialHexagonWeight R P = G.OMonomial R P.toGridRectangle

The weight of a hexagon turning on its initial side times the variable of the column after C.column is the weight of its underlying rectangle.

noncomputable def TauCeti.GridDiagram.hexagonCoefficient {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (x y : GridState n) : MvPolynomial (Fin n) R

The matrix coefficient from x to y of the map counting hexagons turning on their terminal side: the sum of the weights of the counted ones.

theorem TauCeti.GridDiagram.hexagonCoefficient_def {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (x y : GridState n) : G.hexagonCoefficient R C x y = ∑ P ∈ G.hexagons C x y, G.hexagonWeight R P

The matrix coefficient of the hexagon map is the sum of the weights of its counted hexagons.

noncomputable def TauCeti.GridDiagram.initialHexagonCoefficient {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (x y : GridState n) : MvPolynomial (Fin n) R

The matrix coefficient from x to y of the map counting hexagons turning on their initial side: the sum of the weights of the counted ones.

theorem TauCeti.GridDiagram.initialHexagonCoefficient_def {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (x y : GridState n) : G.initialHexagonCoefficient R C x y = ∑ P ∈ G.initialHexagons C x y, G.initialHexagonWeight R P

The matrix coefficient of the initial-side hexagon map is the sum of the weights of its counted hexagons.

noncomputable def TauCeti.GridDiagram.hexagonMap {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) : GridChainMinus R n →ₗ[MvPolynomial (Fin n) R] GridChainMinus R n

The map GC⁻(G) → GC⁻(G) of the validated column commutation C counting the hexagons that turn on their terminal side, linear over the polynomial ring: a generator x goes to the sum over the counted hexagons from x of their weights times their targets.

theorem TauCeti.GridDiagram.hexagonMap_single_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (x y : GridState n) : ((G.hexagonMap R C) (Finsupp.single x 1)) y = G.hexagonCoefficient R C x y

The matrix coefficients of the hexagon map.

@[simp]

theorem TauCeti.GridDiagram.hexagonMap_apply_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (c : GridChainMinus R n) (y : GridState n) : ((G.hexagonMap R C) c) y = Finsupp.sum c fun (x : GridState n) (p : MvPolynomial (Fin n) R) => p * G.hexagonCoefficient R C x y

The coefficient formula for the hexagon map on an arbitrary chain.

noncomputable def TauCeti.GridDiagram.initialHexagonMap {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) : GridChainMinus R n →ₗ[MvPolynomial (Fin n) R] GridChainMinus R n

The map GC⁻(G) → GC⁻(G) of the validated column commutation C counting the hexagons that turn on their initial side, linear over the polynomial ring.

theorem TauCeti.GridDiagram.initialHexagonMap_single_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (x y : GridState n) : ((G.initialHexagonMap R C) (Finsupp.single x 1)) y = G.initialHexagonCoefficient R C x y

The matrix coefficients of the initial-side hexagon map.

@[simp]

theorem TauCeti.GridDiagram.initialHexagonMap_apply_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (c : GridChainMinus R n) (y : GridState n) : ((G.initialHexagonMap R C) c) y = Finsupp.sum c fun (x : GridState n) (p : MvPolynomial (Fin n) R) => p * G.initialHexagonCoefficient R C x y

The coefficient formula for the initial-side hexagon map on an arbitrary chain.

noncomputable def TauCeti.GridDiagram.commutationHomotopy {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) : GridChainMinus R n →ₗ[MvPolynomial (Fin n) R] GridChainMinus R n

The commutation homotopy H : GC⁻(G) → GC⁻(G) of the validated column commutation C: it counts the empty hexagons carrying no X-marking with corners at both intersection points, both those turning on their terminal side (GridDiagram.hexagonMap) and those turning on their initial side (GridDiagram.initialHexagonMap). It is the map that compares the composite of the commutation map with its reverse to the identity.

theorem TauCeti.GridDiagram.commutationHomotopy_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (c : GridChainMinus R n) : (G.commutationHomotopy R C) c = (G.hexagonMap R C) c + (G.initialHexagonMap R C) c

The commutation homotopy is the sum of the two hexagon maps.

noncomputable def TauCeti.GridDiagram.commutationHexagonCoefficient {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (x y : GridState n) : MvPolynomial (Fin n) R

The matrix coefficient of the commutation homotopy from x to y, counting the hexagons turning on either side.

theorem TauCeti.GridDiagram.commutationHexagonCoefficient_def {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (x y : GridState n) : G.commutationHexagonCoefficient R C x y = G.hexagonCoefficient R C x y + G.initialHexagonCoefficient R C x y

The commutation hexagon coefficient is the sum of the two turn-side coefficients.

theorem TauCeti.GridDiagram.commutationHomotopy_single_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (x y : GridState n) : ((G.commutationHomotopy R C) (Finsupp.single x 1)) y = G.commutationHexagonCoefficient R C x y

The matrix coefficients of the commutation homotopy are the commutation hexagon coefficients.

@[simp]

theorem TauCeti.GridDiagram.commutationHomotopy_apply_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (c : GridChainMinus R n) (y : GridState n) : ((G.commutationHomotopy R C) c) y = Finsupp.sum c fun (x : GridState n) (p : MvPolynomial (Fin n) R) => p * (G.hexagonCoefficient R C x y + G.initialHexagonCoefficient R C x y)

The coefficient formula for the commutation homotopy on an arbitrary chain: its matrix coefficients are the sums of those of the two hexagon maps.