Documentation

TauCeti.KnotTheory.Grid.Homology.Basic

The fully blocked grid homology #

This file introduces the homology of the fully blocked grid complex as the subquotient of the finite free grid chain module by cycles over boundaries, and evaluates it on the smallest grids.

The cycle submodule (fullyBlockedCycles, the kernel of the differential) and the boundary submodule (fullyBlockedBoundaries, its range) were built in BasicCycles.lean. Viewing the boundaries inside the cycles gives fullyBlockedBoundariesInCycles, and the homology is their subquotient

fullyBlockedHomology G = fullyBlockedCycles G β§Έ fullyBlockedBoundariesInCycles G,

the cycles modulo the boundaries that are themselves cycles. Whenever the differential squares to zero every boundary is a cycle (fullyBlockedBoundaries_le_cycles), so the subquotient is the genuine homology Z / B; the general subquotient form is what lets us name the object before the square-zero theorem is available in every grid size. Two cycles represent the same homology class exactly when their difference is a boundary (fullyBlockedHomology_mk_eq_iff), independently of square-zeroness.

For grids of size at most two the differential vanishes (SmallGridDifferential.lean), so every chain is a cycle and the only boundary is zero. The homology is therefore the whole chain module: it is ZMod 2-linearly isomorphic to GridChain (ZMod 2) n, has 2 ^ n! elements, and has ZMod 2-dimension n!. On the standard 2 Γ— 2 unknot grid this is dimension two, the rank of the stabilization factor W = 𝔽 βŠ• 𝔽 predicted by the standard grid-homology formula for the unknot.

Main definitions #

Main results #

References #

This supplies a prerequisite for TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.3, "The complexes and βˆ‚Β² = 0", and the acceptance criterion that grid homology compute on the 2 Γ— 2 unknot grid with its bigradings, exhibiting the W^{βŠ—(n-1)} stabilization factor. The homology and stabilization conventions follow OzsvΓ‘th--Stipsicz--SzabΓ³, Grid Homology for Knots and Links, Chapter 4.

source
@[instance_reducible]
noncomputable instance TauCeti.GridDiagram.instAddCommGroupSubtypeGridChainZModOfNatNatMemSubmoduleFullyBlockedCycles {n : β„•} (G : GridDiagram n) :
AddCommGroup β†₯G.fullyBlockedCycles

Shortcut instance. The subquotient fullyBlockedHomology below needs the elaborator to identify the module structure on fullyBlockedCycles that appears in a Submodule argument with the one produced by instance search; a direct head match makes that identification syntactic instead of relying on unfolding a ZMod 2 instance diamond, which fails.

source
@[instance_reducible]
noncomputable instance TauCeti.GridDiagram.instModuleZModOfNatNatSubtypeGridChainMemSubmoduleFullyBlockedCycles {n : β„•} (G : GridDiagram n) :
Module (ZMod 2) β†₯G.fullyBlockedCycles

Shortcut instance, paired with the AddCommGroup one above.

source
noncomputable def TauCeti.GridDiagram.fullyBlockedBoundariesInCycles {n : β„•} (G : GridDiagram n) :
Submodule (ZMod 2) β†₯G.fullyBlockedCycles

The fully blocked boundaries, viewed as a submodule of the fully blocked cycles: the cycles that are hit by the differential. This is B βŠ“ Z sitting inside Z, and equals B itself once the differential squares to zero (fullyBlockedBoundaries_le_cycles).

Instances For
    source
    theorem TauCeti.GridDiagram.fullyBlockedBoundariesInCycles_eq_comap {n : β„•} (G : GridDiagram n) :
    G.fullyBlockedBoundariesInCycles = Submodule.comap G.fullyBlockedCycles.subtype G.fullyBlockedBoundaries

    The boundaries inside the cycles are the preimage of the boundaries under the inclusion of the cycles. The body of fullyBlockedBoundariesInCycles is not exposed outside this module, so this restatement is what lets consumers reason about it as a comap.

    source
    @[simp]
    theorem TauCeti.GridDiagram.mem_fullyBlockedBoundariesInCycles {n : β„•} (G : GridDiagram n) (x : β†₯G.fullyBlockedCycles) :
    x ∈ G.fullyBlockedBoundariesInCycles ↔ ↑x ∈ G.fullyBlockedBoundaries

    A cycle lies in fullyBlockedBoundariesInCycles exactly when it is a fully blocked boundary, letting membership be established without unfolding submoduleOf.

    source
    @[reducible, inline]
    abbrev TauCeti.GridDiagram.fullyBlockedHomology {n : β„•} (G : GridDiagram n) :
    Type

    The fully blocked grid homology: the cycles of the fully blocked differential modulo the boundaries that lie inside them.

    This is the subquotient Z β§Έ (B βŠ“ Z), which is the genuine homology Z / B once every boundary is a cycle, i.e. once the differential squares to zero (fullyBlockedBoundaries_le_cycles). Using the subquotient lets the object be named uniformly, before the square-zero theorem is available in every grid size.

    Instances For
      source
      theorem TauCeti.GridDiagram.fullyBlockedHomology_mk_eq_iff {n : β„•} (G : GridDiagram n) (a b : β†₯G.fullyBlockedCycles) :
      Submodule.Quotient.mk a = Submodule.Quotient.mk b ↔ ↑a - ↑b ∈ G.fullyBlockedBoundaries

      Two cycles represent the same fully blocked homology class exactly when their difference is a boundary. This is the defining relation of the homology and does not need the differential to square to zero.

      source
      theorem TauCeti.GridDiagram.fullyBlockedHomology_mk_eq_zero_iff {n : β„•} (G : GridDiagram n) (a : β†₯G.fullyBlockedCycles) :
      Submodule.Quotient.mk a = 0 ↔ ↑a ∈ G.fullyBlockedBoundaries

      A fully blocked homology class is zero exactly when a representing cycle is a boundary, letting classes be shown trivial without unfolding submoduleOf.

      source
      noncomputable def TauCeti.GridDiagram.fullyBlockedHomologyEquivLinearMapHomology {n : β„•} (G : GridDiagram n) :
      G.fullyBlockedHomology ≃ₗ[ZMod 2] G.fullyBlockedDifferential.homology β‹―

      The fully blocked homology is the homology of its square-zero linear differential.

      Instances For
        source
        @[simp]
        theorem TauCeti.GridDiagram.fullyBlockedHomologyEquivLinearMapHomology_mk {n : β„•} (G : GridDiagram n) (z : β†₯G.fullyBlockedCycles) :
        G.fullyBlockedHomologyEquivLinearMapHomology (Submodule.Quotient.mk z) = Submodule.Quotient.mk ((LinearEquiv.ofEq G.fullyBlockedCycles G.fullyBlockedDifferential.ker β‹―) z)

        The kernel-homology identification preserves the underlying cycle representative.

        source
        @[simp]
        theorem TauCeti.GridDiagram.fullyBlockedHomologyEquivLinearMapHomology_symm_mk {n : β„•} (G : GridDiagram n) (z : β†₯G.fullyBlockedDifferential.ker) :
        G.fullyBlockedHomologyEquivLinearMapHomology.symm (Submodule.Quotient.mk z) = Submodule.Quotient.mk ((LinearEquiv.ofEq G.fullyBlockedCycles G.fullyBlockedDifferential.ker β‹―).symm z)

        The inverse kernel-homology identification also preserves cycle representatives.

        source
        theorem TauCeti.GridDiagram.instFactPrimeOfNatNat :
        Fact (Nat.Prime 2)

        The coefficient ring ZMod 2 is a field, as needed for the dimension formula below.

        source
        theorem TauCeti.GridDiagram.finrank_fullyBlockedHomology_add_two_mul_finrank_range {n : β„•} (G : GridDiagram n) :
        Module.finrank (ZMod 2) G.fullyBlockedHomology + 2 * Module.finrank (ZMod 2) β†₯G.fullyBlockedDifferential.range = n.factorial

        Rank-nullity for fully blocked grid homology: the homology dimension plus twice the differential rank is the number of grid states.

        source
        noncomputable def TauCeti.GridDiagram.fullyBlockedHomologyEquivChainOfLeTwo {n : β„•} (G : GridDiagram n) (hn : n ≀ 2) :
        G.fullyBlockedHomology ≃ₗ[ZMod 2] GridChain (ZMod 2) n

        On grids of size at most two the fully blocked differential vanishes, so the homology is the whole chain module: cycles are everything and the only boundary is zero.

        Instances For
          source
          @[simp]
          theorem TauCeti.GridDiagram.fullyBlockedHomologyEquivChainOfLeTwo_apply_mk {n : β„•} (G : GridDiagram n) (hn : n ≀ 2) (c : β†₯G.fullyBlockedCycles) :
          (G.fullyBlockedHomologyEquivChainOfLeTwo hn) (Submodule.Quotient.mk c) = ↑c

          The small-grid equivalence sends the homology class of a cycle to its underlying chain.

          source
          theorem TauCeti.GridDiagram.natCard_fullyBlockedHomology_of_le_two {n : β„•} (G : GridDiagram n) (hn : n ≀ 2) :
          Nat.card G.fullyBlockedHomology = 2 ^ n.factorial

          In grid size at most two the fully blocked homology has 2 ^ n! elements: the size of the whole chain module, since the differential vanishes.

          source
          theorem TauCeti.GridDiagram.finrank_fullyBlockedHomology_of_le_two {n : β„•} (G : GridDiagram n) (hn : n ≀ 2) :
          Module.finrank (ZMod 2) G.fullyBlockedHomology = n.factorial

          In grid size at most two the fully blocked homology has ZMod 2-dimension n!.

          source
          theorem TauCeti.GridDiagram.natCard_fullyBlockedHomology_of_two (G : GridDiagram 2) :
          Nat.card G.fullyBlockedHomology = 4

          Every 2 Γ— 2 grid has a four-element fully blocked homology.

          source
          theorem TauCeti.GridDiagram.finrank_fullyBlockedHomology_of_two (G : GridDiagram 2) :
          Module.finrank (ZMod 2) G.fullyBlockedHomology = 2

          Every 2 Γ— 2 grid has a two-dimensional fully blocked homology, the rank of the stabilization factor W = 𝔽 βŠ• 𝔽 predicted for the unknot.