The bigrading of the unblocked grid complex GC⁻

Unblocked.lean builds the unblocked grid complex GC⁻, the free module on grid states over R[V₀, …, V_{n-1}], and records how one rectangle counted by its differential moves the two gradings of a grid state. This file fixes the bigrading those two records were made for and proves that the unblocked differential is homogeneous for it.

The convention is the standard one: a variable V_c sits in O-Maslov degree -2 and Alexander degree -1, so the basis element V^e · x has bidegree

(M_O(x) - 2 |e|, A(x) - |e|)

for |e| the total degree of the exponent vector e. This is OddComponentGridDiagram.monomialBidegree; the Alexander grading is an integer exactly for a diagram with an odd number of link components, which is why the bigraded statements are made for OddComponentGridDiagram, matching Grading/Chain.lean. The underlying grading changes are stated first for an arbitrary grid diagram, in the integer gradings GridDiagram.maslovOℤ and GridDiagram.alexanderTwoℤ, where no hypothesis on the component count is needed; they live here rather than beside their rational counterparts in Unblocked.lean because the integer gradings are not among that file's dependencies.

With that convention the two records of Unblocked.lean say exactly that the unblocked grid differential has bidegree (-1, 0): it drops the O-Maslov grading by one and preserves the Alexander grading. That is the convention the roadmap asks to be fixed once and for all before any grid homology is stated, and it is what makes GC⁻ a bigraded complex rather than merely a module carrying a differential.

The homogeneous piece OddComponentGridDiagram.bigradedChainMinusPiece is a submodule over the coefficient ring R only, not over R[V₀, …, V_{n-1}]: the variables move the bidegree. It consists of the chains all of whose monomials have the given bidegree, and these pieces make GC⁻ an internal direct sum (OddComponentGridDiagram.isInternal_bigradedChainMinusPiece). This is not the decomposition of Grading/Chain.lean, which regroups the basis of grid states of the blocked chain module GridChain R n by bidegree over an arbitrary coefficient ring: over the polynomial ring a basis element is a monomial times a grid state, and its bidegree depends on both, so what is graded here is GC⁻ itself and the pieces are submodules of it.

Forgetting the O-Maslov component gives the Alexander grading of GC⁻ (OddComponentGridDiagram.alexanderChainMinusGrading), an internal grading over R which ∂⁻ preserves and in which each variable V_c has degree -1. This is the grading that descends to the unblocked grid homology GH⁻ and in which the concordance invariant τ is read off.

Main definitions

• TauCeti.OddComponentGridDiagram.monomialBidegree: the bidegree of the basis element V^e · x of GC⁻.
• TauCeti.OddComponentGridDiagram.bigradedChainMinusPiece: the homogeneous piece of GC⁻ in one bidegree.
• TauCeti.OddComponentGridDiagram.bigradedChainMinusGrading: the bundled chain bigrading.
• TauCeti.OddComponentGridDiagram.alexanderChainMinusPiece and TauCeti.OddComponentGridDiagram.alexanderChainMinusGrading: the Alexander-homogeneous pieces of GC⁻ and the internal grading they form.

Main results

• TauCeti.GridDiagram.maslovOℤ_sub_two_mul_card_OColumns and TauCeti.GridDiagram.alexanderTwoℤ_sub_two_mul_card_OColumns: the integer forms of the two grading changes across a rectangle counted by ∂⁻.
• TauCeti.GridDiagram.isWeightedHomogeneous_OMonomial and TauCeti.GridDiagram.isWeightedHomogeneous_unblockedCoefficient: with every variable of weight -2, the weight of an empty rectangle from x to y, and so each matrix coefficient of ∂⁻, is weighted homogeneous of degree M_O(x) - 1 - M_O(y), for any diagram.
• TauCeti.OddComponentGridDiagram.monomialBidegree_add_of_mem_unblockedRectangles: multiplying by the weight of a counted rectangle and moving to its target lowers the bidegree by (1, 0).
• TauCeti.OddComponentGridDiagram.unblockedDifferential_mem_bigradedChainMinusPiece: the unblocked grid differential has bidegree (-1, 0).
• TauCeti.OddComponentGridDiagram.monomial_smul_mem_bigradedChainMinusPiece and TauCeti.OddComponentGridDiagram.X_smul_mem_bigradedChainMinusPiece: the variable V_c has bidegree (-2, -1), and a monomial V^d has bidegree -|d| times (2, 1).
• TauCeti.OddComponentGridDiagram.matrixMap_mem_bigradedChainMinusPiece and TauCeti.OddComponentGridDiagram.matrixMap_mem_alexanderChainMinusPiece: a renamed matrix map whose weighted transitions preserve bidegree or Alexander degree preserves the corresponding homogeneous pieces. More generally, one whose weighted transitions raise the bidegree, or the Alexander degree, by δ raises it by δ on homogeneous chains (TauCeti.OddComponentGridDiagram.matrixMap_mem_bigradedChainMinusPiece_add, TauCeti.OddComponentGridDiagram.matrixMap_mem_alexanderChainMinusPiece_add).
• TauCeti.OddComponentGridDiagram.isInternal_bigradedChainMinusPiece: GC⁻ is the internal direct sum of its homogeneous pieces.
• TauCeti.OddComponentGridDiagram.isHomogeneous_unblockedDifferential_alexanderChainMinusGrading and TauCeti.OddComponentGridDiagram.X_smul_mem_alexanderChainMinusPiece: ∂⁻ preserves the Alexander grading and each variable V_c lowers it by one.

References

This advances TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.3, "The complexes and ∂² = 0", whose unblocked complex GC⁻ this bigrades, and its standing convention "Mind the bigrading bookkeeping", which asks to "fix once whether differentials drop Maslov by 1 and preserve Alexander (unblocked)". The conventions follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.

The integer grading changes across a counted rectangle

theorem TauCeti.GridDiagram.maslovOℤ_sub_two_mul_card_OColumns {n : ℕ} (G : GridDiagram n) {x y : GridState n} {r : GridRectangleBetween x y} (hr : r.IsEmpty) : G.maslovOℤ y - 2 * ↑(G.OColumns r.toGridRectangle).card = G.maslovOℤ x - 1

The integer form of the O-Maslov grading change across an empty rectangle: charging the weight V^{O(r)} with -2 per variable, a rectangle counted by ∂⁻ lowers the integer O-Maslov grading by exactly one.

theorem TauCeti.GridDiagram.alexanderTwoℤ_sub_two_mul_card_OColumns {n : ℕ} (G : GridDiagram n) {x y : GridState n} {r : GridRectangleBetween x y} (hr : Disjoint r.toGridRectangle.coveredSquares G.XSet) : G.alexanderTwoℤ y - 2 * ↑(G.OColumns r.toGridRectangle).card = G.alexanderTwoℤ x

The integer form of the Alexander grading change across a rectangle carrying no X-marking: charging the weight V^{O(r)} with -1 per variable, a rectangle counted by ∂⁻ preserves the Alexander grading, here in its doubled integer form.

theorem TauCeti.GridDiagram.alexanderTwoℤ_eq_add_two_mul_card_sub_card {n : ℕ} (G : GridDiagram n) {x y : GridState n} (r : GridRectangleBetween x y) : G.alexanderTwoℤ y = G.alexanderTwoℤ x + 2 * (↑(G.OColumns r.toGridRectangle).card - ↑(G.XSet ∩ r.toGridRectangle.coveredSquares).card)

The integer form of the Alexander grading change across an arbitrary rectangle: it raises the doubled Alexander grading by twice the difference between the numbers of O- and X-markings it carries.

theorem TauCeti.GridDiagram.alexanderTwoℤ_eq_of_card {n : ℕ} (G : GridDiagram n) {x y : GridState n} {r : GridRectangleBetween x y} {S : Finset (Fin n)} (hO : (G.OColumns r.toGridRectangle).card = S.card + 1) (hX : (G.XSet ∩ r.toGridRectangle.coveredSquares).card = 1) : G.alexanderTwoℤ y = G.alexanderTwoℤ x + 2 * ↑S.card

A rectangle carrying exactly one X-marking and one more O-marking than a set S of columns raises the doubled Alexander grading by twice the size of S.

Maslov homogeneity of the rectangle weights

theorem TauCeti.GridDiagram.isWeightedHomogeneous_OMonomial {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : Type u_1) [CommSemiring R] {r : GridRectangleBetween x y} (hr : r.IsEmpty) : MvPolynomial.IsWeightedHomogeneous (fun (x : Fin n) => -2) (G.OMonomial R r.toGridRectangle) (G.maslovOℤ x - 1 - G.maslovOℤ y)

The weight of an empty rectangle is Maslov homogeneous. Giving every variable the weight -2, the weight V^{O(r)} of an empty rectangle from x to y is weighted homogeneous of degree M_O(x) - 1 - M_O(y): the term V^{O(r)} · y lies one below x in the O-Maslov grading. No condition on the X-markings is needed.

theorem TauCeti.GridDiagram.isWeightedHomogeneous_sum_OMonomial {n : ℕ} (G : GridDiagram n) {x y : GridState n} (R : Type u_1) [CommSemiring R] (s : Finset (GridRectangleBetween x y)) (hs : ∀ r ∈ s, r.IsEmpty) : MvPolynomial.IsWeightedHomogeneous (fun (x : Fin n) => -2) (∑ r ∈ s, G.OMonomial R r.toGridRectangle) (G.maslovOℤ x - 1 - G.maslovOℤ y)

A sum of weights of empty rectangles from x to y, such as a matrix coefficient of the unblocked differential or of an X-marking homotopy, is weighted homogeneous of degree M_O(x) - 1 - M_O(y) when every variable has weight -2.

theorem TauCeti.GridDiagram.isWeightedHomogeneous_unblockedCoefficient {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (x y : GridState n) : MvPolynomial.IsWeightedHomogeneous (fun (x : Fin n) => -2) (G.unblockedCoefficient R x y) (G.maslovOℤ x - 1 - G.maslovOℤ y)

The unblocked differential drops the O-Maslov grading by one, in the form of its matrix coefficients: with every variable of weight -2, the coefficient from x to y is weighted homogeneous of degree M_O(x) - 1 - M_O(y). Unlike the bigraded statements below, this needs no hypothesis on the number of link components.

theorem TauCeti.OddComponentGridDiagram.alexanderℤ_sub_card_OColumns_eq_sub_card {n : ℕ} (G : OddComponentGridDiagram n) {x y : GridState n} (r : GridRectangleBetween x y) : G.alexanderℤ y - ↑((↑G).OColumns r.toGridRectangle).card = G.alexanderℤ x - ↑((↑G).XSet ∩ r.toGridRectangle.coveredSquares).card

The integer Alexander grading change across an arbitrary rectangle: once its weight V^{O(r)} is charged -1 per variable, a rectangle lowers the Alexander grading by the number of X-markings it covers.

theorem TauCeti.OddComponentGridDiagram.alexanderℤ_sub_card_OColumns {n : ℕ} (G : OddComponentGridDiagram n) {x y : GridState n} {r : GridRectangleBetween x y} (hr : Disjoint r.toGridRectangle.coveredSquares (↑G).XSet) : G.alexanderℤ y - ↑((↑G).OColumns r.toGridRectangle).card = G.alexanderℤ x

The integer Alexander grading is unchanged across a rectangle counted by ∂⁻, once its weight V^{O(r)} is charged -1 per variable.

The bidegree of a monomial generator

noncomputable def TauCeti.OddComponentGridDiagram.monomialBidegree {n : ℕ} (G : OddComponentGridDiagram n) (x : GridState n) (e : Fin n →₀ ℕ) : ℤ × ℤ

The bidegree of the basis element V^e · x of the unblocked grid chain module GC⁻.

Each variable V_c sits in O-Maslov degree -2 and Alexander degree -1, so the exponent vector e shifts the bidegree of the grid state x by -|e| times (2, 1), for |e| the total degree of e.

@[simp]

theorem TauCeti.OddComponentGridDiagram.monomialBidegree_fst {n : ℕ} (G : OddComponentGridDiagram n) (x : GridState n) (e : Fin n →₀ ℕ) : (G.monomialBidegree x e).1 = (↑G).maslovOℤ x - 2 * ↑(Finsupp.degree e)

The O-Maslov component of the bidegree of V^e · x.

@[simp]

theorem TauCeti.OddComponentGridDiagram.monomialBidegree_snd {n : ℕ} (G : OddComponentGridDiagram n) (x : GridState n) (e : Fin n →₀ ℕ) : (G.monomialBidegree x e).2 = G.alexanderℤ x - ↑(Finsupp.degree e)

The Alexander component of the bidegree of V^e · x.

theorem TauCeti.OddComponentGridDiagram.monomialBidegree_mapDomain_add_sum_eq_add {n : ℕ} (G : OddComponentGridDiagram n) {x y : GridState n} (G' : OddComponentGridDiagram n) (σ : Equiv.Perm (Fin n)) (d : Fin n →₀ ℕ) (S : Finset (Fin n)) (δ : ℤ × ℤ) (hM : (↑G').maslovOℤ y = (↑G).maslovOℤ x + δ.1 + 2 * ↑S.card) (hA : G'.alexanderℤ y = G.alexanderℤ x + δ.2 + ↑S.card) : G'.monomialBidegree y (Finsupp.mapDomain (⇑σ) d + ∑ c ∈ S, Finsupp.single (σ c) 1) = G.monomialBidegree x d + δ

Renaming the input variables and multiplying by a squarefree weight raises the bidegree by δ when the target state's Maslov and Alexander gradings rise by δ plus twice and once the weight's size.

theorem TauCeti.OddComponentGridDiagram.monomialBidegree_mapDomain_add_sum {n : ℕ} (G : OddComponentGridDiagram n) {x y : GridState n} (G' : OddComponentGridDiagram n) (σ : Equiv.Perm (Fin n)) (d : Fin n →₀ ℕ) (S : Finset (Fin n)) (hM : (↑G').maslovOℤ y = (↑G).maslovOℤ x + 2 * ↑S.card) (hA : G'.alexanderℤ y = G.alexanderℤ x + ↑S.card) : G'.monomialBidegree y (Finsupp.mapDomain (⇑σ) d + ∑ c ∈ S, Finsupp.single (σ c) 1) = G.monomialBidegree x d

Renaming the input variables and multiplying by a squarefree weight preserves bidegree when the target state's Maslov and Alexander gradings rise by twice and once the weight's size.

@[simp]

theorem TauCeti.OddComponentGridDiagram.monomialBidegree_zero {n : ℕ} (G : OddComponentGridDiagram n) (x : GridState n) : G.monomialBidegree x 0 = G.bidegree x

A grid-state generator carries the bidegree of its state.

theorem TauCeti.OddComponentGridDiagram.monomialBidegree_add_of_mem_unblockedRectangles {n : ℕ} (G : OddComponentGridDiagram n) {x y : GridState n} {r : GridRectangleBetween x y} (hr : r ∈ (↑G).unblockedRectangles x y) (e : Fin n →₀ ℕ) : G.monomialBidegree y (e + ∑ c ∈ (↑G).OColumns r.toGridRectangle, Finsupp.single c 1) = G.monomialBidegree x e - (1, 0)

Multiplying the basis element V^e · x by the weight of a rectangle counted by ∂⁻ and passing to the rectangle's target lowers the bidegree by (1, 0). This is the whole content of the statement that ∂⁻ has bidegree (-1, 0).

The homogeneous pieces of GC⁻

def TauCeti.OddComponentGridDiagram.bigradedChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (g : ℤ × ℤ) : Submodule R (GridChainMinus R n)

The homogeneous piece of the unblocked grid chain module GC⁻ in bidegree g: the chains all of whose monomials V^e · x have bidegree g.

The variables move the bidegree, so this is a submodule over the coefficient ring R only, not over R[V₀, …, V_{n-1}].

@[simp]

theorem TauCeti.OddComponentGridDiagram.mem_bigradedChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) {R : Type u_1} [CommSemiring R] {g : ℤ × ℤ} {c : GridChainMinus R n} : c ∈ G.bigradedChainMinusPiece R g ↔ ∀ (x : GridState n), ∀ e ∈ (c x).support, G.monomialBidegree x e = g

A chain of GC⁻ is homogeneous of bidegree g exactly when every monomial occurring in it has bidegree g.

theorem TauCeti.OddComponentGridDiagram.single_monomial_mem_bigradedChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (x : GridState n) (e : Fin n →₀ ℕ) (a : R) : Finsupp.single x ((MvPolynomial.monomial e) a) ∈ G.bigradedChainMinusPiece R (G.monomialBidegree x e)

A monomial multiple of a single grid-state generator is homogeneous of its own bidegree.

theorem TauCeti.OddComponentGridDiagram.single_one_mem_bigradedChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (x : GridState n) : Finsupp.single x 1 ∈ G.bigradedChainMinusPiece R (G.bidegree x)

A grid-state generator of GC⁻ is homogeneous of the bidegree of its state.

theorem TauCeti.OddComponentGridDiagram.unblockedDifferential_mem_bigradedChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) {R : Type u_1} [CommSemiring R] {g : ℤ × ℤ} {c : GridChainMinus R n} (hc : c ∈ G.bigradedChainMinusPiece R g) : ((↑G).unblockedDifferential R) c ∈ G.bigradedChainMinusPiece R (g - (1, 0))

The unblocked grid differential has bidegree (-1, 0): it drops the O-Maslov grading by one and preserves the Alexander grading.

theorem TauCeti.OddComponentGridDiagram.map_unblockedDifferential_bigradedChainMinusPiece_le {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (g : ℤ × ℤ) : Submodule.map (↑R ((↑G).unblockedDifferential R)) (G.bigradedChainMinusPiece R g) ≤ G.bigradedChainMinusPiece R (g - (1, 0))

The unblocked grid differential maps each homogeneous piece of GC⁻ into the piece one lower in the O-Maslov grading.

theorem TauCeti.OddComponentGridDiagram.monomial_smul_mem_bigradedChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) {R : Type u_1} [CommSemiring R] (d : Fin n →₀ ℕ) (a : R) {g : ℤ × ℤ} {c : GridChainMinus R n} (hc : c ∈ G.bigradedChainMinusPiece R g) : (MvPolynomial.monomial d) a • c ∈ G.bigradedChainMinusPiece R (g - (2 * ↑(Finsupp.degree d), ↑(Finsupp.degree d)))

A monomial of the polynomial ring has bidegree -|d| times (2, 1): multiplying a homogeneous chain of GC⁻ by V^d lowers its O-Maslov grading by 2 |d| and its Alexander grading by |d|.

theorem TauCeti.OddComponentGridDiagram.X_smul_mem_bigradedChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) {R : Type u_1} [CommSemiring R] (i : Fin n) {g : ℤ × ℤ} {c : GridChainMinus R n} (hc : c ∈ G.bigradedChainMinusPiece R g) : MvPolynomial.X i • c ∈ G.bigradedChainMinusPiece R (g - (2, 1))

The variable V_c has bidegree (-2, -1): multiplying a homogeneous chain of GC⁻ by a polynomial variable lowers its O-Maslov grading by two and its Alexander grading by one.

theorem TauCeti.OddComponentGridDiagram.X_smul_mem_bigradedChainMinusPiece_iff {n : ℕ} (G : OddComponentGridDiagram n) {R : Type u_1} [CommSemiring R] (i : Fin n) {g : ℤ × ℤ} {c : GridChainMinus R n} : MvPolynomial.X i • c ∈ G.bigradedChainMinusPiece R (g - (2, 1)) ↔ c ∈ G.bigradedChainMinusPiece R g

Multiplication by a variable reflects homogeneity as well as lowering bidegree by (2, 1). No condition on the coefficient semiring is needed.

GC⁻ is the direct sum of its homogeneous pieces

theorem TauCeti.OddComponentGridDiagram.iSup_bigradedChainMinusPiece_eq_top {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] : ⨆ (g : ℤ × ℤ), G.bigradedChainMinusPiece R g = ⊤

The homogeneous pieces of GC⁻ span it: every chain is a finite sum of monomial multiples of grid-state generators.

theorem TauCeti.OddComponentGridDiagram.iSupIndep_bigradedChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] : iSupIndep (G.bigradedChainMinusPiece R)

The homogeneous pieces of GC⁻ are independent: every monomial of a chain has exactly one bidegree.

theorem TauCeti.OddComponentGridDiagram.isInternal_bigradedChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] : DirectSum.IsInternal (G.bigradedChainMinusPiece R)

The unblocked grid chain module is bigraded: GC⁻ is the internal direct sum of its homogeneous pieces.

The coefficient ring is a CommRing here, and not merely a CommSemiring as elsewhere in the file, because independence plus spanning gives an internal direct sum only over a ring (DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top). The grid coefficient rings of interest, ZMod 2 first among them, are rings.

noncomputable def TauCeti.OddComponentGridDiagram.bigradedChainMinusGrading {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] : InternalGrading R (GridChainMinus R n) (ℤ × ℤ)

The internal (O-Maslov, Alexander) grading of the unblocked chain module GC⁻.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedChainMinusGrading_piece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] (g : ℤ × ℤ) : (G.bigradedChainMinusGrading R).piece g = G.bigradedChainMinusPiece R g

The pieces of the bundled chain grading are the bigraded chain pieces.

theorem TauCeti.OddComponentGridDiagram.isHomogeneous_unblockedDifferential_bigradedChainMinusGrading {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] : LinearMap.IsHomogeneous ((↑G).unblockedDifferential R) (G.bigradedChainMinusGrading R).piece (G.bigradedChainMinusGrading R).piece (-(1, 0))

The unblocked grid differential is homogeneous of bidegree (-1, 0).

The Alexander grading of GC⁻

def TauCeti.OddComponentGridDiagram.alexanderChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (a : ℤ) : Submodule R (GridChainMinus R n)

The Alexander-homogeneous piece of the unblocked grid chain module GC⁻ in degree a: the chains all of whose monomials V^e · x have Alexander grading A(x) - |e| = a, whatever their O-Maslov grading. Like the bigraded pieces, it is a submodule over the coefficient ring R only.

@[simp]

theorem TauCeti.OddComponentGridDiagram.mem_alexanderChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) {R : Type u_1} [CommSemiring R] {a : ℤ} {c : GridChainMinus R n} : c ∈ G.alexanderChainMinusPiece R a ↔ ∀ (x : GridState n), ∀ e ∈ (c x).support, G.alexanderℤ x - ↑(Finsupp.degree e) = a

A chain of GC⁻ is Alexander-homogeneous of degree a exactly when every monomial V^e · x occurring in it has Alexander grading A(x) - |e| = a.

theorem TauCeti.OddComponentGridDiagram.bigradedChainMinusPiece_le_alexanderChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (m a : ℤ) : G.bigradedChainMinusPiece R (m, a) ≤ G.alexanderChainMinusPiece R a

A bigraded piece of GC⁻ lies in the Alexander piece of its Alexander degree.

theorem TauCeti.OddComponentGridDiagram.unblockedDifferential_mem_alexanderChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) {R : Type u_1} [CommSemiring R] {a : ℤ} {c : GridChainMinus R n} (hc : c ∈ G.alexanderChainMinusPiece R a) : ((↑G).unblockedDifferential R) c ∈ G.alexanderChainMinusPiece R a

The unblocked grid differential preserves the Alexander grading.

theorem TauCeti.OddComponentGridDiagram.X_smul_mem_alexanderChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) {R : Type u_1} [CommSemiring R] (i : Fin n) {a : ℤ} {c : GridChainMinus R n} (hc : c ∈ G.alexanderChainMinusPiece R a) : MvPolynomial.X i • c ∈ G.alexanderChainMinusPiece R (a - 1)

The variable V_c has Alexander degree -1: multiplying an Alexander-homogeneous chain of GC⁻ by a polynomial variable lowers its Alexander grading by one.

theorem TauCeti.OddComponentGridDiagram.iSup_alexanderChainMinusPiece_eq_top {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] : ⨆ (a : ℤ), G.alexanderChainMinusPiece R a = ⊤

The Alexander pieces of GC⁻ span it.

theorem TauCeti.OddComponentGridDiagram.iSupIndep_alexanderChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] : iSupIndep (G.alexanderChainMinusPiece R)

The Alexander pieces of GC⁻ are independent: every monomial of a chain has exactly one Alexander grading.

def TauCeti.OddComponentGridDiagram.alexanderChainMinusGrading {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] : InternalGrading R (GridChainMinus R n) ℤ

The Alexander grading of GC⁻: the unblocked grid chain module is the internal direct sum of its Alexander pieces, as a module over the coefficient ring R.

@[simp]

theorem TauCeti.OddComponentGridDiagram.alexanderChainMinusGrading_piece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] (a : ℤ) : (G.alexanderChainMinusGrading R).piece ℤ a = G.alexanderChainMinusPiece R a

The degree-a piece of the Alexander grading of GC⁻ is its Alexander piece.

@[simp]

theorem TauCeti.OddComponentGridDiagram.coeff_decompose_alexanderChainMinusGrading {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] (a : ℤ) (c : GridChainMinus R n) (x : GridState n) (e : Fin n →₀ ℕ) : (↑(((DirectSum.decompose ((G.alexanderChainMinusGrading R).piece ℤ)) c) a) x).coeff e = if G.alexanderℤ x - ↑(Finsupp.degree e) = a then (c x).coeff e else 0

The degree-a component of the Alexander grading retains exactly the monomials of Alexander degree a.

theorem TauCeti.OddComponentGridDiagram.isHomogeneous_unblockedDifferential_alexanderChainMinusGrading {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] : LinearMap.IsHomogeneous ((↑G).unblockedDifferential R) ((G.alexanderChainMinusGrading R).piece ℤ) ((G.alexanderChainMinusGrading R).piece ℤ) 0

The unblocked grid differential is homogeneous of degree zero for the Alexander grading.

Grading preservation by renamed matrix maps

theorem TauCeti.OddComponentGridDiagram.matrixMap_mem_bigradedChainMinusPiece_add {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (G' : OddComponentGridDiagram n) (σ : Equiv.Perm (Fin n)) (M : GridState n → GridState n → MvPolynomial (Fin n) R) (f : GridChainMinus R n → GridChainMinus R n) (hf : ∀ (c : GridChainMinus R n) (y : GridState n), (f c) y = Finsupp.sum c fun (x : GridState n) (p : MvPolynomial (Fin n) R) => (MvPolynomial.rename ⇑σ) p * M x y) (δ : ℤ × ℤ) (hδ : ∀ (x y : GridState n), ∀ w ∈ (M x y).support, ∀ (d : Fin n →₀ ℕ), G'.monomialBidegree y (Finsupp.mapDomain (⇑σ) d + w) = G.monomialBidegree x d + δ) {g : ℤ × ℤ} {c : GridChainMinus R n} (hc : c ∈ G.bigradedChainMinusPiece R g) : f c ∈ G'.bigradedChainMinusPiece R (g + δ)

A renamed matrix map whose weighted transitions raise the bidegree by δ sends a chain homogeneous of bidegree g for the source diagram G to a chain of bidegree g + δ for the target diagram G'.

theorem TauCeti.OddComponentGridDiagram.matrixMap_mem_bigradedChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (G' : OddComponentGridDiagram n) (σ : Equiv.Perm (Fin n)) (M : GridState n → GridState n → MvPolynomial (Fin n) R) (f : GridChainMinus R n → GridChainMinus R n) (hf : ∀ (c : GridChainMinus R n) (y : GridState n), (f c) y = Finsupp.sum c fun (x : GridState n) (p : MvPolynomial (Fin n) R) => (MvPolynomial.rename ⇑σ) p * M x y) (hgrade : ∀ (x y : GridState n), ∀ w ∈ (M x y).support, ∀ (d : Fin n →₀ ℕ), G'.monomialBidegree y (Finsupp.mapDomain (⇑σ) d + w) = G.monomialBidegree x d) {g : ℤ × ℤ} {c : GridChainMinus R n} (hc : c ∈ G.bigradedChainMinusPiece R g) : f c ∈ G'.bigradedChainMinusPiece R g

A renamed matrix map whose weighted transitions preserve bidegree sends a chain homogeneous for the source diagram G to a chain of the same bidegree for the target diagram G'.

theorem TauCeti.OddComponentGridDiagram.matrixMap_mem_alexanderChainMinusPiece_add {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (G' : OddComponentGridDiagram n) (σ : Equiv.Perm (Fin n)) (M : GridState n → GridState n → MvPolynomial (Fin n) R) (f : GridChainMinus R n → GridChainMinus R n) (hf : ∀ (c : GridChainMinus R n) (y : GridState n), (f c) y = Finsupp.sum c fun (x : GridState n) (p : MvPolynomial (Fin n) R) => (MvPolynomial.rename ⇑σ) p * M x y) (δ : ℤ) (hAlexander : ∀ (x y : GridState n), ∀ w ∈ (M x y).support, ∀ (d : Fin n →₀ ℕ), (G'.monomialBidegree y (Finsupp.mapDomain (⇑σ) d + w)).2 = (G.monomialBidegree x d).2 + δ) {a : ℤ} {c : GridChainMinus R n} (hc : c ∈ G.alexanderChainMinusPiece R a) : f c ∈ G'.alexanderChainMinusPiece R (a + δ)

A renamed matrix map whose weighted transitions raise the Alexander degree by δ sends an Alexander-homogeneous chain of degree a for G to a chain of Alexander degree a + δ for G'.

theorem TauCeti.OddComponentGridDiagram.matrixMap_mem_alexanderChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (G' : OddComponentGridDiagram n) (σ : Equiv.Perm (Fin n)) (M : GridState n → GridState n → MvPolynomial (Fin n) R) (f : GridChainMinus R n → GridChainMinus R n) (hf : ∀ (c : GridChainMinus R n) (y : GridState n), (f c) y = Finsupp.sum c fun (x : GridState n) (p : MvPolynomial (Fin n) R) => (MvPolynomial.rename ⇑σ) p * M x y) (hAlexander : ∀ (x y : GridState n), ∀ w ∈ (M x y).support, ∀ (d : Fin n →₀ ℕ), (G'.monomialBidegree y (Finsupp.mapDomain (⇑σ) d + w)).2 = (G.monomialBidegree x d).2) {a : ℤ} {c : GridChainMinus R n} (hc : c ∈ G.alexanderChainMinusPiece R a) : f c ∈ G'.alexanderChainMinusPiece R a

A renamed matrix map whose weighted transitions preserve Alexander degree sends an Alexander-homogeneous chain for G to a chain of the same Alexander degree for G'.