Pentagons turning on their initial side, and the commutation map

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 at the turn point, in square row s, where γ crosses from the left of β to its right going upwards, and at one other point. The pentagons of TauCeti.GridPentagonBetween lie to the left of β ∪ γ: their terminal side runs up γ to the turn point and then up β. The commutation map Φ of Ozsváth--Stipsicz--Szabó also counts the empty pentagons lying to the right of β ∪ γ, whose initial side runs up β to the turn point and then up γ.

Such a pentagon from a state x of G to a state y of G' starts at the point of x on β, runs right along a horizontal circle to a point of y, up a vertical line to a point of x, left along a horizontal circle to the point of y on γ, down γ to an intersection point of β and γ, and down β back to the start. Convexity of the corner at the intersection point forces it to be the same turn point as for the terminal-side pentagons. Its corners are those of the oriented rectangle from x to y whose initial side is the line b, and the turn row must lie among the rows that side spans (TauCeti.GridInitialPentagonBetween).

Away from columns a and b such a pentagon carries the markings of the underlying rectangle. The column-a markings lie in the bigon below the turn point, between γ and β; the pentagon contains such a marking exactly when it lies above the turn row, where its initial side runs along γ. The column-b markings lie in the bigon above the turn point, between β and γ; the pentagon contains such a marking exactly when it lies below the turn row, where its initial side runs along β. These are the same two arcs as for a terminal-side pentagon (TauCeti.GridInitialPentagonBetween.coveredSquares).

Both kinds of pentagon are needed. A rectangle followed by a terminal-side pentagon can make a corner of angle 3π/2 at the turn point. Cutting that domain along the other curve through the turn point decomposes it again, now as a rectangle followed by an initial-side pentagon. Without the initial-side pentagons the pentagon-counting map is not a chain map. For example, take the 4 × 4 diagram with O = (0, 2, 1, 3) and X = (2, 3, 0, 1), commute columns 0 and 1, and use turn row 2 with the other intersection in row 0. The identity state then has the diagonal coefficient V₁ in Φ ∘ ∂⁻ - ∂⁻' ∘ Φ when only terminal-side pentagons are counted. Counting initial-side pentagons too gives a second rectangle--pentagon term with the same weight, so the coefficient vanishes in characteristic two.

Main definitions

• TauCeti.GridInitialPentagonBetween: the combinatorial shape of a pentagon turning on its initial side.
• TauCeti.GridInitialPentagonBetween.coveredSquares: the squares of G whose marking lies inside such a pentagon.
• TauCeti.GridDiagram.initialPentagons: the empty ones carrying no X-marking.
• TauCeti.GridDiagram.initialPentagonWeight, TauCeti.GridDiagram.initialPentagonCoefficient: their monomial weights and the resulting matrix coefficients.
• TauCeti.GridDiagram.initialPentagonMap: the map counting them.
• TauCeti.GridDiagram.commutationMap: the commutation map Φ : GC⁻(G) → GC⁻(G.swapColumns a b), counting pentagons of both kinds, with matrix coefficients TauCeti.GridDiagram.commutationPentagonCoefficient.

Main results

• TauCeti.GridInitialPentagonBetween.nonempty_iff: such a pentagon from x to y exists exactly when y is x with column b swapped against another column j and the turn row lies between the rows of x on b and on j; Subsingleton records that it is then unique.
• TauCeti.GridInitialPentagonBetween.mem_coveredSquares_iff_of_ne: away from columns a and b the covered squares are those of the underlying rectangle; TauCeti.GridInitialPentagonBetween.mk_mem_coveredSquares_left_column and TauCeti.GridInitialPentagonBetween.mk_mem_coveredSquares_right_column give them in those two columns; TauCeti.GridInitialPentagonBetween.mk_mem_toGridRectangle_coveredSquares_right_column and TauCeti.GridInitialPentagonBetween.mk_notMem_toGridRectangle_coveredSquares_left_column give those of the underlying rectangle.
• TauCeti.GridInitialPentagonBetween.disjoint_coveredSquares_XSet_iff: the X-avoidance condition column by column.
• TauCeti.GridDiagram.commutationMap_apply_apply: the matrix coefficients of Φ are the sums of those of the two pentagon maps; TauCeti.GridDiagram.commutationMap_single_apply states this on a generator.

References

The commutation map is P of Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.1, and Φ_{βγ} of Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.1 (arXiv:math/0610559), both of which count every empty pentagon with a corner at the turn point.

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

The combinatorial shape of a pentagon turning on its initial side, for columns a and finRotate n a, with turn point in 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 together with the curve γ replacing it above the turn point; the rows that side spans must contain the turn row. The points of x sit at the lower-left corner, on β, and the upper-right corner; those of y at the upper-left corner, on γ, and the lower-right corner.

• 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.

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

  The turn point lies on the initial side: its row is among the rows that side spans.

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

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

theorem TauCeti.GridInitialPentagonBetween.ne_finRotate {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridInitialPentagonBetween a s x y) : a ≠ (finRotate n) a

The two columns next to the replaced line of a pentagon turning on its initial side are distinct.

theorem TauCeti.GridInitialPentagonBetween.turn_mem_cIco {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridInitialPentagonBetween a s x y) : s ∈ Grid.cIco (x.toPerm ((finRotate n) a)) (x.toPerm P.right)

The turn row lies in the rows spanned by the initial side, from the row of x on the replaced line to its row on the terminal side.

theorem TauCeti.GridInitialPentagonBetween.turn_mem_cIco_bottom_top {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridInitialPentagonBetween a s x y) : s ∈ Grid.cIco P.bottom P.top

The turn row of a pentagon turning on its initial side lies among its rows.

theorem TauCeti.GridInitialPentagonBetween.bottom_eq_bottom_of_pentagon {n : ℕ} {a s : Fin n} {x y : GridState n} {t : Fin n} {z : GridState n} (Q : GridInitialPentagonBetween a s x y) (P : GridPentagonBetween a t z x) : Q.bottom = P.bottom

A terminal-side pentagon followed by an initial-side pentagon at the same column shares its bottom row with that pentagon, regardless of their turn rows.

theorem TauCeti.GridInitialPentagonBetween.turn_eq_bottom_of_top_eq_finRotate_bottom {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridInitialPentagonBetween a s x y) (hthin : P.top = (finRotate n) P.bottom) : s = P.bottom

An initial-side pentagon spanning one cyclic row turns at its bottom row.

theorem TauCeti.GridInitialPentagonBetween.cIco_bottom_top_eq_singleton_of_top_eq_finRotate_bottom {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridInitialPentagonBetween a s x y) (hthin : P.top = (finRotate n) P.bottom) : Grid.cIco P.bottom P.top = {s}

The row interval of a thin initial-side pentagon consists exactly of its turn row.

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

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

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

There is at most one pentagon 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.GridInitialPentagonBetween.instFintype {n : ℕ} {a s : Fin n} {x y : GridState n} : Fintype (GridInitialPentagonBetween a s x y)

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

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

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

def TauCeti.GridInitialPentagonBetween.ofSwapColumns {n : ℕ} {a 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)) : GridInitialPentagonBetween a s x (GridState.swapColumns ((finRotate n) a) j x)

The pentagon turning on its initial side from x to x.swapColumns (finRotate n a) j, when the turn row lies between the rows of x on the two sides.

@[simp]

theorem TauCeti.GridInitialPentagonBetween.ofSwapColumns_right {n : ℕ} {a 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)) : (ofSwapColumns x j hj hs).right = j

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

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

A pentagon 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 turn row lies between the rows of x on that line and on j.

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

The squares of the original diagram whose marking lies inside a pentagon turning on its initial side.

Away from the two columns next to the replaced line these are the squares covered by the underlying rectangle. In column a they are the rows strictly above the turn row, up to the top side, where the initial side runs along γ to the left of β; in column finRotate n a they are the rows from the bottom side up to and excluding the turn row, where the initial side runs along β. The markings of these two columns in the turn row lie below and above the turn point respectively, and neither is inside the pentagon. As for GridPentagonBetween.coveredSquares, only the marked squares of those two columns matter.

theorem TauCeti.GridInitialPentagonBetween.mem_coveredSquares {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridInitialPentagonBetween a s x y) (p : Fin n × Fin n) : p ∈ P.coveredSquares ↔ p.1 ≠ (finRotate n) a ∧ p.1 ∈ Grid.cIco ((finRotate n) a) P.right ∧ p.2 ∈ Grid.cIco P.bottom P.top ∨ p.1 = a ∧ p.2 ∈ Grid.cIoo s P.top ∨ p.1 = (finRotate n) a ∧ p.2 ∈ Grid.cIco P.bottom s

Membership in the covered squares of a pentagon turning on its initial side, column by column.

theorem TauCeti.GridInitialPentagonBetween.mem_coveredSquares_iff_of_ne {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridInitialPentagonBetween a s x y) {p : Fin n × Fin n} (ha : p.1 ≠ a) (hb : p.1 ≠ (finRotate n) a) : p ∈ P.coveredSquares ↔ p ∈ P.toGridRectangle.coveredSquares

Away from the two columns next to the replaced line, a pentagon turning on its initial side covers the squares of its underlying rectangle.

theorem TauCeti.GridInitialPentagonBetween.mk_mem_coveredSquares_left_column {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridInitialPentagonBetween a s x y) (t : Fin n) : (a, t) ∈ P.coveredSquares ↔ t ∈ Grid.cIoo s P.top

In the column before the replaced line an initial-side pentagon covers the rows strictly between the turn row and its top row.

theorem TauCeti.GridInitialPentagonBetween.mk_mem_coveredSquares_right_column {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridInitialPentagonBetween a s x y) (t : Fin n) : ((finRotate n) a, t) ∈ P.coveredSquares ↔ t ∈ Grid.cIco P.bottom s

In the column after the replaced line an initial-side pentagon covers the rows from its bottom row up to the turn row.

theorem TauCeti.GridInitialPentagonBetween.mk_mem_toGridRectangle_coveredSquares_right_column {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridInitialPentagonBetween a s x y) (t : Fin n) : ((finRotate n) a, t) ∈ P.toGridRectangle.coveredSquares ↔ t ∈ Grid.cIco P.bottom P.top

In the column after the replaced line the underlying rectangle of an initial-side pentagon covers all of its rows.

theorem TauCeti.GridInitialPentagonBetween.mk_notMem_toGridRectangle_coveredSquares_left_column {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridInitialPentagonBetween a s x y) (t : Fin n) : (a, t) ∉ P.toGridRectangle.coveredSquares

The underlying rectangle of an initial-side pentagon covers nothing in the column before the replaced line.

theorem TauCeti.GridInitialPentagonBetween.coveredSquares_eq_product_singleton_of_top_eq_finRotate_bottom {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridInitialPentagonBetween a s x y) (hthin : P.top = (finRotate n) P.bottom) : P.coveredSquares = (Grid.cIco ((finRotate n) a) P.right).erase ((finRotate n) a) ×ˢ {s}

A thin initial-side pentagon covers its turn row in every column of its underlying rectangle except the column immediately after the first commuted column.

theorem TauCeti.GridInitialPentagonBetween.disjoint_coveredSquares_XSet_iff {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridInitialPentagonBetween a 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) ∧ G.X.toPerm a ∉ Grid.cIoo s P.top ∧ G.X.toPerm ((finRotate n) a) ∉ Grid.cIco P.bottom s

A pentagon turning on its initial side carries no X-marking exactly when the underlying rectangle carries none away from columns a and finRotate n a, the X-marking of column a is not above the turn row, and the X-marking of column finRotate n a is not below it.

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

Initial-side pentagons with the same underlying toroidal rectangle cover the same squares.

The pentagons turning on their initial side counted by the commutation map

noncomputable def TauCeti.GridDiagram.initialPentagons {n : ℕ} (G : GridDiagram n) (C : ColumnTurn n) (x y : GridState n) : Finset (GridInitialPentagonBetween C.column C.turnRow x y)

The pentagons turning on their initial side from x to y counted at a column turn: the empty ones carrying no X-marking.

@[simp]

theorem TauCeti.GridDiagram.mem_initialPentagons {n : ℕ} (G : GridDiagram n) {C : ColumnTurn n} {x y : GridState n} (P : GridInitialPentagonBetween C.column C.turnRow x y) : P ∈ G.initialPentagons C x y ↔ P.IsEmpty ∧ Disjoint P.coveredSquares G.XSet

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

theorem TauCeti.GridDiagram.card_initialPentagons_le_one {n : ℕ} (G : GridDiagram n) (C : ColumnTurn n) (x y : GridState n) : (G.initialPentagons C x y).card ≤ 1

At most one pentagon turning on its initial side contributes to each matrix coefficient.

noncomputable def TauCeti.GridDiagram.initialPentagonWeight {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x y : GridState n} (C : ColumnTurn n) (P : GridInitialPentagonBetween C.column C.turnRow x y) : MvPolynomial (Fin n) R

The weight of a pentagon turning on its initial side: the product of the variables that the commuted diagram G.swapColumns a (finRotate n a) attaches to the O-markings the pentagon carries. As for GridDiagram.pentagonWeight, the O-marking of column c of G contributes the variable of column Equiv.swap a (finRotate n a) c.

theorem TauCeti.GridDiagram.initialPentagonWeight_eq_monomial {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x y : GridState n} (C : ColumnTurn n) (P : GridInitialPentagonBetween C.column C.turnRow x y) : G.initialPentagonWeight R C P = (MvPolynomial.monomial (∑ c ∈ G.OColumnsOfSquares P.coveredSquares, Finsupp.single ((Equiv.swap C.column ((finRotate n) C.column)) c) 1)) 1

The weight of an initial-side pentagon is the monomial with one renamed variable for each covered O-marking.

theorem TauCeti.GridDiagram.initialPentagonWeight_eq_prod_coveredSquares {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x y : GridState n} (C : ColumnTurn n) (P : GridInitialPentagonBetween C.column C.turnRow x y) : G.initialPentagonWeight R C P = ∏ p ∈ P.coveredSquares, if p ∈ G.OSet then MvPolynomial.X ((Equiv.swap C.column ((finRotate n) C.column)) p.1) else 1

The weight of a pentagon turning on its initial side as a product over the squares it covers: the renamed variable of the column at each O-marked square and 1 elsewhere.

theorem TauCeti.GridDiagram.rename_initialPentagonWeight {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x y : GridState n} (C : ColumnTurn n) (P : GridInitialPentagonBetween C.column C.turnRow x y) : (MvPolynomial.rename ⇑(Equiv.swap C.column ((finRotate n) C.column))) (G.initialPentagonWeight R C P) = ∏ p ∈ P.coveredSquares, if p ∈ G.OSet then MvPolynomial.X p.1 else 1

Renamed back by the column swap, the weight of a pentagon turning on its initial side is the product, over the squares it covers, of the variable of the square's column in G at the O-marked squares and of 1 elsewhere.

theorem TauCeti.GridDiagram.initialPentagonWeight_swapColumns {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {y z : GridState n} (C : ColumnTurn n) (Q : GridInitialPentagonBetween C.column C.turnRow y z) : (swapColumns C.column ((finRotate n) C.column) G).initialPentagonWeight R C Q = ∏ p ∈ Finset.map (Equiv.prodCongr (Equiv.swap C.column ((finRotate n) C.column)) (Equiv.refl (Fin n))).toEmbedding Q.coveredSquares, if p ∈ G.OSet then MvPolynomial.X p.1 else 1

The weight of a pentagon turning on its initial side in column C.column, counted in the diagram obtained by exchanging that column with the next one, is the product, over the squares it covers read in G by exchanging the two columns, of the variable of the square's column at the O-marked squares of G and of 1 elsewhere.

theorem TauCeti.GridDiagram.initialPentagonWeight_reverse {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {y z : GridState n} (C : G.ColumnCommutationData) (Q : GridInitialPentagonBetween C.reverse.column C.reverse.turnRow y z) : (swapColumns C.column ((finRotate n) C.column) G).initialPentagonWeight R C.reverse.toColumnTurn Q = ∏ p ∈ Finset.map (Equiv.prodCongr (Equiv.swap C.column ((finRotate n) C.column)) (Equiv.refl (Fin n))).toEmbedding Q.coveredSquares, if p ∈ G.OSet then MvPolynomial.X p.1 else 1

The weight of a pentagon of the reverse commutation turning on its initial side, counted in the commuted diagram, is the product, over the squares it covers read in G by exchanging the two commuted columns, of the variable of the square's column at the O-marked squares of G and of 1 elsewhere.

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

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

theorem TauCeti.GridDiagram.initialPentagonCoefficient_def {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : ColumnTurn n) (x y : GridState n) : G.initialPentagonCoefficient R C x y = ∑ P ∈ G.initialPentagons C x y, G.initialPentagonWeight R C P

The matrix coefficient of the initial-side pentagon map is the sum of the weights of its counted pentagons.

noncomputable def TauCeti.GridDiagram.initialPentagonMap {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : ColumnTurn n) : GridChainMinus R n →ₛₗ[↑(MvPolynomial.renameEquiv R (Equiv.swap C.column ((finRotate n) C.column))).toRingEquiv] GridChainMinus R n

The map GC⁻(G) → GC⁻(G.swapColumns C.column (finRotate n C.column)) counting the pentagons that turn on their initial side, semilinear over the renaming of the variables by Equiv.swap C.column (finRotate n C.column).

@[simp]

theorem TauCeti.GridDiagram.initialPentagonMap_single {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : ColumnTurn n) (x : GridState n) (p : MvPolynomial (Fin n) R) : (G.initialPentagonMap R C) (Finsupp.single x p) = (MvPolynomial.rename ⇑(Equiv.swap C.column ((finRotate n) C.column))) p • ∑ y : GridState n, Finsupp.single y (G.initialPentagonCoefficient R C x y)

The initial-side pentagon map sends a generator with coefficient p to the renamed coefficient times the row of its matrix coefficients.

@[simp]

theorem TauCeti.GridDiagram.initialPentagonMap_apply_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : ColumnTurn n) (c : GridChainMinus R n) (y : GridState n) : ((G.initialPentagonMap R C) c) y = Finsupp.sum c fun (x : GridState n) (p : MvPolynomial (Fin n) R) => (MvPolynomial.rename ⇑(Equiv.swap C.column ((finRotate n) C.column))) p * G.initialPentagonCoefficient R C x y

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

The commutation map

noncomputable def TauCeti.GridDiagram.commutationMap {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : ColumnTurn n) : GridChainMinus R n →ₛₗ[↑(MvPolynomial.renameEquiv R (Equiv.swap C.column ((finRotate n) C.column))).toRingEquiv] GridChainMinus R n

The commutation map Φ : GC⁻(G) → GC⁻(G.swapColumns C.column (finRotate n C.column)) of the column turn C: it counts the empty pentagons carrying no X-marking with a corner at the turn point, both those turning on their terminal side (GridDiagram.pentagonMap) and those turning on their initial side (GridDiagram.initialPentagonMap).

theorem TauCeti.GridDiagram.commutationMap_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : ColumnTurn n) (c : GridChainMinus R n) : (G.commutationMap R C) c = (G.pentagonMap R C) c + (G.initialPentagonMap R C) c

The commutation map is the sum of the two pentagon maps.

@[simp]

theorem TauCeti.GridDiagram.commutationMap_apply_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : ColumnTurn n) (c : GridChainMinus R n) (y : GridState n) : ((G.commutationMap R C) c) y = Finsupp.sum c fun (x : GridState n) (p : MvPolynomial (Fin n) R) => (MvPolynomial.rename ⇑(Equiv.swap C.column ((finRotate n) C.column))) p * (G.pentagonCoefficient R C x y + G.initialPentagonCoefficient R C x y)

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

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

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

theorem TauCeti.GridDiagram.commutationPentagonCoefficient_def {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : ColumnTurn n) (x y : GridState n) : G.commutationPentagonCoefficient R C x y = G.pentagonCoefficient R C x y + G.initialPentagonCoefficient R C x y

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

theorem TauCeti.GridDiagram.commutationMap_single_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : ColumnTurn n) (x y : GridState n) : ((G.commutationMap R C) (Finsupp.single x 1)) y = G.commutationPentagonCoefficient R C x y

The matrix coefficients of the commutation map are the commutation pentagon coefficients.