Pentagons of a column commutation

Let G be a grid diagram and let b = finRotate n a be the column following column a. The column commutation G' = G.swapColumns a b is compared with G by drawing both diagrams on one torus: the vertical grid line β between columns a and b (the line with index b) is replaced by a curve γ which meets β in two points and bounds with it two thin bigons. The column-a markings of G lie in one bigon, on the right of γ, and the column-b markings in the other, on the left of γ, so that reading the markings off with γ in place of β gives G'. Every other grid line is shared by the two diagrams, so a grid state of G' is again a permutation of Fin n whose value at the line index b is its row on γ.

A pentagon from a state x of G to a state y of G' is an embedded disk bounded by five arcs: starting at the point of x on β, it runs left along a horizontal circle to a point of y, down a vertical line to a point of x, right along a horizontal circle to the point of y on γ, up γ to one of the two intersection points of β and γ, and up β back to the start. All corners are convex, which forces the intersection point to be the one, called the turn point, at which γ crosses from the left of β to its right going upwards. Just below the turn point lies the bigon carrying the column-a markings, and just above it the bigon carrying the column-b markings.

The pentagons, and the map below, depend only on the column a and the row of the turn point, recorded by GridDiagram.ColumnTurn. For a commutation, GridDiagram.ColumnCommutationData extends this by the row of the other intersection and certifies that the markings lie in the appropriate two bigons. Every elementary column commutation admits such data (GridDiagram.isColumnCommutation_iff_exists_columnCommutationData), so the map below is available for each of them. The same count applies to any curve γ leaving the column-a markings on its right and the column-b markings on its left, at any of its intersections with β of the turning kind, even when γ meets β in more than two points because the two marking segments interleave. The combinatorics of a pentagon is recorded with no curve in sight. Its corners are those of the oriented rectangle from x to y whose terminal side is the line b (GridPentagonBetween, which extends GridRectangleBetween); the turn row must lie in the rows spanned by the terminal side. The lattice points strictly inside the pentagon are those strictly inside that rectangle, so emptiness is GridRectangleBetween.IsEmpty. The markings it carries differ from those of the rectangle only in the two columns next to β (GridPentagonBetween.coveredSquares): a column-a marking is inside exactly when it lies above the turn point, where the terminal side runs along β, and a column-b marking exactly when it lies below the turn point, where the terminal side runs along γ to the right of β. A column-a marking in the row of the turn point lies below it and a column-b marking lies above it, since they lie in the bigons below and above the turn point respectively.

The pentagon map GC⁻(G) → GC⁻(G') (GridDiagram.pentagonMap) counts the empty pentagons carrying no X-marking, each weighted by the product of the variables of the O-markings it carries. The variable of an O-marking is the one attached to its column in G', so the weight of a covered column-c marking of G is V_{swap a b c}, and the map is semilinear over the renaming of the variables by Equiv.swap a b. The reverse comparison GC⁻(G') → GC⁻(G) counts pentagons turning at the other intersection point; seen from G', where γ is the grid line and β the replacement curve, that is the same construction for G' with the square row of the other intersection point as its turn row.

The pentagons here lie to the left of β ∪ γ. The commutation map Φ also counts the pentagons lying to its right, whose initial side turns at the same point; those, and Φ itself (GridDiagram.commutationMap), are in Commutation/InitialPentagon/Basic.lean. The map defined here is only one part of Φ and is not a chain map on its own.

This file sets up the pentagons and the map. That Φ is a chain map, and that together with the reverse map it is a chain homotopy equivalence via the hexagon-counting homotopies, is not proved here.

Main definitions

• TauCeti.GridPentagonBetween: the combinatorial shape of a pentagon, recorded by its corners and its turn row.
• TauCeti.GridPentagonBetween.coveredSquares: the squares of G whose marking lies inside the pentagon.
• TauCeti.GridDiagram.pentagons: the empty pentagons carrying no X-marking.
• TauCeti.GridDiagram.pentagonWeight: the monomial weighting a pentagon.
• TauCeti.GridDiagram.pentagonCoefficient: the matrix coefficients of the pentagon map.
• TauCeti.GridDiagram.pentagonMap: the map GC⁻(G) → GC⁻(G.swapColumns a b) counting these pentagons, the terminal-side part of the commutation map Φ.

Main results

• TauCeti.GridPentagonBetween.nonempty_iff: 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 j and on b; Subsingleton records that it is then unique.
• TauCeti.GridPentagonBetween.mem_coveredSquares, TauCeti.GridPentagonBetween.mem_coveredSquares_iff_of_ne: the covered squares, which agree with those of the underlying rectangle away from columns a and b. TauCeti.GridPentagonBetween.mk_mem_coveredSquares_left_column and TauCeti.GridPentagonBetween.mk_mem_coveredSquares_right_column give them in those two columns.
• TauCeti.GridPentagonBetween.coveredSquares_eq_product_singleton_of_top_eq_finRotate_bottom: a pentagon spanning one row covers that row away from the first commuted column.
• TauCeti.GridPentagonBetween.disjoint_coveredSquares_XSet_iff: the X-avoidance condition column by column.
• TauCeti.GridPentagonBetween.coveredSquares_subset_union_of_stacked: a pentagon spanning a pentagon with a rectangle stacked on it covers only squares one of those two covers.
• TauCeti.GridDiagram.pentagonWeight_eq_prod_coveredSquares, TauCeti.GridDiagram.pentagonWeight_eq_prod_swapColumns: the weight as a product over the covered squares, and as the product of the variables of the covered O-markings of the commuted diagram.
• TauCeti.GridDiagram.pentagonMap_single, TauCeti.GridDiagram.pentagonMap_apply_apply: the action of the pentagon map on generators and its matrix coefficients.
• TauCeti.GridDiagram.pentagonMapOnGenerator_support_subset: the pentagon map moves a generator only by swapping its point on β against one other point.

References

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

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

The combinatorial shape of a pentagon 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 terminal side is the grid line finRotate n a replaced by the curve γ; the rows that side spans must contain the turn row. The points of x sit at the lower-left and upper-right corners and those of y at the upper-left and lower-right corners, the latter on γ. A pentagon-counting map only uses these shapes through a GridDiagram.ColumnTurn, which records the column a and the turn row s.

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

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

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

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

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

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

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

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

The two columns next to the replaced grid line of a pentagon are distinct.

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

The turn row of a pentagon lies among its rows.

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

A pentagon spanning one cyclic row turns at its bottom row.

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

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

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

A pentagon is determined by its initial side.

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

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

There are finitely many pentagons between two grid states.

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

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

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

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

def TauCeti.GridPentagonBetween.ofRightEq {n : ℕ} {a s : Fin n} {u v : GridState n} (r : GridRectangleBetween u v) (hright : r.right = (finRotate n) a) (hs : s ∈ Grid.cIco r.bottom r.top) : GridPentagonBetween a s u v

Regard an oriented rectangle as a pentagon: its terminal side must be the grid line replaced by γ, and the turn row must lie among the rows that side spans.

@[simp]

theorem TauCeti.GridPentagonBetween.ofRightEq_toGridRectangleBetween {n : ℕ} {a s : Fin n} {u v : GridState n} (r : GridRectangleBetween u v) (hright : r.right = (finRotate n) a) (hs : s ∈ Grid.cIco r.bottom r.top) : (ofRightEq r hright hs).toGridRectangleBetween = r

The rectangle underlying ofRightEq is the supplied rectangle.

theorem TauCeti.GridPentagonBetween.ofRightEq_right {n : ℕ} {a s : Fin n} {u v : GridState n} (r : GridRectangleBetween u v) (hright : r.right = (finRotate n) a) (hs : s ∈ Grid.cIco r.bottom r.top) : (ofRightEq r hright hs).right = (finRotate n) a

The terminal side of ofRightEq is the grid line replaced by γ.

theorem TauCeti.GridPentagonBetween.ofRightEq_left {n : ℕ} {a s : Fin n} {u v : GridState n} (r : GridRectangleBetween u v) (hright : r.right = (finRotate n) a) (hs : s ∈ Grid.cIco r.bottom r.top) : (ofRightEq r hright hs).left = r.left

The initial side of ofRightEq is the rectangle's.

theorem TauCeti.GridPentagonBetween.ofRightEq_bottom {n : ℕ} {a s : Fin n} {u v : GridState n} (r : GridRectangleBetween u v) (hright : r.right = (finRotate n) a) (hs : s ∈ Grid.cIco r.bottom r.top) : (ofRightEq r hright hs).bottom = r.bottom

The bottom row of ofRightEq is the rectangle's.

theorem TauCeti.GridPentagonBetween.ofRightEq_top {n : ℕ} {a s : Fin n} {u v : GridState n} (r : GridRectangleBetween u v) (hright : r.right = (finRotate n) a) (hs : s ∈ Grid.cIco r.bottom r.top) : (ofRightEq r hright hs).top = r.top

The top row of ofRightEq is the rectangle's.

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

Regard a rectangle between possibly different endpoint states as a pentagon when its underlying toroidal rectangle agrees with that of an existing pentagon.

@[simp]

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

The rectangle underlying ofToGridRectangleEq is the supplied rectangle.

@[simp]

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

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

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

A pentagon from x to y exists exactly when y is x with some column j swapped against the line replaced by γ, and the turn row lies between the rows of x on j and on that line.

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

The squares of the original diagram whose marking lies inside the pentagon.

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 terminal side runs along β; in column finRotate n a they are the rows from the bottom side up to and excluding the turn row, where the terminal side runs along γ to the right of β. The markings of these two columns in the turn row lie below and above the turn point respectively, and neither is inside the pentagon.

These are the correct squares for the markings of columns a and finRotate n a when the turn point is placed as in the combined diagram of the commutation: the column-a markings in the bigon below it and the column-finRotate n a markings in the bigon above it. Only marked squares of those two columns matter for the weights and the X-avoidance condition.

theorem TauCeti.GridPentagonBetween.mem_coveredSquares {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridPentagonBetween a s x y) (p : Fin n × Fin n) : p ∈ P.coveredSquares ↔ p.1 ≠ a ∧ p.1 ∈ Grid.cIco P.left ((finRotate n) a) ∧ 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, column by column.

theorem TauCeti.GridPentagonBetween.mem_cIco_of_mem_coveredSquares {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridPentagonBetween a s x y) {p : Fin n × Fin n} (hp : p ∈ P.coveredSquares) : p.2 ∈ Grid.cIco P.bottom P.top

Every square covered by a pentagon lies in the row arc of its underlying rectangle.

theorem TauCeti.GridPentagonBetween.disjoint_coveredSquares_of_forall_mem_cIco {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridPentagonBetween a s x y) {S : Finset (Fin n × Fin n)} (hS : ∀ p ∈ S, p.2 ∈ Grid.cIco P.top P.bottom) : Disjoint P.coveredSquares S

A pentagon covers no square in a set supported on the complementary row arc.

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

A pentagon spanning one cyclic row has its turn in that row and covers only the columns of its underlying rectangle other than the first commuted column.

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

Pentagons with the same underlying toroidal rectangle cover the same squares.

theorem TauCeti.GridPentagonBetween.mem_coveredSquares_iff_of_ne {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridPentagonBetween 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 covers the squares of its underlying rectangle.

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

In the column before the replaced grid line a pentagon covers the rows above the turn row.

theorem TauCeti.GridPentagonBetween.mk_mem_coveredSquares_right_column {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridPentagonBetween 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 grid line a pentagon covers the rows from its bottom row up to the turn row.

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

In the column before the replaced grid line the underlying rectangle of a pentagon covers all of its rows.

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

The underlying rectangle of a pentagon covers nothing in the column after the replaced grid line.

theorem TauCeti.GridPentagonBetween.coveredSquares_subset_union_of_stacked {n : ℕ} {a s : Fin n} {u v u' v' : GridState n} (Q : GridPentagonBetween a s u v) (P : GridPentagonBetween a s u' v') (r : GridRectangle n) (hbottom : Q.bottom = P.bottom) (htop : Q.top = r.top) (hcut : P.top = r.bottom) (hP : Grid.cIco Q.left ((finRotate n) a) ⊆ Grid.cIco P.left ((finRotate n) a)) (hr : Grid.cIco Q.left ((finRotate n) a) ⊆ Grid.cIco r.left r.right) : Q.coveredSquares ⊆ P.coveredSquares ∪ r.coveredSquares

A pentagon spanning a pentagon with a toroidal rectangle stacked on it covers only squares one of those two covers.

The hypotheses place P directly below r, the top row of P being the bottom row of r, and make Q span the two of them: the rows of Q run from the bottom row of P to the top row of r, and its column arc lies inside both of theirs. The two columns next to the replaced grid line are what makes this more than the corresponding statement about the underlying rectangles: in column a the arc of Q above the turn row is cut into the arc of P above the turn row and a band of rows of r, and in column finRotate n a the arc of Q below the turn row is the one P covers, because the two pentagons share a bottom row.

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

A pentagon 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.

The pentagons counted by the pentagon map

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

The pentagons from x to y counted at a column turn: the empty pentagons carrying no X-marking.

@[simp]

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

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

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

At most one pentagon contributes to each matrix coefficient of the pentagon map.

noncomputable def TauCeti.GridDiagram.pentagonOColumns {n : ℕ} (G : GridDiagram n) {x y : GridState n} (C : ColumnTurn n) (P : GridPentagonBetween C.column C.turnRow x y) : Finset (Fin n)

The columns of the original diagram whose O-marking a pentagon carries.

@[simp]

theorem TauCeti.GridDiagram.mem_pentagonOColumns {n : ℕ} (G : GridDiagram n) {x y : GridState n} {C : ColumnTurn n} {P : GridPentagonBetween C.column C.turnRow x y} {c : Fin n} : c ∈ G.pentagonOColumns C P ↔ (c, G.O.toPerm c) ∈ P.coveredSquares

A column is a covered O-column of a pentagon exactly when its O-marking is a covered square.

theorem TauCeti.GridDiagram.card_pentagonOColumns {n : ℕ} (G : GridDiagram n) {x y : GridState n} (C : ColumnTurn n) (P : GridPentagonBetween C.column C.turnRow x y) : (G.pentagonOColumns C P).card = (G.OSet ∩ P.coveredSquares).card

The number of columns whose O-marking a pentagon carries is the number of O-markings among the squares it covers.

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

The weight of a pentagon in the pentagon map: the product of the variables that the commuted diagram G.swapColumns a (finRotate n a) attaches to the O-markings the pentagon carries.

The O-marking of column c of G is the O-marking of column Equiv.swap a (finRotate n a) c of the commuted diagram, so it contributes the variable of that column.

theorem TauCeti.GridDiagram.pentagonWeight_eq_prod_coveredSquares {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x y : GridState n} (C : ColumnTurn n) (P : GridPentagonBetween C.column C.turnRow x y) : G.pentagonWeight 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 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.pentagonWeight_eq_prod_swapColumns {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x y : GridState n} (C : ColumnTurn n) (P : GridPentagonBetween C.column C.turnRow x y) : G.pentagonWeight R C P = ∏ c : Fin n with ((Equiv.swap C.column ((finRotate n) C.column)) c, (swapColumns C.column ((finRotate n) C.column) G).O.toPerm c) ∈ P.coveredSquares, MvPolynomial.X c

The weight of a pentagon is the product of the variables of the columns of the commuted diagram whose O-marking the pentagon carries.

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

The pentagon weight is the squarefree monomial of its covered O-columns, with variables renamed by the column swap.

theorem TauCeti.GridDiagram.rename_pentagonWeight {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x y : GridState n} (C : ColumnTurn n) (P : GridPentagonBetween C.column C.turnRow x y) : (MvPolynomial.rename ⇑(Equiv.swap C.column ((finRotate n) C.column))) (G.pentagonWeight 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 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: the weight a rectangle covering the same squares would have in G.

theorem TauCeti.GridDiagram.pentagonWeight_swapColumns {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {y z : GridState n} (C : ColumnTurn n) (Q : GridPentagonBetween C.column C.turnRow y z) : (swapColumns C.column ((finRotate n) C.column) G).pentagonWeight 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 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.pentagonWeight_reverse {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {y z : GridState n} (C : G.ColumnCommutationData) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) : (swapColumns C.column ((finRotate n) C.column) G).pentagonWeight 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, which turns at the opposite intersection and is 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.

The pentagon map

noncomputable def TauCeti.GridDiagram.pentagonCoefficient {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 pentagon map from x to y: the sum of the weights of the empty pentagons from x to y carrying no X-marking.

theorem TauCeti.GridDiagram.pentagonCoefficient_def {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : ColumnTurn n) (x y : GridState n) : G.pentagonCoefficient R C x y = ∑ P ∈ G.pentagons C x y, G.pentagonWeight R C P

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

noncomputable def TauCeti.GridDiagram.pentagonMapOnGenerator {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : ColumnTurn n) (x : GridState n) : GridChainMinus R n

The value of the pentagon map on a single grid-state generator.

@[simp]

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

The y-coefficient of the pentagon map on the generator x.

theorem TauCeti.GridDiagram.pentagonMapOnGenerator_support_subset {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : ColumnTurn n) (x : GridState n) : (G.pentagonMapOnGenerator R C x).support ⊆ Finset.image (fun (j : Fin n) => GridState.swapColumns j ((finRotate n) C.column) x) Finset.univ

The pentagon map moves a generator only by swapping its point on the replaced line against one other point.

noncomputable def TauCeti.GridDiagram.pentagonMap {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 pentagon map GC⁻(G) → GC⁻(G.swapColumns C.column (finRotate n C.column)) of the column turn C, counting the pentagons whose turn lies on their terminal side.

A generator x goes to the sum over the counted pentagons from x of their weights times their targets. The map is semilinear over the renaming of the variables by Equiv.swap C.column (finRotate n C.column), which carries the variable of each O-marking in G to its variable in the commuted diagram. It is only one of the two parts of the commutation map Φ; the other counts the pentagons turning on their initial side (TauCeti.GridDiagram.initialPentagonMap).

@[simp]

theorem TauCeti.GridDiagram.pentagonMap_single {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : ColumnTurn n) (x : GridState n) (p : MvPolynomial (Fin n) R) : (G.pentagonMap R C) (Finsupp.single x p) = (MvPolynomial.rename ⇑(Equiv.swap C.column ((finRotate n) C.column))) p • G.pentagonMapOnGenerator R C x

The pentagon map sends a generator with coefficient p to the renamed coefficient times the row of pentagon weights of the generator.

@[simp]

theorem TauCeti.GridDiagram.pentagonMap_apply_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : ColumnTurn n) (c : GridChainMinus R n) (y : GridState n) : ((G.pentagonMap 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

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