The bigraded grid chain module

This file turns the integer O-Maslov and Alexander gradings of a grid diagram with odd component count into a direct-sum decomposition of the grid chain module. The summand in bidegree (m, a) is the direct sum of one copy of the coefficient ring for each state with O-Maslov grading m and Alexander grading a.

The decomposition groups the standard basis through Mathlib's linear direct-sum reindexing and sigma-currying equivalences; no second direct-sum or graded-module framework is introduced.

Main definitions

• TauCeti.OddComponentGridDiagram.BigradedChainPiece: the homogeneous grid-chain module in one bidegree.
• TauCeti.OddComponentGridDiagram.bigradedChainEquiv: the grid chain module as the direct sum of its homogeneous pieces.
• TauCeti.OddComponentGridDiagram.bigradedChainInclusion and TauCeti.OddComponentGridDiagram.bigradedChainProjection: inclusion and projection of a piece.

Main results

• TauCeti.OddComponentGridDiagram.bigradedChainEquiv_single: a state generator lies in its own bidegree.
• TauCeti.OddComponentGridDiagram.finrank_bigradedChainPiece: the rank of a homogeneous piece is the number of states in that bidegree.
• TauCeti.OddComponentGridDiagram.sum_finrank_bigradedChainPiece: the ranks of the occupied pieces add to n!.
• TauCeti.OddComponentGridDiagram.map_bigradedChainInclusion_bigradedChainProjection: a linear map shifting the bidegree of every generator by r sends homogeneous parts of bidegree g to homogeneous parts of bidegree g + r.

References

This advances TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.3, by giving the grid chain module its missing bigraded decomposition. It is also the algebraic input for Lane G.4, where the Alexander-graded Euler characteristic is compared with the grid determinant. The grading conventions follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.

@[reducible, inline]

abbrev TauCeti.OddComponentGridDiagram.BigradedChainPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] (g : ℤ × ℤ) : Type u_1

The homogeneous grid-chain module in bidegree g: one copy of R for each state of that bidegree.

noncomputable def TauCeti.OddComponentGridDiagram.bigradedChainEquiv {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] : GridChain R n ≃ₗ[R] DirectSum (ℤ × ℤ) fun (g : ℤ × ℤ) => G.BigradedChainPiece R g

The grid chain module decomposed as the direct sum of its (O-Maslov, Alexander)-homogeneous pieces.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedChainEquiv_apply_apply {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] (c : GridChain R n) (g : ℤ × ℤ) (x : { x : GridState n // G.bidegree x = g }) : (((G.bigradedChainEquiv R) c) g) x = c ↑x

In the bigraded decomposition, the coefficient at a state in degree g is its original grid chain coefficient.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedChainEquiv_symm_apply_apply {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] (d : DirectSum (ℤ × ℤ) fun (g : ℤ × ℤ) => G.BigradedChainPiece R g) (x : GridState n) : ((G.bigradedChainEquiv R).symm d) x = (d (G.bidegree x)) ⟨x, ⋯⟩

Reading a chain back off its homogeneous components: the coefficient at a state is the component of the state's own bidegree, at that state.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedChainEquiv_single {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] (x : GridState n) (r : R) : (G.bigradedChainEquiv R) (Finsupp.single x r) = (DirectSum.lof R (ℤ × ℤ) (fun (g : ℤ × ℤ) => G.BigradedChainPiece R g) (G.bidegree x)) ((DirectSum.lof R { y : GridState n // G.bidegree y = G.bidegree x } (fun (x : { y : GridState n // G.bidegree y = G.bidegree x }) => R) ⟨x, ⋯⟩) r)

A grid-state generator maps to the copy of the coefficient ring indexed by that state inside its own bidegree.

noncomputable def TauCeti.OddComponentGridDiagram.bigradedChainInclusion {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] (g : ℤ × ℤ) : G.BigradedChainPiece R g →ₗ[R] GridChain R n

Include a homogeneous grid-chain piece into the total grid chain module.

noncomputable def TauCeti.OddComponentGridDiagram.bigradedChainProjection {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] (g : ℤ × ℤ) : GridChain R n →ₗ[R] G.BigradedChainPiece R g

Project a grid chain onto one homogeneous piece.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedChainProjection_apply {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] (g : ℤ × ℤ) (c : GridChain R n) (x : { x : GridState n // G.bidegree x = g }) : ((G.bigradedChainProjection R g) c) x = c ↑x

Homogeneous projection retains the coefficients of states of the specified bidegree.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedChainInclusion_apply {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] (g : ℤ × ℤ) (c : G.BigradedChainPiece R g) (x : GridState n) : ((G.bigradedChainInclusion R g) c) x = if h : G.bidegree x = g then c ⟨x, h⟩ else 0

Inclusion extends the coefficients of a homogeneous chain by zero.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedChainProjection_bigradedChainInclusion {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] (g : ℤ × ℤ) (c : G.BigradedChainPiece R g) : (G.bigradedChainProjection R g) ((G.bigradedChainInclusion R g) c) = c

Projection is a left inverse to the inclusion of the same homogeneous piece.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedChainProjection_bigradedChainInclusion_of_ne {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] {g g' : ℤ × ℤ} (h : g ≠ g') (c : G.BigradedChainPiece R g') : (G.bigradedChainProjection R g) ((G.bigradedChainInclusion R g') c) = 0

Projection onto a different bidegree annihilates a homogeneous inclusion.

theorem TauCeti.OddComponentGridDiagram.bigradedChainInclusion_injective {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] (g : ℤ × ℤ) : Function.Injective ⇑(G.bigradedChainInclusion R g)

Inclusion of a homogeneous piece is injective.

theorem TauCeti.OddComponentGridDiagram.finrank_bigradedChainPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] [StrongRankCondition R] (g : ℤ × ℤ) : Module.finrank R (G.BigradedChainPiece R g) = {x : GridState n | G.bidegree x = g}.card

The rank of a homogeneous grid-chain piece is the number of states in its bidegree.

theorem TauCeti.OddComponentGridDiagram.finrank_bigradedChainPiece_pos_iff {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] [StrongRankCondition R] (g : ℤ × ℤ) : 0 < Module.finrank R (G.BigradedChainPiece R g) ↔ g ∈ G.bidegreeSupport

A homogeneous grid-chain piece has positive rank exactly when its bidegree is occupied by a grid state.

theorem TauCeti.OddComponentGridDiagram.sum_finrank_bigradedChainPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] [StrongRankCondition R] : ∑ g ∈ G.bidegreeSupport, Module.finrank R (G.BigradedChainPiece R g) = n.factorial

The ranks of all occupied homogeneous pieces add to n!, the number of grid states.

Homogeneous parts of chains

theorem TauCeti.OddComponentGridDiagram.bigradedChainInclusion_bigradedChainProjection_single {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] (g : ℤ × ℤ) (x : GridState n) (a : R) : (G.bigradedChainInclusion R g) ((G.bigradedChainProjection R g) (Finsupp.single x a)) = if G.bidegree x = g then Finsupp.single x a else 0

The homogeneous part of bidegree g of a state generator is the generator itself when the state has bidegree g, and zero otherwise.

theorem TauCeti.OddComponentGridDiagram.map_bigradedChainInclusion_bigradedChainProjection {n : ℕ} (G : OddComponentGridDiagram n) {m : ℕ} (G' : OddComponentGridDiagram m) {R : Type u_1} [Semiring R] (f : GridChain R n →ₗ[R] GridChain R m) (r : ℤ × ℤ) (hf : ∀ (x : GridState n) (y : GridState m), G'.bidegree y ≠ G.bidegree x + r → (f (Finsupp.single x 1)) y = 0) (g : ℤ × ℤ) (c : GridChain R n) : f ((G.bigradedChainInclusion R g) ((G.bigradedChainProjection R g) c)) = (G'.bigradedChainInclusion R (g + r)) ((G'.bigradedChainProjection R (g + r)) (f c))

A linear map of grid chain modules that shifts the bidegree of every state generator by r commutes with taking homogeneous parts: it sends the part of bidegree g of a chain to the part of bidegree g + r of the image.