Face weights for plumbing-lattice cubes

This file adds the codimension-one face bookkeeping needed for the cubical boundary in Némethi's lattice homology. A cube with base point x and directions S has two faces in a direction v: the lower face with the same base point and directions S.erase v, and the upper face with base point x + E_v and directions S.erase v.

The cube weight is the maximum of the point weights over all vertices, so each face weight is bounded above by the ambient cube weight. The resulting nonnegative differences are the exponents of the U-powers in the later lattice-homology differential.

Main results

• TauCeti.PlumbingGraph.cubeVertices_upperFace_subset: the upper face's vertices are vertices of the ambient cube, when v ∈ S.
• TauCeti.PlumbingGraph.characteristicUpperFaceWeight_le: the upper face weight is bounded by the ambient cube weight.
• TauCeti.PlumbingGraph.characteristicLowerFaceExponent and TauCeti.PlumbingGraph.characteristicUpperFaceExponent: the corresponding natural-number weight differences.

References

This supplies a prerequisite for TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane L ("lattice homology"), whose opening item asks for Némethi's lattice (co)homology from lattice points and weight functions. The face-weight exponents are the standard cubical-boundary weights in Némethi, arXiv:0709.0841.

theorem TauCeti.PlumbingGraph.cubeVertices_upperFace_subset {V : Type u_1} [DecidableEq V] [DecidableEq (V → ℤ)] {x : V → ℤ} {S : Finset V} {v : V} (hv : v ∈ S) : cubeVertices (x + Pi.single v 1) (S.erase v) ⊆ cubeVertices x S

The upper face in a direction has its vertices among the vertices of the ambient cube.

theorem TauCeti.PlumbingGraph.characteristicUpperFaceWeight_le {V : Type u_1} [DecidableEq V] [DecidableEq (V → ℤ)] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {x : V → ℤ} {S : Finset V} {v : V} (hv : v ∈ S) : P.characteristicCubeWeight k (x + Pi.single v 1) (S.erase v) ≤ P.characteristicCubeWeight k x S

The upper face's characteristic cube weight is bounded by the ambient cube weight.

noncomputable def TauCeti.PlumbingGraph.characteristicLowerFaceExponent {V : Type u_1} [DecidableEq V] [DecidableEq (V → ℤ)] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (x : V → ℤ) (S : Finset V) (v : V) : ℕ

The nonnegative U-exponent contributed by the lower face in a cube direction.

Equations

• P.characteristicLowerFaceExponent k x S v = (P.characteristicCubeWeight k x S - P.characteristicCubeWeight k x (S.erase v)).toNat

@[simp]

theorem TauCeti.PlumbingGraph.characteristicLowerFaceExponent_natCast {V : Type u_1} [DecidableEq V] [DecidableEq (V → ℤ)] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {x : V → ℤ} {S : Finset V} {v : V} : ↑(P.characteristicLowerFaceExponent k x S v) = P.characteristicCubeWeight k x S - P.characteristicCubeWeight k x (S.erase v)

The lower-face exponent, cast back to ℤ, is the difference between the ambient cube weight and the lower face weight.

theorem TauCeti.PlumbingGraph.characteristicLowerFaceExponent_eq_zero_iff {V : Type u_1} [DecidableEq V] [DecidableEq (V → ℤ)] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {x : V → ℤ} {S : Finset V} {v : V} : P.characteristicLowerFaceExponent k x S v = 0 ↔ P.characteristicCubeWeight k x S = P.characteristicCubeWeight k x (S.erase v)

The lower-face exponent is zero exactly when the lower face has the same weight as the ambient cube.

noncomputable def TauCeti.PlumbingGraph.characteristicUpperFaceExponent {V : Type u_1} [DecidableEq V] [DecidableEq (V → ℤ)] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (x : V → ℤ) (S : Finset V) {v : V} (_hv : v ∈ S) : ℕ

The nonnegative U-exponent contributed by the upper face in a direction.

Equations

• P.characteristicUpperFaceExponent k x S _hv = (P.characteristicCubeWeight k x S - P.characteristicCubeWeight k (x + Pi.single v 1) (S.erase v)).toNat

@[simp]

theorem TauCeti.PlumbingGraph.characteristicUpperFaceExponent_natCast {V : Type u_1} [DecidableEq V] [DecidableEq (V → ℤ)] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {x : V → ℤ} {S : Finset V} {v : V} (hv : v ∈ S) : ↑(P.characteristicUpperFaceExponent k x S hv) = P.characteristicCubeWeight k x S - P.characteristicCubeWeight k (x + Pi.single v 1) (S.erase v)

The upper-face exponent, cast back to ℤ, is the difference between the ambient cube weight and the upper face weight.

theorem TauCeti.PlumbingGraph.characteristicUpperFaceExponent_eq_zero_iff {V : Type u_1} [DecidableEq V] [DecidableEq (V → ℤ)] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {x : V → ℤ} {S : Finset V} {v : V} (hv : v ∈ S) : P.characteristicUpperFaceExponent k x S hv = 0 ↔ P.characteristicCubeWeight k x S = P.characteristicCubeWeight k (x + Pi.single v 1) (S.erase v)

The upper-face exponent is zero exactly when the upper face has the same weight as the ambient cube.