Documentation

TauCeti.LowDimTopology.Plumbing.Weight.Sublevel

Sublevel sets of the plumbing-lattice weight function #

Némethi builds lattice homology out of the sublevel sets S_c = {x | χ_k(x) ≤ c} of the characteristic weight function of a negative-definite plumbing: the lattice complex is filtered by them, and the invariants read off from that filtration — including the d-invariant analogues — only make sense because each S_c is a finite set of lattice points and because χ_k attains a minimum. This file proves both facts.

The mechanism is completing the square. Write A for the intersection matrix, d = det A, and u = adjugate A *ᵥ k, so that A *ᵥ u = d • k and hence A(x, u) = d ⟪k, x⟫. Expanding the self-pairing of 2d • x + u therefore gives

A(2d • x + u, 2d • x + u) = 4 d² (⟪k, x⟫ + A(x, x)) + A(u, u),

whose middle factor ⟪k, x⟫ + A(x, x) is exactly the weight numerator characteristicWeightNumerator k x, which is -2 χ_k(x). So a sublevel set of χ_k is carried, by the injective affine map x ↦ 2d • x + u, into a superlevel set of the intersection-form self-pairing, and those are finite on a negative-definite plumbing by IsNegativeDefinite.finite_setOfPred_le_intersectionForm_self. Negative-definiteness enters twice: it makes d ≠ 0, so the affine map is injective, and it makes the target set finite.

Finiteness immediately yields a minimizer: the lattice points with χ_k(x) ≤ χ_k(0) form a finite nonempty set, and a minimum over it is a global minimum. That minimum is the numerical input to the d-invariant of the plumbed three-manifold in the spin^c structure recorded by k, and it transforms under the two moves that change the representative k of a spin^c structure: passing to k + 2 · A m shifts it by -χ_k(m), and spin^c conjugation leaves it fixed.

Main results #

References #

This advances TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane L ("lattice homology"), whose target is "Némethi's lattice (co)homology ℍ⁻/ℍ⁰ as a ℤ[U]-module from lattice points and weight functions … and d-invariant analogues": the sublevel sets treated here are the ones that filtration is taken over. See Némethi, arXiv:0709.0841, after Ozsváth--Szabó, arXiv:math/0203265.

source
theorem TauCeti.PlumbingGraph.finite_setOfPred_le_characteristicWeightNumerator {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (h : P.IsNegativeDefinite) (k : V → ℤ) (c : ℤ) :
{x : V → ℤ | c ≤ P.characteristicWeightNumerator k x}.Finite

On a negative-definite plumbing only finitely many lattice points have characteristic-weight numerator above a fixed bound.

The affine map x ↦ 2 (det A) • x + adjugate A *ᵥ k is injective because negative-definiteness forces det A ≠ 0, and by the completed square it carries the superlevel set into a superlevel set of the intersection-form self-pairing, which is finite.

source
theorem TauCeti.PlumbingGraph.finite_setOfPred_characteristicWeight_le {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (h : P.IsNegativeDefinite) (k : P.characteristicVectors) (N : ℤ) :
{x : V → ℤ | P.characteristicWeight k x ≤ N}.Finite

On a negative-definite plumbing every sublevel set of the characteristic weight function is finite: only finitely many lattice points satisfy χ_k(x) ≤ N.

This is the finiteness that makes Némethi's filtration of the lattice complex by weight sublevel sets a filtration by finitely generated pieces.

source
theorem TauCeti.PlumbingGraph.exists_forall_characteristicWeight_le {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (h : P.IsNegativeDefinite) (k : P.characteristicVectors) :
∃ (x₀ : V → ℤ), ∀ (x : V → ℤ), P.characteristicWeight k x₀ ≤ P.characteristicWeight k x

On a negative-definite plumbing the characteristic weight function attains a global minimum.

The lattice points with χ_k(x) ≤ χ_k(0) form a finite nonempty set, and a point minimizing χ_k over it minimizes χ_k everywhere. The value at such a point is the numerical input to the d-invariant of the plumbed three-manifold in the spin^c structure recorded by k.

source
theorem TauCeti.PlumbingGraph.bddBelow_range_characteristicWeight {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (h : P.IsNegativeDefinite) (k : P.characteristicVectors) :
BddBelow (Set.range (P.characteristicWeight k))

On a negative-definite plumbing the characteristic weight function is bounded below.

source
noncomputable def TauCeti.PlumbingGraph.sInfCharacteristicWeight {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) :
ℤ

The infimum of the characteristic weight function, as an integer.

On a negative-definite plumbing this is a genuine minimum — sInfCharacteristicWeight_le bounds the weight below by it and exists_characteristicWeight_eq_sInfCharacteristicWeight attains it — and it is the numerical input to the d-invariant of the plumbed three-manifold in the spin^c structure recorded by k. Without negative-definiteness the range need not be bounded below and the value is the junk value 0 of Int.csInf_of_not_bddBelow, which is why the name records the infimum rather than a minimum.

Equations
Instances For
    source
    theorem TauCeti.PlumbingGraph.sInfCharacteristicWeight_def {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) :
    P.sInfCharacteristicWeight k = sInf (Set.range (P.characteristicWeight k))

    The infimum of the characteristic weight, as the infimum of its range.

    source
    theorem TauCeti.PlumbingGraph.le_sInfCharacteristicWeight {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) {c : ℤ} (k : P.characteristicVectors) (hc : ∀ (x : V → ℤ), c ≤ P.characteristicWeight k x) :
    c ≤ P.sInfCharacteristicWeight k

    The greatest-lower-bound rule for the infimum of the characteristic weight: any lower bound for the weight is a lower bound for the infimum. No hypothesis on the plumbing is needed, since the range is nonempty.

    source
    theorem TauCeti.PlumbingGraph.sInfCharacteristicWeight_le {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (h : P.IsNegativeDefinite) (k : P.characteristicVectors) (x : V → ℤ) :
    P.sInfCharacteristicWeight k ≤ P.characteristicWeight k x

    On a negative-definite plumbing the infimum of the characteristic weight is a lower bound for the characteristic weight.

    source
    theorem TauCeti.PlumbingGraph.exists_characteristicWeight_eq_sInfCharacteristicWeight {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (h : P.IsNegativeDefinite) (k : P.characteristicVectors) :
    ∃ (x : V → ℤ), P.characteristicWeight k x = P.sInfCharacteristicWeight k

    On a negative-definite plumbing the infimum of the characteristic weight is attained: some lattice point has that exact weight, so it is a minimum.

    source
    theorem TauCeti.PlumbingGraph.sInfCharacteristicWeight_add_two_mulVec {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (h : P.IsNegativeDefinite) (k : P.characteristicVectors) (m : V → ℤ) :
    P.sInfCharacteristicWeight ⟨fun (v : V) => ↑k v + 2 * P.intersectionMatrix.mulVec m v, ⋯⟩ = P.sInfCharacteristicWeight k - P.characteristicWeight k m

    Passing to the other representative k + 2 · A m of the same spin^c structure shifts the minimal characteristic weight by the constant -χ_k(m).

    The two weight functions differ by the translation χ_{k + 2·A m}(x) = χ_k(x + m) - χ_k(m) of characteristicWeight_add_two_mulVec_eq_sub, and translating the lattice argument permutes the range; so the minimum picks up exactly the constant. This is what lets a d-invariant computed from a chosen representative be transported to any other.

    source
    @[simp]
    theorem TauCeti.PlumbingGraph.sInfCharacteristicWeight_conjugate {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (k : P.characteristicVectors) :
    P.sInfCharacteristicWeight (P.conjugate k) = P.sInfCharacteristicWeight k

    The infimum of the characteristic weight is invariant under spin^c conjugation: negating the covector and the lattice point together preserves the weight, so it permutes the range.

    Conjugation is an involution on characteristic covectors, and characteristicWeight_conjugate_neg says χ_{-k}(-x) = χ_k(x); hence the two weight functions have the same range, and in particular the same infimum.

    source
    theorem TauCeti.PlumbingGraph.IsNegativeDefinite.not_bddAbove_range_characteristicWeight {V : Type u_1} [DecidableEq V] [Fintype V] (P : PlumbingGraph V) (h : P.IsNegativeDefinite) [Nonempty V] (k : P.characteristicVectors) :
    ¬BddAbove (Set.range (P.characteristicWeight k))

    On a negative-definite plumbing with at least one vertex the characteristic weight function is unbounded above: a bound would make every lattice point lie in one sublevel set, which is finite while the lattice is infinite.

    Together with finite_setOfPred_characteristicWeight_le this says that the weight sublevel sets form a genuine exhaustion of the lattice by finite subsets each of which is proper: no single sublevel set is the whole lattice.