Documentation

TauCeti.KnotTheory.Grid.BasicCycles

Cycles and boundaries for the fully blocked grid differential #

This file packages the kernel and range of the fully blocked grid differential as the cycle and boundary submodules of the finite free grid chain module. It does not assert the global square-zero theorem; instead it records the exact condition under which boundaries are cycles.

Main results #

References #

This supplies a prerequisite for TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.3, "The complexes and ∂² = 0". The terminology follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

source
noncomputable def TauCeti.GridDiagram.fullyBlockedCycles {n : ℕ} (G : GridDiagram n) :
Submodule (ZMod 2) (GridChain (ZMod 2) n)

The cycles of the fully blocked grid differential: chains killed by ∂.

Instances For
    source
    noncomputable def TauCeti.GridDiagram.fullyBlockedBoundaries {n : ℕ} (G : GridDiagram n) :
    Submodule (ZMod 2) (GridChain (ZMod 2) n)

    The boundaries of the fully blocked grid differential: chains hit by ∂.

    Instances For
      source
      @[simp]
      theorem TauCeti.GridDiagram.mem_fullyBlockedCycles {n : ℕ} (G : GridDiagram n) (c : GridChain (ZMod 2) n) :
      c ∈ G.fullyBlockedCycles ↔ G.fullyBlockedDifferential c = 0

      A chain is a fully blocked cycle exactly when its differential vanishes.

      source
      @[simp]
      theorem TauCeti.GridDiagram.mem_fullyBlockedBoundaries {n : ℕ} (G : GridDiagram n) (c : GridChain (ZMod 2) n) :
      c ∈ G.fullyBlockedBoundaries ↔ ∃ (b : GridChain (ZMod 2) n), G.fullyBlockedDifferential b = c

      A chain is a fully blocked boundary exactly when it is the differential of some chain.

      source
      theorem TauCeti.GridDiagram.fullyBlockedCycles_eq_ker {n : ℕ} (G : GridDiagram n) :
      G.fullyBlockedCycles = G.fullyBlockedDifferential.ker

      The fully blocked cycle submodule is the kernel of the fully blocked differential, restated so that downstream files can rewrite with it without unfolding the definition.

      source
      theorem TauCeti.GridDiagram.fullyBlockedBoundaries_eq_range {n : ℕ} (G : GridDiagram n) :
      G.fullyBlockedBoundaries = G.fullyBlockedDifferential.range

      The fully blocked boundary submodule is the range of the fully blocked differential, restated so that downstream files can rewrite with it without unfolding the definition.

      source
      theorem TauCeti.GridDiagram.fullyBlockedBoundaries_le_cycles {n : ℕ} (G : GridDiagram n) (hsq : G.fullyBlockedDifferential ∘ₗ G.fullyBlockedDifferential = 0) :
      G.fullyBlockedBoundaries ≤ G.fullyBlockedCycles

      Boundaries lie in cycles once the fully blocked differential is square-zero.

      source
      theorem TauCeti.GridDiagram.fullyBlockedCycles_eq_top_of_fullyBlockedDifferential_eq_zero {n : ℕ} (G : GridDiagram n) (h : G.fullyBlockedDifferential = 0) :
      G.fullyBlockedCycles = ⊤

      The fully blocked cycle submodule is top when the differential is the zero map.

      source
      theorem TauCeti.GridDiagram.fullyBlockedBoundaries_eq_bot_of_fullyBlockedDifferential_eq_zero {n : ℕ} (G : GridDiagram n) (h : G.fullyBlockedDifferential = 0) :
      G.fullyBlockedBoundaries = ⊥

      The fully blocked boundary submodule is bottom when the differential is the zero map.