The lattice-homology differential over 𝔽₂[U]

This file constructs the first chain complex in the plumbing-lattice lane. For a plumbing graph P and a characteristic covector k, the chain module is freely generated over 𝔽₂[U] by plumbing cubes (x, S). Its differential has two terms for every direction v ∈ S: the lower face and the upper face, multiplied by the powers of U determined by the corresponding drops in the characteristic cube weight.

Applying the differential twice produces the four codimension-two faces for every ordered pair of distinct directions. Reversing the pair reaches the same face with the same total U-exponent by the commuting-face and exponent-square lemmas. Thus every term occurs twice and cancels over 𝔽₂[U].

The coefficient choice is the roadmap's 𝔽₂-first stage. Integral signs form a separate later layer: the unsigned formula here is exactly the characteristic-two reduction of Némethi's oriented cubical differential.

Main definitions

• TauCeti.PlumbingChain: the free 𝔽₂[U]-module on plumbing cubes.
• TauCeti.PlumbingGraph.latticeDifferentialOnGenerator: the weighted boundary of one cube.
• TauCeti.PlumbingGraph.latticeDifferential: the linear lattice differential.

Main results

• TauCeti.PlumbingGraph.latticeDifferential_single: the differential on a basis cube.
• TauCeti.PlumbingGraph.latticeDifferential_single_mk_singleton: the differential on a one-dimensional basis cube.
• TauCeti.PlumbingGraph.latticeDifferential_eq_zero_of_forall_directions_eq_empty: a chain supported on lattice points is a cycle.
• TauCeti.PlumbingGraph.single_add_sub_smul_single_mem_range and TauCeti.PlumbingGraph.single_sub_smul_single_add_mem_range: the boundary relations between adjacent lattice points.
• TauCeti.PlumbingGraph.latticeDifferential_comp_self: the lattice differential squares to zero.
• TauCeti.PlumbingGraph.latticeDifferential_eq_zero_of_isEmpty: the zero-vertex plumbing has zero differential.

References

This advances TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane L ("lattice homology"), which asks for Némethi's lattice homology as a polynomial-module chain complex built from lattice points and weight functions. The face formula follows A. Némethi, arXiv:0709.0841, Section 3.

@[reducible, inline]

abbrev TauCeti.PlumbingCoefficient : Type

The coefficient ring for the first, characteristic-two lattice-homology complex.

Equations

• TauCeti.PlumbingCoefficient = Polynomial (ZMod 2)

@[reducible, inline]

abbrev TauCeti.PlumbingChain (V : Type u_1) : Type u_1

The free 𝔽₂[U]-module generated by plumbing-lattice cubes.

Equations

• TauCeti.PlumbingChain V = (TauCeti.PlumbingCube V →₀ TauCeti.PlumbingCoefficient)

noncomputable def TauCeti.PlumbingGraph.latticeDifferentialOnGenerator {V : Type u_1} [decV : DecidableEq V] [finV : Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (C : PlumbingCube V) : PlumbingChain V

The lattice differential of one plumbing-cube generator.

For every direction of the cube, this is the sum of its lower and upper faces weighted by the drop in characteristic cube weight.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.PlumbingGraph.latticeDifferentialOnGenerator_def {V : Type u_1} [decV : DecidableEq V] [finV : Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (C : PlumbingCube V) : P.latticeDifferentialOnGenerator k C = ∑ v ∈ C.directions.attach, (Finsupp.single (C.lowerFace ↑v ⋯) (Polynomial.X ^ PlumbingCube.characteristicLowerFaceExponent P k C ↑v) + Finsupp.single (C.upperFace ↑v ⋯) (Polynomial.X ^ PlumbingCube.characteristicUpperFaceExponent P k C ⋯))

The defining weighted face-sum formula for the generator differential.

noncomputable def TauCeti.PlumbingGraph.latticeDifferential {V : Type u_1} [decV : DecidableEq V] [finV : Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) : PlumbingChain V →ₗ[PlumbingCoefficient] PlumbingChain V

The 𝔽₂[U]-linear lattice differential on plumbing chains.

Equations

• P.latticeDifferential k = (Finsupp.lsum TauCeti.PlumbingCoefficient) fun (C : TauCeti.PlumbingCube V) => LinearMap.id.smulRight (P.latticeDifferentialOnGenerator k C)

@[simp]

theorem TauCeti.PlumbingGraph.latticeDifferential_single {V : Type u_1} [decV : DecidableEq V] [finV : Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (C : PlumbingCube V) (a : PlumbingCoefficient) : (P.latticeDifferential k) (Finsupp.single C a) = a • P.latticeDifferentialOnGenerator k C

The lattice differential sends a single cube with coefficient a to a times its weighted sum of codimension-one faces.

theorem TauCeti.PlumbingGraph.latticeDifferential_apply {V : Type u_1} [decV : DecidableEq V] [finV : Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (c : PlumbingChain V) : (P.latticeDifferential k) c = Finsupp.sum c fun (C : PlumbingCube V) (a : PlumbingCoefficient) => a • P.latticeDifferentialOnGenerator k C

The lattice differential is the finite linear combination of its values on the generators in the support of a chain.

@[simp]

theorem TauCeti.PlumbingGraph.latticeDifferentialOnGenerator_eq_zero_of_directions_eq_empty {V : Type u_1} [decV : DecidableEq V] [finV : Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {C : PlumbingCube V} (hC : C.directions = ∅) : P.latticeDifferentialOnGenerator k C = 0

A zero-dimensional cube has no directions to differentiate along, so it is a cycle.

theorem TauCeti.PlumbingGraph.latticeDifferential_eq_zero_of_forall_directions_eq_empty {V : Type u_1} [decV : DecidableEq V] [finV : Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {c : PlumbingChain V} (hc : ∀ C ∈ c.support, C.directions = ∅) : (P.latticeDifferential k) c = 0

A chain supported in cubical degree zero is a cycle: a lattice point has no faces.

One-dimensional cubes and adjacent lattice points

theorem TauCeti.PlumbingGraph.latticeDifferential_single_mk_singleton {V : Type u_1} [decV : DecidableEq V] [finV : Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (x : V → ℤ) (v : V) : (P.latticeDifferential k) (Finsupp.single { base := x, directions := {v} } 1) = Finsupp.single { base := x, directions := ∅ } (Polynomial.X ^ (max (P.characteristicWeight k x) (P.characteristicWeight k (x + Pi.single v 1)) - P.characteristicWeight k x).toNat) + Finsupp.single { base := x + Pi.single v 1, directions := ∅ } (Polynomial.X ^ (max (P.characteristicWeight k x) (P.characteristicWeight k (x + Pi.single v 1)) - P.characteristicWeight k (x + Pi.single v 1)).toNat)

The lattice differential of a one-dimensional cube generator: each endpoint appears, weighted by the drop from the cube weight to that endpoint's weight.

theorem TauCeti.PlumbingGraph.single_add_sub_smul_single_mem_range {V : Type u_1} [decV : DecidableEq V] [finV : Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (x : V → ℤ) (v : V) (h : P.characteristicWeight k x ≤ P.characteristicWeight k (x + Pi.single v 1)) : Finsupp.single { base := x + Pi.single v 1, directions := ∅ } 1 - Polynomial.X ^ (P.characteristicWeight k (x + Pi.single v 1) - P.characteristicWeight k x).toNat • Finsupp.single { base := x, directions := ∅ } 1 ∈ (P.latticeDifferential k).range

Crossing a one-dimensional cube towards a lattice point of no smaller weight: the far endpoint is, modulo boundaries, U ^ d times the near one.

theorem TauCeti.PlumbingGraph.single_sub_smul_single_add_mem_range {V : Type u_1} [decV : DecidableEq V] [finV : Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (x : V → ℤ) (v : V) (h : P.characteristicWeight k (x + Pi.single v 1) ≤ P.characteristicWeight k x) : Finsupp.single { base := x, directions := ∅ } 1 - Polynomial.X ^ (P.characteristicWeight k x - P.characteristicWeight k (x + Pi.single v 1)).toNat • Finsupp.single { base := x + Pi.single v 1, directions := ∅ } 1 ∈ (P.latticeDifferential k).range

Crossing a one-dimensional cube away from a lattice point of no larger weight: the near endpoint is, modulo boundaries, U ^ d times the far one.

Cancellation around codimension-two faces

@[simp]

theorem TauCeti.PlumbingGraph.latticeDifferential_latticeDifferentialOnGenerator_eq_zero {V : Type u_1} [decV : DecidableEq V] [finV : Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (C : PlumbingCube V) : (P.latticeDifferential k) (P.latticeDifferentialOnGenerator k C) = 0

The differential of the weighted boundary of a single plumbing cube vanishes.

theorem TauCeti.PlumbingGraph.latticeDifferential_comp_self {V : Type u_1} [decV : DecidableEq V] [finV : Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) : P.latticeDifferential k ∘ₗ P.latticeDifferential k = 0

The characteristic-two weighted lattice differential squares to zero.

@[simp]

theorem TauCeti.PlumbingGraph.latticeDifferential_eq_zero_of_isEmpty {V : Type u_1} [decV : DecidableEq V] [finV : Fintype V] [IsEmpty V] (P : PlumbingGraph V) (k : P.characteristicVectors) : P.latticeDifferential k = 0

The lattice differential vanishes when the plumbing graph has no vertices. Every cube then has an empty direction set, so the weighted face sum on every generator is empty.