The weight filtration on the lattice chain complex

For a characteristic covector k and an integer N, this file restricts Némethi's lattice chain complex to the plumbing cubes whose characteristic cube weight is at most N. The lower and upper faces of such a cube have no larger weight, so the weighted lattice differential preserves this submodule. Restricting in every cubical degree therefore gives a chain complex latticeWeightSublevelComplex P k N.

When the plumbing form is negative definite, every weight sublevel contains only finitely many cubes. Indeed, a cube's base point is one of its vertices and hence has weight at most the cube weight; the possible base points are finite by the properness theorem for the characteristic weight, and the possible direction sets form the finite type Finset V. Consequently every chain group of the restricted complex is a finitely generated 𝔽₂[U]-module.

The inclusions for N ≤ M make these complexes the filtered system whose direct limit is the untruncated lattice complex. That direct limit is constructed in TauCeti.LowDimTopology.Plumbing.Filtration.Colimit; identifying its homology with Némethi's ℍ⁻ is a subsequent step.

Main definitions

• TauCeti.PlumbingGraph.characteristicCubeWeightSublevel: cubes of weight at most N.
• TauCeti.PlumbingChain.supportedCharacteristicWeightSublevel: chains supported on those cubes.
• TauCeti.PlumbingChain.characteristicWeightDegreePart: the weight-≤ N, cubical-degree-q chain group.
• TauCeti.PlumbingGraph.latticeDifferentialWeightDegree: the restricted differential.
• TauCeti.PlumbingGraph.latticeWeightSublevelComplex: the filtered chain complex at level N.
• TauCeti.PlumbingGraph.latticeWeightSublevelInclusion: the inclusion between filtration levels.

References

This advances TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane L, which asks for Némethi's lattice homology from lattice points and weight functions. The filtration by the sublevel cubical complexes is the construction in A. Némethi, arXiv:0709.0841, Section 3.

noncomputable def TauCeti.PlumbingChain.supportedCharacteristicWeightSublevel {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) : Submodule PlumbingCoefficient (PlumbingChain V)

The 𝔽₂[U]-submodule of plumbing chains supported on cubes of weight at most N.

Equations

• TauCeti.PlumbingChain.supportedCharacteristicWeightSublevel P k N = Finsupp.supported TauCeti.PlumbingCoefficient TauCeti.PlumbingCoefficient (P.characteristicCubeWeightSublevel k N)

theorem TauCeti.PlumbingChain.supportedCharacteristicWeightSublevel_def {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) : supportedCharacteristicWeightSublevel P k N = Finsupp.supported PlumbingCoefficient PlumbingCoefficient (P.characteristicCubeWeightSublevel k N)

The chain-level characteristic-weight sublevel is the submodule supported on the corresponding cube sublevel.

@[simp]

theorem TauCeti.PlumbingChain.mem_supportedCharacteristicWeightSublevel {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) (c : PlumbingChain V) : c ∈ supportedCharacteristicWeightSublevel P k N ↔ ∀ C ∈ c.support, PlumbingCube.characteristicWeight P k C ≤ N

A chain belongs to the weight sublevel exactly when every cube in its support has weight at most the level.

theorem TauCeti.PlumbingChain.single_mem_supportedCharacteristicWeightSublevel {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) (C : PlumbingCube V) (a : PlumbingCoefficient) (hC : PlumbingCube.characteristicWeight P k C ≤ N) : Finsupp.single C a ∈ supportedCharacteristicWeightSublevel P k N

A single cube of weight at most N, with any coefficient, belongs to the weight sublevel.

theorem TauCeti.PlumbingChain.supportedCharacteristicWeightSublevel_mono {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {N M : ℤ} (hNM : N ≤ M) : supportedCharacteristicWeightSublevel P k N ≤ supportedCharacteristicWeightSublevel P k M

The chain-level weight submodules increase with the level.

theorem TauCeti.PlumbingChain.exists_mem_supportedCharacteristicWeightSublevel {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (c : PlumbingChain V) : ∃ (N : ℤ), c ∈ supportedCharacteristicWeightSublevel P k N

Every plumbing chain belongs to some weight sublevel.

theorem TauCeti.PlumbingChain.iSup_supportedCharacteristicWeightSublevel_eq_top {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) : ⨆ (N : ℤ), supportedCharacteristicWeightSublevel P k N = ⊤

The weight filtration exhausts the full plumbing chain module.

theorem TauCeti.PlumbingChain.supportedCharacteristicWeightSublevel_fg {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (h : P.IsNegativeDefinite) (k : P.characteristicVectors) (N : ℤ) : (supportedCharacteristicWeightSublevel P k N).FG

On a negative-definite plumbing, each chain-level weight submodule is finitely generated over 𝔽₂[U].

noncomputable def TauCeti.PlumbingChain.characteristicWeightDegreePart {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) (q : ℕ) : Submodule PlumbingCoefficient (PlumbingChain V)

The chains simultaneously lying in cubical degree q and weight at most N.

Equations

• TauCeti.PlumbingChain.characteristicWeightDegreePart P k N q = TauCeti.PlumbingChain.degreePart V q ⊓ TauCeti.PlumbingChain.supportedCharacteristicWeightSublevel P k N

theorem TauCeti.PlumbingChain.characteristicWeightDegreePart_def {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) (q : ℕ) : characteristicWeightDegreePart P k N q = degreePart V q ⊓ supportedCharacteristicWeightSublevel P k N

The filtered degree part is the intersection of the cubical-degree part and the chain-level characteristic-weight sublevel.

theorem TauCeti.PlumbingChain.characteristicWeightDegreePart_le_degreePart {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) (q : ℕ) : characteristicWeightDegreePart P k N q ≤ degreePart V q

A filtered degree part lies in the corresponding unfiltered cubical-degree part.

theorem TauCeti.PlumbingChain.characteristicWeightDegreePart_le_supportedCharacteristicWeightSublevel {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) (q : ℕ) : characteristicWeightDegreePart P k N q ≤ supportedCharacteristicWeightSublevel P k N

A filtered degree part lies in the corresponding chain-level characteristic-weight sublevel.

@[simp]

theorem TauCeti.PlumbingChain.mem_characteristicWeightDegreePart {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) (q : ℕ) (c : PlumbingChain V) : c ∈ characteristicWeightDegreePart P k N q ↔ ∀ C ∈ c.support, C.dimension = q ∧ PlumbingCube.characteristicWeight P k C ≤ N

Membership in a weight-graded chain group means that every support cube has the specified cubical dimension and weight at most the level.

theorem TauCeti.PlumbingChain.characteristicWeightDegreePart_eq_supported {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) (q : ℕ) : characteristicWeightDegreePart P k N q = Finsupp.supported PlumbingCoefficient PlumbingCoefficient {C : PlumbingCube V | C.dimension = q ∧ PlumbingCube.characteristicWeight P k C ≤ N}

A filtered degree part is the submodule supported on cubes having the prescribed dimension and characteristic-weight bound.

theorem TauCeti.PlumbingChain.single_mem_characteristicWeightDegreePart {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) (q : ℕ) (C : PlumbingCube V) (a : PlumbingCoefficient) (hdim : C.dimension = q) (hweight : PlumbingCube.characteristicWeight P k C ≤ N) : Finsupp.single C a ∈ characteristicWeightDegreePart P k N q

A basis cube of dimension q and weight at most N belongs to the corresponding filtered chain group.

theorem TauCeti.PlumbingChain.characteristicWeightDegreePart_mono {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {N M : ℤ} (hNM : N ≤ M) (q : ℕ) : characteristicWeightDegreePart P k N q ≤ characteristicWeightDegreePart P k M q

Filtered cubical-degree chain groups increase with the weight level.

theorem TauCeti.PlumbingChain.iSup_characteristicWeightDegreePart_eq_degreePart {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (q : ℕ) : ⨆ (N : ℤ), characteristicWeightDegreePart P k N q = degreePart V q

In a fixed cubical degree, the weight filtration exhausts the full degree submodule.

theorem TauCeti.PlumbingChain.characteristicWeightDegreePart_fg {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (h : P.IsNegativeDefinite) (k : P.characteristicVectors) (N : ℤ) (q : ℕ) : (characteristicWeightDegreePart P k N q).FG

On a negative-definite plumbing, every filtered cubical-degree chain group is finitely generated over 𝔽₂[U].

theorem TauCeti.PlumbingGraph.latticeDifferentialOnGenerator_mem_supportedCharacteristicWeightSublevel {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {N : ℤ} (C : PlumbingCube V) (hC : PlumbingCube.characteristicWeight P k C ≤ N) : P.latticeDifferentialOnGenerator k C ∈ PlumbingChain.supportedCharacteristicWeightSublevel P k N

The differential of a cube in a weight sublevel is supported in the same sublevel.

theorem TauCeti.PlumbingGraph.latticeDifferential_mem_supportedCharacteristicWeightSublevel {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {N : ℤ} {c : PlumbingChain V} (hc : c ∈ PlumbingChain.supportedCharacteristicWeightSublevel P k N) : (P.latticeDifferential k) c ∈ PlumbingChain.supportedCharacteristicWeightSublevel P k N

The lattice differential preserves every chain-level weight submodule.

theorem TauCeti.PlumbingGraph.latticeDifferential_mem_characteristicWeightDegreePart {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {N : ℤ} {q : ℕ} {c : PlumbingChain V} (hc : c ∈ PlumbingChain.characteristicWeightDegreePart P k N (q + 1)) : (P.latticeDifferential k) c ∈ PlumbingChain.characteristicWeightDegreePart P k N q

The lattice differential sends filtered chains of cubical degree q + 1 to filtered chains of cubical degree q.

noncomputable def TauCeti.PlumbingGraph.latticeDifferentialWeightDegree {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) (q : ℕ) : ↥(PlumbingChain.characteristicWeightDegreePart P k N (q + 1)) →ₗ[PlumbingCoefficient] ↥(PlumbingChain.characteristicWeightDegreePart P k N q)

The lattice differential restricted to consecutive cubical degrees inside one weight sublevel.

Equations

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

@[simp]

theorem TauCeti.PlumbingGraph.latticeDifferentialWeightDegree_apply {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) (q : ℕ) (c : ↥(PlumbingChain.characteristicWeightDegreePart P k N (q + 1))) : ↑((P.latticeDifferentialWeightDegree k N q) c) = (P.latticeDifferential k) ↑c

Forgetting the submodule wrappers, the filtered differential is the total lattice differential.

theorem TauCeti.PlumbingGraph.latticeDifferentialWeightDegree_comp {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) (q : ℕ) : P.latticeDifferentialWeightDegree k N q ∘ₗ P.latticeDifferentialWeightDegree k N (q + 1) = 0

Two consecutive differentials in a weight sublevel compose to zero.

theorem TauCeti.PlumbingGraph.latticeDifferentialWeightDegree_comp_inclusion {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {N M : ℤ} (hNM : N ≤ M) (q : ℕ) : P.latticeDifferentialWeightDegree k M q ∘ₗ Submodule.inclusion ⋯ = Submodule.inclusion ⋯ ∘ₗ P.latticeDifferentialWeightDegree k N q

Increasing the weight level commutes with the restricted lattice differential.

theorem TauCeti.PlumbingGraph.latticeDifferentialDegree_comp_inclusion {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) (q : ℕ) : P.latticeDifferentialDegree k q ∘ₗ Submodule.inclusion ⋯ = Submodule.inclusion ⋯ ∘ₗ P.latticeDifferentialWeightDegree k N q

The full lattice differential after including a weight sublevel agrees with first applying the restricted differential and then including the result into the full degree part.

noncomputable def TauCeti.PlumbingGraph.latticeWeightSublevelComplex {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) : ChainComplex (ModuleCat PlumbingCoefficient) ℕ

The cubically graded lattice chain complex restricted to cubes of characteristic weight at most N.

Equations

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

@[simp]

theorem TauCeti.PlumbingGraph.latticeWeightSublevelComplex_X {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) (q : ℕ) : (P.latticeWeightSublevelComplex k N).X q = ModuleCat.of PlumbingCoefficient ↥(PlumbingChain.characteristicWeightDegreePart P k N q)

The degree-q object of the weight-sublevel complex is the corresponding filtered cubical-degree chain group.

@[simp]

theorem TauCeti.PlumbingGraph.latticeWeightSublevelComplex_d {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) (q : ℕ) : (P.latticeWeightSublevelComplex k N).d (q + 1) q = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (P.latticeDifferentialWeightDegree k N q)) (CategoryTheory.eqToHom ⋯))

The differential of the weight-sublevel complex is the restricted lattice differential.

noncomputable def TauCeti.PlumbingGraph.latticeWeightSublevelInclusion {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {N M : ℤ} (hNM : N ≤ M) : P.latticeWeightSublevelComplex k N ⟶ P.latticeWeightSublevelComplex k M

The chain-complex inclusion from weight level N to a larger level M.

Equations

• P.latticeWeightSublevelInclusion k hNM = ChainComplex.ofHom (fun (q : ℕ) => ModuleCat.ofHom (Submodule.inclusion ⋯)) ⋯

theorem TauCeti.PlumbingGraph.latticeWeightSublevelInclusion_f {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {N M : ℤ} (hNM : N ≤ M) (q : ℕ) : (P.latticeWeightSublevelInclusion k hNM).f q = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Submodule.inclusion ⋯)) (CategoryTheory.eqToHom ⋯))

The component of a weight-sublevel inclusion is the corresponding submodule inclusion of filtered degree parts.

@[simp]

theorem TauCeti.PlumbingGraph.latticeWeightSublevelInclusion_apply {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {N M : ℤ} (hNM : N ≤ M) (q : ℕ) (c : ↑((P.latticeWeightSublevelComplex k N).X q)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((P.latticeWeightSublevelInclusion k hNM).f q)) c) = (CategoryTheory.ConcreteCategory.hom (ModuleCat.ofHom (Submodule.inclusion ⋯))) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) c)

A weight-sublevel complex inclusion does not change the underlying filtered chain.

@[simp]

theorem TauCeti.PlumbingGraph.latticeWeightSublevelInclusion_id {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) : P.latticeWeightSublevelInclusion k ⋯ = CategoryTheory.CategoryStruct.id (P.latticeWeightSublevelComplex k N)

The weight-sublevel inclusion from a level to itself is the identity chain map.

@[simp]

theorem TauCeti.PlumbingGraph.latticeWeightSublevelInclusion_comp {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {N M L : ℤ} (hNM : N ≤ M) (hML : M ≤ L) : CategoryTheory.CategoryStruct.comp (P.latticeWeightSublevelInclusion k hNM) (P.latticeWeightSublevelInclusion k hML) = P.latticeWeightSublevelInclusion k ⋯

Weight-sublevel inclusions compose to the inclusion between the outer levels.

noncomputable def TauCeti.PlumbingGraph.latticeWeightSublevelFunctor {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) : CategoryTheory.Functor ℤ (ChainComplex (ModuleCat PlumbingCoefficient) ℕ)

The characteristic-weight sublevel complexes and their canonical inclusions, as a filtered diagram indexed by the ordered set of integers.

Equations

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

@[simp]

theorem TauCeti.PlumbingGraph.latticeWeightSublevelFunctor_obj {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) (N : ℤ) : (P.latticeWeightSublevelFunctor k).obj N = P.latticeWeightSublevelComplex k N

The object at level N in the characteristic-weight filtration diagram is the corresponding weight-sublevel complex.

@[simp]

theorem TauCeti.PlumbingGraph.latticeWeightSublevelFunctor_map {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) {N M : ℤ} (f : N ⟶ M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((P.latticeWeightSublevelFunctor k).map f) (CategoryTheory.eqToHom ⋯)) = P.latticeWeightSublevelInclusion k ⋯

The map in the characteristic-weight filtration diagram is the canonical inclusion between the corresponding weight-sublevel complexes.