Small-grid cycles and boundaries for the fully blocked grid differential

This file computes the cycle and boundary submodules of the fully blocked grid differential in the already-proved zero-differential small-grid case.

Main results

• TauCeti.GridDiagram.fullyBlockedCycles_eq_top_of_le_two and TauCeti.GridDiagram.fullyBlockedBoundaries_eq_bot_of_le_two: the small-grid computation.
• TauCeti.GridDiagram.natCard_fullyBlockedCycles_of_le_two and TauCeti.GridDiagram.natCard_fullyBlockedBoundaries_of_le_two: the small-grid cardinalities.

References

This supplies a prerequisite for TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.3, "The complexes and ∂² = 0", and for the standing convention that grid complexes compute on explicit small grids.

theorem TauCeti.GridDiagram.fullyBlockedCycles_eq_top_of_le_two {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) : G.fullyBlockedCycles = ⊤

In grid size at most two, every chain is a cycle for the fully blocked differential.

theorem TauCeti.GridDiagram.fullyBlockedBoundaries_eq_bot_of_le_two {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) : G.fullyBlockedBoundaries = ⊥

In grid size at most two, the only boundary for the fully blocked differential is zero.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedCycles_eq_top_of_two (G : GridDiagram 2) : G.fullyBlockedCycles = ⊤

On every 2 × 2 grid, every chain is a cycle for the fully blocked differential.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedBoundaries_eq_bot_of_two (G : GridDiagram 2) : G.fullyBlockedBoundaries = ⊥

On every 2 × 2 grid, the only boundary for the fully blocked differential is zero.

theorem TauCeti.GridDiagram.mem_fullyBlockedCycles_of_le_two {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) (c : GridChain (ZMod 2) n) : c ∈ G.fullyBlockedCycles

In grid size at most two, every chain is a fully blocked cycle.

theorem TauCeti.GridDiagram.mem_fullyBlockedBoundaries_iff_eq_zero_of_le_two {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) (c : GridChain (ZMod 2) n) : c ∈ G.fullyBlockedBoundaries ↔ c = 0

In grid size at most two, a fully blocked boundary is exactly the zero chain.

theorem TauCeti.GridDiagram.mem_fullyBlockedCycles_of_two (G : GridDiagram 2) (c : GridChain (ZMod 2) 2) : c ∈ G.fullyBlockedCycles

On every 2 × 2 grid, every chain is a fully blocked cycle.

theorem TauCeti.GridDiagram.mem_fullyBlockedBoundaries_iff_eq_zero_of_two (G : GridDiagram 2) (c : GridChain (ZMod 2) 2) : c ∈ G.fullyBlockedBoundaries ↔ c = 0

On every 2 × 2 grid, a fully blocked boundary is exactly the zero chain.

theorem TauCeti.GridDiagram.natCard_fullyBlockedCycles_of_le_two {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) : Nat.card ↥G.fullyBlockedCycles = 2 ^ n.factorial

In grid size at most two, there are 2 ^ n! fully blocked cycles.

theorem TauCeti.GridDiagram.natCard_fullyBlockedBoundaries_of_le_two {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) : Nat.card ↥G.fullyBlockedBoundaries = 1

In grid size at most two, there is one fully blocked boundary.

theorem TauCeti.GridDiagram.natCard_fullyBlockedCycles_of_two (G : GridDiagram 2) : Nat.card ↥G.fullyBlockedCycles = 4

Every 2 × 2 grid has four fully blocked cycles.

theorem TauCeti.GridDiagram.natCard_fullyBlockedBoundaries_of_two (G : GridDiagram 2) : Nat.card ↥G.fullyBlockedBoundaries = 1

Every 2 × 2 grid has one fully blocked boundary.