Documentation

TauCeti.KnotTheory.Grid.StateCardinality

Cardinality of grid states #

This file records the finite size of the generator set for an n × n grid complex. A grid state is encoded in TauCeti.KnotTheory.Grid.Diagram.Basic as a permutation graph on the columns, so the set of grid states is equivalent to Equiv.Perm (Fin n) and has cardinality n!.

The statements here are deliberately about the generator set only. They are the counting API needed before explicit computations of small fully blocked grid complexes, whose chain module is the free ZMod 2-module on GridState n.

Main results #

References #

This advances TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.1, "Grid diagrams and grid states", and the standing convention that the grid complexes should compute on explicit small grids. The encoding follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3: a grid state is one occupied grid point in every row and every column.

source
@[simp]
theorem TauCeti.GridState.card (n : ℕ) :
Fintype.card (GridState n) = n.factorial

The number of grid states on an n × n grid is n!.

source
theorem TauCeti.GridState.card_univ (n : ℕ) :
Finset.univ.card = n.factorial

The universe finite set of grid states has cardinality n!.

source
theorem TauCeti.GridState.natCard (n : ℕ) :
Nat.card (GridState n) = n.factorial

The natural cardinality of grid states is n!.

source
theorem TauCeti.GridState.card_zero :
Fintype.card (GridState 0) = 1

There is one grid state on the empty grid.

source
theorem TauCeti.GridState.card_one :
Fintype.card (GridState 1) = 1

There is one grid state on a 1 × 1 grid.

source
theorem TauCeti.GridState.card_two :
Fintype.card (GridState 2) = 2

There are two grid states on a 2 × 2 grid.

source
theorem TauCeti.GridState.subsingletonOfLeOne {n : ℕ} (hn : n ≤ 1) :
Subsingleton (GridState n)

Any two grid states are equal whenever the grid has at most one row and column.

source
@[instance_reducible]
instance TauCeti.GridState.instUniqueZero :
Unique (GridState 0)

There is a unique grid state on the empty grid.

source
theorem TauCeti.GridState.default_zero_eq :
default = (equivPerm 0).symm 1

The unique empty-grid state is the state associated to the identity permutation.

source
@[instance_reducible]
instance TauCeti.GridState.instUniqueOne :
Unique (GridState 1)

There is a unique grid state on a 1 × 1 grid.

source
@[simp]
theorem TauCeti.GridState.apply_eq_zero (x : GridState 1) (c : Fin 1) :
x.toPerm c = 0

The unique 1 × 1 grid state sends the only column to the only row.

source
theorem TauCeti.GridState.eq_equivPerm_symm_one_or_eq_equivPerm_symm_swap (x : GridState 2) :
x = (equivPerm 2).symm 1 ∨ x = (equivPerm 2).symm (Equiv.swap 0 1)

The two grid states on a 2 × 2 grid are exactly the identity and the transposition.

source
@[reducible, inline]
abbrev TauCeti.GridState.twoByTwoId :
GridState 2

The identity grid state on a 2 × 2 grid.

Instances For
    source
    @[reducible, inline]
    abbrev TauCeti.GridState.twoByTwoSwap :
    GridState 2

    The transposition grid state on a 2 × 2 grid.

    Instances For
      source
      @[simp]
      theorem TauCeti.GridState.twoByTwoId_zero :
      twoByTwoId.toPerm 0 = 0

      The identity two-by-two state sends column 0 to row 0.

      source
      @[simp]
      theorem TauCeti.GridState.twoByTwoId_one :
      twoByTwoId.toPerm 1 = 1

      The identity two-by-two state sends column 1 to row 1.

      source
      theorem TauCeti.GridState.twoByTwoSwap_zero :
      twoByTwoSwap.toPerm 0 = 1

      The transposition two-by-two state sends column 0 to row 1.

      source
      theorem TauCeti.GridState.twoByTwoSwap_one :
      twoByTwoSwap.toPerm 1 = 0

      The transposition two-by-two state sends column 1 to row 0.

      source
      theorem TauCeti.GridState.twoByTwoId_ne_twoByTwoSwap :
      twoByTwoId ≠ twoByTwoSwap

      The two named 2 × 2 grid states are distinct.

      source
      theorem TauCeti.GridState.eq_twoByTwoId_or_eq_twoByTwoSwap (x : GridState 2) :
      x = twoByTwoId ∨ x = twoByTwoSwap

      Every 2 × 2 grid state is either the identity state or the transposition state.