Composite domains in the grid-commutation homotopy equation

The homotopy equation for a column commutation compares three kinds of two-step domain. On its left are a commutation hexagon followed by a rectangle and a rectangle followed by a commutation hexagon. On its right are two commutation pentagons, the second for the reverse commutation. Each commutation polygon may turn on either side of the replaced grid line.

This file packages those alternatives and rewrites the matrix-coefficient equation as sums over finite families of composite domains. In this form every summand records the actual polygons it counts, rather than only their intermediate grid state. This is the input for the geometric pairing of juxtaposed domains in the proof of commutation invariance.

The two kinds of hexagon and pentagon are represented by sum types. This retains the distinction between the two turn sides while avoiding four parallel decomposition types. All three composite domain families specialize the generic two-step decomposition TauCeti.GridTwoStepDecomposition, whose counted finite families have membership characterizations.

Main results

• TauCeti.GridDiagram.sum_commutationHexagonCoefficient_mul_unblockedCoefficient and TauCeti.GridDiagram.sum_unblockedCoefficient_mul_commutationHexagonCoefficient rewrite the two rectangle--hexagon matrix products as composite-domain sums.
• TauCeti.GridDiagram.sum_rename_commutationPentagonCoefficient_mul_commutationPentagonCoefficient rewrites the round-trip commutation coefficient as a sum over pairs of pentagons.
• TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_add_eq_iff_decompositions states the homotopy equation entirely in terms of the three finite domain families.
• TauCeti.GridHexagonCompositeDecomposition combines the two orders of hexagon--rectangle composition, with counted family TauCeti.GridDiagram.hexagonCompositeDecompositions and weight TauCeti.GridDiagram.hexagonCompositeWeight.
• TauCeti.GridDiagram.XSet_inter_coveredSquares_of_mem_commutationHexagons and TauCeti.GridDiagram.X_cutColumn_mul_commutationHexagonWeight: the rectangle under a counted commutation hexagon carries exactly one X-marking, in the column the hexagon cuts away (TauCeti.GridCommutationHexagonBetween.cutColumn), and its weight exceeds the hexagon weight by the variable of that column.

References

Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.1, and Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.1 (arXiv:math/0610559).

@[reducible, inline]

abbrev TauCeti.GridCommutationHexagonBetween {n : ℕ} (a s s' : Fin n) (x y : GridState n) : Type

A commutation hexagon for column a, turn row s and opposite turn row s' is either a hexagon turning on its terminal side or one turning on its initial side.

The two row parameters play opposite roles in the two cases: the terminal-side hexagon GridHexagonBetween a s' s cuts away the bigon from s' up to s, while the initial-side hexagon GridInitialHexagonBetween a s s' cuts away the bigon from s up to s'.

def TauCeti.GridCommutationHexagonBetween.toGridRectangleBetween {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridCommutationHexagonBetween a s s' x y) : GridRectangleBetween x y

Forget the two turns of a commutation hexagon, retaining its oriented rectangle.

@[simp]

theorem TauCeti.GridCommutationHexagonBetween.toGridRectangleBetween_inl {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridHexagonBetween a s' s x y) : toGridRectangleBetween (Sum.inl P) = P.toGridRectangleBetween

The toGridRectangleBetween accessor on a terminal-side hexagon.

@[simp]

theorem TauCeti.GridCommutationHexagonBetween.toGridRectangleBetween_inr {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridInitialHexagonBetween a s s' x y) : toGridRectangleBetween (Sum.inr P) = P.toGridRectangleBetween

The toGridRectangleBetween accessor on a initial-side hexagon.

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

The underlying rectangle determines a commutation hexagon, including its turn side.

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

The marking squares covered by a commutation hexagon of either turn-side kind.

@[simp]

theorem TauCeti.GridCommutationHexagonBetween.coveredSquares_inl {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridHexagonBetween a s' s x y) : coveredSquares (Sum.inl P) = P.coveredSquares

The coveredSquares accessor on a terminal-side hexagon.

@[simp]

theorem TauCeti.GridCommutationHexagonBetween.coveredSquares_inr {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridInitialHexagonBetween a s s' x y) : coveredSquares (Sum.inr P) = P.coveredSquares

The coveredSquares accessor on a initial-side hexagon.

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

Transfer a commutation hexagon along an equality of underlying toroidal rectangles, preserving the turn-side kind.

@[simp]

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

Forgetting a transferred commutation hexagon returns the supplied rectangle.

@[simp]

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

Transferring a commutation hexagon preserves the marking squares it covers.

def TauCeti.GridCommutationHexagonBetween.cutColumn {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridCommutationHexagonBetween a s s' x y) : Fin n

The column of the underlying rectangle that a commutation hexagon cuts away: column a for a hexagon turning on its terminal side and the column after it for one turning on its initial side. For a validated column commutation it is the column whose markings lie in the cut-away bigon.

@[simp]

theorem TauCeti.GridCommutationHexagonBetween.cutColumn_inl {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridHexagonBetween a s' s x y) : cutColumn (Sum.inl P) = a

A hexagon turning on its terminal side cuts away column a.

@[simp]

theorem TauCeti.GridCommutationHexagonBetween.cutColumn_inr {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridInitialHexagonBetween a s s' x y) : cutColumn (Sum.inr P) = (finRotate n) a

A hexagon turning on its initial side cuts away the column after a.

theorem TauCeti.GridCommutationHexagonBetween.left_eq_or_right_eq {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridCommutationHexagonBetween a s s' x y) : P.toGridRectangleBetween.left = (finRotate n) a ∨ P.toGridRectangleBetween.right = (finRotate n) a

A commutation hexagon has the replaced grid line as a side.

theorem TauCeti.GridCommutationHexagonBetween.pair_subset_cIco_bottom_top {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridCommutationHexagonBetween a s s' x y) : {s, s'} ⊆ Grid.cIco P.toGridRectangleBetween.bottom P.toGridRectangleBetween.top

Both intersection rows lie among the rows of a commutation hexagon.

theorem TauCeti.GridCommutationHexagonBetween.ne {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridCommutationHexagonBetween a s s' x y) : s ≠ s'

The two intersection rows of a commutation hexagon are distinct.

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

Away from the two columns next to the replaced line, a commutation hexagon covers the squares of its underlying rectangle.

theorem TauCeti.GridCommutationHexagonBetween.mk_notMem_coveredSquares_left_column {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridCommutationHexagonBetween a s s' x y) (t : Fin n) : (a, t) ∉ P.coveredSquares

A commutation hexagon covers no square of the column before the replaced line.

theorem TauCeti.GridCommutationHexagonBetween.mk_notMem_coveredSquares_right_column {n : ℕ} {a s s' : Fin n} {x y : GridState n} (P : GridCommutationHexagonBetween a s s' x y) (t : Fin n) : ((finRotate n) a, t) ∉ P.coveredSquares

A commutation hexagon covers no square of the column after the replaced line.

@[reducible, inline]

abbrev TauCeti.GridCommutationPentagonBetween {n : ℕ} (a s : Fin n) (x y : GridState n) : Type

A commutation pentagon is either a pentagon turning on its terminal side or one turning on its initial side.

def TauCeti.GridCommutationPentagonBetween.toGridRectangleBetween {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridCommutationPentagonBetween a s x y) : GridRectangleBetween x y

Forget the turn of a commutation pentagon, retaining its oriented rectangle.

@[simp]

theorem TauCeti.GridCommutationPentagonBetween.toGridRectangleBetween_inl {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridPentagonBetween a s x y) : toGridRectangleBetween (Sum.inl P) = P.toGridRectangleBetween

@[simp]

theorem TauCeti.GridCommutationPentagonBetween.toGridRectangleBetween_inr {n : ℕ} {a s : Fin n} {x y : GridState n} (P : GridInitialPentagonBetween a s x y) : toGridRectangleBetween (Sum.inr P) = P.toGridRectangleBetween

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

The underlying oriented rectangle determines a commutation pentagon, including its side.

@[reducible, inline]

abbrev TauCeti.GridHexagonRectangleDecomposition {n : ℕ} (a s s' : Fin n) (x z : GridState n) : Type

A two-step domain consisting of a commutation hexagon followed by a rectangle.

@[reducible, inline]

abbrev TauCeti.GridHexagonRectangleDecomposition.hexagon {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridHexagonRectangleDecomposition a s s' x z) : GridCommutationHexagonBetween a s s' x D.middle

The commutation hexagon in a hexagon--rectangle decomposition.

@[reducible, inline]

abbrev TauCeti.GridHexagonRectangleDecomposition.rectangle {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridHexagonRectangleDecomposition a s s' x z) : GridRectangleBetween D.middle z

The rectangle in a hexagon--rectangle decomposition.

@[reducible, inline]

abbrev TauCeti.GridHexagonRectangleDecomposition.toRectangleDecomposition {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridHexagonRectangleDecomposition a s s' x z) : GridRectangleDecomposition x z

Forget the turns of the hexagon in a hexagon--rectangle domain.

theorem TauCeti.GridHexagonRectangleDecomposition.toRectangleDecomposition_injective {n : ℕ} {a s s' : Fin n} {x z : GridState n} : Function.Injective toRectangleDecomposition

Forgetting the hexagon turns is injective on two-step domains.

@[reducible, inline]

abbrev TauCeti.GridRectangleHexagonDecomposition {n : ℕ} (a s s' : Fin n) (x z : GridState n) : Type

A two-step domain consisting of a rectangle followed by a commutation hexagon.

@[reducible, inline]

abbrev TauCeti.GridRectangleHexagonDecomposition.rectangle {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridRectangleHexagonDecomposition a s s' x z) : GridRectangleBetween x D.middle

The rectangle in a rectangle--hexagon decomposition.

@[reducible, inline]

abbrev TauCeti.GridRectangleHexagonDecomposition.hexagon {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridRectangleHexagonDecomposition a s s' x z) : GridCommutationHexagonBetween a s s' D.middle z

The commutation hexagon in a rectangle--hexagon decomposition.

@[reducible, inline]

abbrev TauCeti.GridRectangleHexagonDecomposition.toRectangleDecomposition {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridRectangleHexagonDecomposition a s s' x z) : GridRectangleDecomposition x z

Forget the turns of the hexagon in a rectangle--hexagon domain.

theorem TauCeti.GridRectangleHexagonDecomposition.toRectangleDecomposition_injective {n : ℕ} {a s s' : Fin n} {x z : GridState n} : Function.Injective toRectangleDecomposition

Forgetting the hexagon turns is injective on two-step domains.

@[reducible, inline]

abbrev TauCeti.GridHexagonCompositeDecomposition {n : ℕ} (a s s' : Fin n) (x z : GridState n) : Type

A two-step domain on the left-hand side of the commutation homotopy equation: a commutation hexagon followed by a rectangle, or a rectangle followed by a commutation hexagon.

def TauCeti.GridHexagonCompositeDecomposition.toRectangleDecomposition {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridHexagonCompositeDecomposition a s s' x z) : GridRectangleDecomposition x z

Forget the turns of the hexagon in a hexagon composite.

@[simp]

theorem TauCeti.GridHexagonCompositeDecomposition.toRectangleDecomposition_inl {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridHexagonRectangleDecomposition a s s' x z) : toRectangleDecomposition (Sum.inl D) = D.toRectangleDecomposition

The underlying rectangle decomposition of a hexagon followed by a rectangle.

@[simp]

theorem TauCeti.GridHexagonCompositeDecomposition.toRectangleDecomposition_inr {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridRectangleHexagonDecomposition a s s' x z) : toRectangleDecomposition (Sum.inr D) = D.toRectangleDecomposition

The underlying rectangle decomposition of a rectangle followed by a hexagon.

theorem TauCeti.GridHexagonCompositeDecomposition.injOn_toRectangleDecomposition_of_isLeft_iff {n : ℕ} {a s s' : Fin n} {x z : GridState n} {S : Set (GridHexagonCompositeDecomposition a s s' x z)} (p : GridRectangleDecomposition x z → Prop) (h : ∀ D ∈ S, Sum.isLeft D = true ↔ p D.toRectangleDecomposition) : Set.InjOn toRectangleDecomposition S

A family of hexagon composites is determined by the underlying rectangle decompositions as soon as a property of the underlying decomposition tells which piece is the hexagon.

theorem TauCeti.GridHexagonCompositeDecomposition.toRectangleDecomposition_ne_of_notMem_cIco {n : ℕ} {a s s' : Fin n} {x z : GridState n} (F : GridHexagonCompositeDecomposition a s s' x z) {D : GridRectangleDecomposition x z} (hs' : s' ∉ Grid.cIco D.first.bottom D.first.top) (hs : s ∉ Grid.cIco D.second.bottom D.second.top) : F.toRectangleDecomposition ≠ D

If the rows of the first rectangle of a decomposition miss s' and those of the second miss s, then the decomposition underlies no hexagon composite with turn rows s and s': one rectangle of a hexagon composite contains both turn rows.

@[reducible, inline]

abbrev TauCeti.GridPentagonPairDecomposition {n : ℕ} (a s b t : Fin n) (x z : GridState n) : Type

A two-step domain consisting of a commutation pentagon followed by a pentagon for the reverse commutation.

@[reducible, inline]

abbrev TauCeti.GridPentagonPairDecomposition.toRectangleDecomposition {n : ℕ} {a s b t : Fin n} {x z : GridState n} (D : GridPentagonPairDecomposition a s b t x z) : GridRectangleDecomposition x z

Forget both turns in a pair of commutation pentagons.

theorem TauCeti.GridPentagonPairDecomposition.toRectangleDecomposition_injective {n : ℕ} {a s b t : Fin n} {x z : GridState n} : Function.Injective toRectangleDecomposition

The underlying rectangle decomposition determines the pentagon pair.

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

The counted commutation hexagons of either turn-side kind.

@[simp]

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

A commutation hexagon is counted exactly when its underlying rectangle is empty and its marking squares avoid every X-marking.

theorem TauCeti.GridDiagram.XSet_inter_coveredSquares_of_mem_commutationHexagons {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y : GridState n} {P : GridCommutationHexagonBetween C.column C.turnRow C.oppositeTurnRow x y} (hP : P ∈ G.commutationHexagons C x y) : G.XSet ∩ P.toGridRectangleBetween.toGridRectangle.coveredSquares = {(P.cutColumn, G.X.toPerm P.cutColumn)}

The rectangle under a counted commutation hexagon carries exactly one X-marking, that of the column the hexagon cuts away.

theorem TauCeti.GridDiagram.cutColumn_X_mem_toGridRectangle_coveredSquares {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y : GridState n} (P : GridCommutationHexagonBetween C.column C.turnRow C.oppositeTurnRow x y) : (P.cutColumn, G.X.toPerm P.cutColumn) ∈ P.toGridRectangleBetween.toGridRectangle.coveredSquares

The rectangle under a commutation hexagon covers the X-marking of the column the hexagon cuts away, whether or not the hexagon is counted.

theorem TauCeti.GridDiagram.mem_commutationHexagons_iff_XSet_inter_eq {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y : GridState n} (P : GridCommutationHexagonBetween C.column C.turnRow C.oppositeTurnRow x y) : P ∈ G.commutationHexagons C x y ↔ P.toGridRectangleBetween.IsEmpty ∧ G.XSet ∩ P.toGridRectangleBetween.toGridRectangle.coveredSquares = {(P.cutColumn, G.X.toPerm P.cutColumn)}

A commutation hexagon is counted exactly when its underlying rectangle is empty and carries exactly one X-marking, that of the column the hexagon cuts away.

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

The counted commutation pentagons of either turn-side kind.

@[simp]

theorem TauCeti.GridDiagram.inl_mem_commutationPentagons {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) : Sum.inl P ∈ G.commutationPentagons C x y ↔ P ∈ G.pentagons C.toColumnTurn x y

A terminal-side commutation pentagon is counted exactly when it is a counted pentagon.

@[simp]

theorem TauCeti.GridDiagram.inr_mem_commutationPentagons {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y : GridState n} (P : GridInitialPentagonBetween C.column C.turnRow x y) : Sum.inr P ∈ G.commutationPentagons C x y ↔ P ∈ G.initialPentagons C.toColumnTurn x y

An initial-side commutation pentagon is counted exactly when it is a counted initial-side pentagon.

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

The weight of a commutation hexagon of either kind.

@[simp]

theorem TauCeti.GridDiagram.commutationHexagonWeight_inl {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x y : GridState n} (P : GridHexagonBetween C.column C.oppositeTurnRow C.turnRow x y) : G.commutationHexagonWeight C R (Sum.inl P) = G.hexagonWeight R P

The weight of a terminal-side commutation hexagon.

@[simp]

theorem TauCeti.GridDiagram.commutationHexagonWeight_inr {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x y : GridState n} (P : GridInitialHexagonBetween C.column C.turnRow C.oppositeTurnRow x y) : G.commutationHexagonWeight C R (Sum.inr P) = G.initialHexagonWeight R P

The weight of an initial-side commutation hexagon.

theorem TauCeti.GridDiagram.commutationHexagonWeight_eq_prod_coveredSquares {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x y : GridState n} (P : GridCommutationHexagonBetween C.column C.turnRow C.oppositeTurnRow x y) : G.commutationHexagonWeight C R P = ∏ p ∈ P.coveredSquares, if p ∈ G.OSet then MvPolynomial.X p.1 else 1

The weight of a commutation hexagon is the product of the per-square O-weights.

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

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

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

The weight of a commutation pentagon of either kind.

@[simp]

theorem TauCeti.GridDiagram.commutationPentagonWeight_inl {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x y : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) : G.commutationPentagonWeight C R (Sum.inl P) = G.pentagonWeight R C.toColumnTurn P

The weight of a terminal-side commutation pentagon.

@[simp]

theorem TauCeti.GridDiagram.commutationPentagonWeight_inr {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x y : GridState n} (P : GridInitialPentagonBetween C.column C.turnRow x y) : G.commutationPentagonWeight C R (Sum.inr P) = G.initialPentagonWeight R C.toColumnTurn P

The weight of an initial-side commutation pentagon.

noncomputable def TauCeti.GridDiagram.hexagonRectangleDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x z : GridState n) : Finset (GridHexagonRectangleDecomposition C.column C.turnRow C.oppositeTurnRow x z)

The hexagon--rectangle decompositions counted in the coefficient of the differential after the commutation homotopy.

@[simp]

theorem TauCeti.GridDiagram.mem_hexagonRectangleDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} (D : GridHexagonRectangleDecomposition C.column C.turnRow C.oppositeTurnRow x z) : D ∈ G.hexagonRectangleDecompositions C x z ↔ D.hexagon ∈ G.commutationHexagons C x D.middle ∧ D.rectangle ∈ G.unblockedRectangles D.middle z

Membership in the counted hexagon--rectangle family is countedness of both domains.

noncomputable def TauCeti.GridDiagram.rectangleHexagonDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x z : GridState n) : Finset (GridRectangleHexagonDecomposition C.column C.turnRow C.oppositeTurnRow x z)

The rectangle--hexagon decompositions counted in the coefficient of the commutation homotopy after the differential.

@[simp]

theorem TauCeti.GridDiagram.mem_rectangleHexagonDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} (D : GridRectangleHexagonDecomposition C.column C.turnRow C.oppositeTurnRow x z) : D ∈ G.rectangleHexagonDecompositions C x z ↔ D.rectangle ∈ G.unblockedRectangles x D.middle ∧ D.hexagon ∈ G.commutationHexagons C D.middle z

Membership in the counted rectangle--hexagon family is countedness of both domains.

noncomputable def TauCeti.GridDiagram.pentagonPairDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x z : GridState n) : Finset (GridPentagonPairDecomposition C.column C.turnRow C.reverse.column C.reverse.turnRow x z)

The pairs of forward and reverse pentagons counted in the round-trip commutation map.

@[simp]

theorem TauCeti.GridDiagram.mem_pentagonPairDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} (D : GridPentagonPairDecomposition C.column C.turnRow C.reverse.column C.reverse.turnRow x z) : D ∈ G.pentagonPairDecompositions C x z ↔ D.first ∈ G.commutationPentagons C x D.middle ∧ D.second ∈ (swapColumns C.column ((finRotate n) C.column) G).commutationPentagons C.reverse D.middle z

Membership in the counted pentagon-pair family is countedness of the forward and reverse pentagons.

theorem TauCeti.GridDiagram.isEmpty_of_mem_pentagonPairDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} {D : GridPentagonPairDecomposition C.column C.turnRow C.reverse.column C.reverse.turnRow x z} (hD : D ∈ G.pentagonPairDecompositions C x z) : D.toRectangleDecomposition.first.IsEmpty ∧ D.toRectangleDecomposition.second.IsEmpty

Both underlying rectangles of a counted pentagon pair are empty.

noncomputable def TauCeti.GridDiagram.hexagonRectangleWeight {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x z : GridState n} (D : GridHexagonRectangleDecomposition C.column C.turnRow C.oppositeTurnRow x z) : MvPolynomial (Fin n) R

The weight of a counted hexagon followed by a rectangle.

theorem TauCeti.GridDiagram.hexagonRectangleWeight_def {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x z : GridState n} (D : GridHexagonRectangleDecomposition C.column C.turnRow C.oppositeTurnRow x z) : G.hexagonRectangleWeight C R D = G.commutationHexagonWeight C R D.hexagon * G.OMonomial R D.rectangle.toGridRectangle

The weight of a hexagon--rectangle decomposition is the product of the two domain weights.

noncomputable def TauCeti.GridDiagram.rectangleHexagonWeight {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x z : GridState n} (D : GridRectangleHexagonDecomposition C.column C.turnRow C.oppositeTurnRow x z) : MvPolynomial (Fin n) R

The weight of a counted rectangle followed by a hexagon.

theorem TauCeti.GridDiagram.rectangleHexagonWeight_def {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x z : GridState n} (D : GridRectangleHexagonDecomposition C.column C.turnRow C.oppositeTurnRow x z) : G.rectangleHexagonWeight C R D = G.OMonomial R D.rectangle.toGridRectangle * G.commutationHexagonWeight C R D.hexagon

The weight of a rectangle--hexagon decomposition is the product of the two domain weights.

The counted hexagon composites

noncomputable def TauCeti.GridDiagram.hexagonCompositeDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x z : GridState n) : Finset (GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z)

The counted hexagon composites from x to z: the counted hexagon--rectangle and rectangle--hexagon decompositions.

@[simp]

theorem TauCeti.GridDiagram.inl_mem_hexagonCompositeDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} (D : GridHexagonRectangleDecomposition C.column C.turnRow C.oppositeTurnRow x z) : Sum.inl D ∈ G.hexagonCompositeDecompositions C x z ↔ D ∈ G.hexagonRectangleDecompositions C x z

A hexagon followed by a rectangle is a counted composite exactly when it is counted as a hexagon--rectangle decomposition.

@[simp]

theorem TauCeti.GridDiagram.inr_mem_hexagonCompositeDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} (D : GridRectangleHexagonDecomposition C.column C.turnRow C.oppositeTurnRow x z) : Sum.inr D ∈ G.hexagonCompositeDecompositions C x z ↔ D ∈ G.rectangleHexagonDecompositions C x z

A rectangle followed by a hexagon is a counted composite exactly when it is counted as a rectangle--hexagon decomposition.

noncomputable def TauCeti.GridDiagram.hexagonCompositeWeight {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x z : GridState n} (D : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z) : MvPolynomial (Fin n) R

The weight of a hexagon composite: that of its hexagon--rectangle or rectangle--hexagon decomposition.

@[simp]

theorem TauCeti.GridDiagram.hexagonCompositeWeight_inl {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x z : GridState n} (D : GridHexagonRectangleDecomposition C.column C.turnRow C.oppositeTurnRow x z) : G.hexagonCompositeWeight C R (Sum.inl D) = G.hexagonRectangleWeight C R D

The weight of a hexagon followed by a rectangle.

@[simp]

theorem TauCeti.GridDiagram.hexagonCompositeWeight_inr {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x z : GridState n} (D : GridRectangleHexagonDecomposition C.column C.turnRow C.oppositeTurnRow x z) : G.hexagonCompositeWeight C R (Sum.inr D) = G.rectangleHexagonWeight C R D

The weight of a rectangle followed by a hexagon.

theorem TauCeti.GridDiagram.isEmpty_of_mem_hexagonCompositeDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} {D : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z} (hD : D ∈ G.hexagonCompositeDecompositions C x z) : D.toRectangleDecomposition.first.IsEmpty ∧ D.toRectangleDecomposition.second.IsEmpty

Both rectangles under a counted composite are empty.

theorem TauCeti.GridDiagram.hexagonCompositeWeight_eq_of_isRepartition {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x z : GridState n} {D E : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z} (hD : D ∈ G.hexagonCompositeDecompositions C x z) (hE : E ∈ G.hexagonCompositeDecompositions C x z) (h : D.toRectangleDecomposition.IsRepartition E.toRectangleDecomposition) : G.hexagonCompositeWeight C R D = G.hexagonCompositeWeight C R E

Two counted composites whose underlying rectangle decompositions repartition the same squares have the same weight.

theorem TauCeti.GridDiagram.injOn_toRectangleDecomposition_hexagonCompositeDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x z : GridState n) : Set.InjOn GridHexagonCompositeDecomposition.toRectangleDecomposition ↑(G.hexagonCompositeDecompositions C x z)

A counted composite is determined by its underlying rectangle decomposition, including the order of its hexagon and rectangle.

noncomputable def TauCeti.GridDiagram.pentagonPairWeight {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x z : GridState n} (D : GridPentagonPairDecomposition C.column C.turnRow C.reverse.column C.reverse.turnRow x z) : MvPolynomial (Fin n) R

The weight of a forward pentagon followed by a reverse pentagon. The first factor is renamed because the forward commutation map is semilinear.

theorem TauCeti.GridDiagram.pentagonPairWeight_def {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x z : GridState n} (D : GridPentagonPairDecomposition C.column C.turnRow C.reverse.column C.reverse.turnRow x z) : G.pentagonPairWeight C R D = (MvPolynomial.rename ⇑(Equiv.swap C.column ((finRotate n) C.column))) (G.commutationPentagonWeight C R D.first) * (swapColumns C.column ((finRotate n) C.column) G).commutationPentagonWeight C.reverse R D.second

The weight of a pentagon pair is the product of the renamed forward weight and the reverse weight.

theorem TauCeti.GridDiagram.commutationHexagonCoefficient_eq_sum_weight {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] (x y : GridState n) : G.commutationHexagonCoefficient R C x y = ∑ P ∈ G.commutationHexagons C x y, G.commutationHexagonWeight C R P

The sum of the two kinds of hexagon coefficients is the sum of their combined weights.

theorem TauCeti.GridDiagram.commutationPentagonCoefficient_eq_sum_weight {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] (x y : GridState n) : G.commutationPentagonCoefficient R C.toColumnTurn x y = ∑ P ∈ G.commutationPentagons C x y, G.commutationPentagonWeight C R P

The sum of the two kinds of pentagon coefficients is the sum of their combined weights.

theorem TauCeti.GridDiagram.sum_commutationHexagonCoefficient_mul_unblockedCoefficient {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] (x z : GridState n) : ∑ y : GridState n, G.commutationHexagonCoefficient R C x y * G.unblockedCoefficient R y z = ∑ D ∈ G.hexagonRectangleDecompositions C x z, G.hexagonRectangleWeight C R D

The hexagon--rectangle matrix product is the sum of the weights of the counted composite domains.

theorem TauCeti.GridDiagram.sum_unblockedCoefficient_mul_commutationHexagonCoefficient {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] (x z : GridState n) : ∑ y : GridState n, G.unblockedCoefficient R x y * G.commutationHexagonCoefficient R C y z = ∑ D ∈ G.rectangleHexagonDecompositions C x z, G.rectangleHexagonWeight C R D

The rectangle--hexagon matrix product is the sum of the weights of the counted composite domains.

theorem TauCeti.GridDiagram.sum_rename_commutationPentagonCoefficient_mul_commutationPentagonCoefficient {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] (x z : GridState n) : ∑ y : GridState n, (MvPolynomial.rename ⇑(Equiv.swap C.column ((finRotate n) C.column))) (G.commutationPentagonCoefficient R C.toColumnTurn x y) * (swapColumns C.column ((finRotate n) C.column) G).commutationPentagonCoefficient R C.reverse.toColumnTurn y z = ∑ D ∈ G.pentagonPairDecompositions C x z, G.pentagonPairWeight C R D

The forward--reverse pentagon matrix product is the sum of the weights of the counted pentagon pairs.

theorem TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_add_eq_iff_decompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] : (∀ (c : GridChainMinus R n), (G.unblockedDifferential R) ((G.commutationHomotopy R C) c) + (G.commutationHomotopy R C) ((G.unblockedDifferential R) c) = c + ((swapColumns C.column ((finRotate n) C.column) G).commutationMap R C.reverse.toColumnTurn) ((G.commutationMap R C.toColumnTurn) c)) ↔ ∀ (x z : GridState n), ∑ D ∈ G.hexagonRectangleDecompositions C x z, G.hexagonRectangleWeight C R D + ∑ D ∈ G.rectangleHexagonDecompositions C x z, G.rectangleHexagonWeight C R D = (if x = z then 1 else 0) + ∑ D ∈ G.pentagonPairDecompositions C x z, G.pentagonPairWeight C R D

The commutation homotopy equation holds exactly when the three finite composite-domain sums satisfy the coefficient identity for every source and target state.