Documentation

TauCeti.KnotTheory.Grid.Rectangle.Relabeling

Relabeling oriented grid rectangles #

An oriented rectangle between two grid states only records where the two states exchange rows, so it survives an arbitrary relabeling of the rows or of the columns: relabeling the rows keeps its side columns, while relabeling the columns renames them. This file packages these two transports as equivalences between the rectangles joining two states and the rectangles joining their relabelings.

Emptiness and the covered squares are a different matter, because they are defined by cyclic intervals and an arbitrary permutation of Fin n does not preserve the cyclic order. The cyclic permutation finRotate n does, by Grid.mem_cIoo_finRotate_finRotate and Grid.mem_cIco_finRotate_finRotate, so for it the transported rectangle is empty exactly when the original one is, and covers the correspondingly rotated squares. These are the rectangle-level facts behind the invariance of the grid differentials under the cyclic permutation moves of a grid diagram.

The half-turn GridState.halfTurn relabels both the rows and the columns by negation modulo n, which reverses the cyclic order. Composed with exchanging the two side columns (GridRectangleBetween.swapSides), it transports rectangles again, and the transported rectangle is empty exactly when the original one is; it covers the squares obtained by reversing both coordinates with Fin.rev, which are where GridDiagram.rotate moves the markings.

Main definitions #

Main results #

References #

Cyclic permutations of a toroidal grid diagram and their effect on rectangles follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

Row relabeling #

source
def TauCeti.GridRectangleBetween.relabelRowsEquiv {n : ℕ} (ρ : Equiv.Perm (Fin n)) (x y : GridState n) :
GridRectangleBetween x y ≃ GridRectangleBetween (GridState.relabelRows ρ x) (GridState.relabelRows ρ y)

Relabeling the rows of two grid states transports the oriented rectangles between them: the relabeled states still exchange rows at the same two side columns.

Instances For
    source
    @[simp]
    theorem TauCeti.GridRectangleBetween.relabelRowsEquiv_apply_left {n : ℕ} {x y : GridState n} (ρ : Equiv.Perm (Fin n)) (R : GridRectangleBetween x y) :
    ((relabelRowsEquiv ρ x y) R).left = R.left

    Row relabeling keeps the initial side column.

    source
    @[simp]
    theorem TauCeti.GridRectangleBetween.relabelRowsEquiv_apply_right {n : ℕ} {x y : GridState n} (ρ : Equiv.Perm (Fin n)) (R : GridRectangleBetween x y) :
    ((relabelRowsEquiv ρ x y) R).right = R.right

    Row relabeling keeps the terminal side column.

    source
    @[simp]
    theorem TauCeti.GridRectangleBetween.relabelRowsEquiv_symm_apply_left {n : ℕ} {x y : GridState n} (ρ : Equiv.Perm (Fin n)) (S : GridRectangleBetween (GridState.relabelRows ρ x) (GridState.relabelRows ρ y)) :
    ((relabelRowsEquiv ρ x y).symm S).left = S.left

    The inverse of row relabeling keeps the initial side column.

    source
    @[simp]
    theorem TauCeti.GridRectangleBetween.relabelRowsEquiv_symm_apply_right {n : ℕ} {x y : GridState n} (ρ : Equiv.Perm (Fin n)) (S : GridRectangleBetween (GridState.relabelRows ρ x) (GridState.relabelRows ρ y)) :
    ((relabelRowsEquiv ρ x y).symm S).right = S.right

    The inverse of row relabeling keeps the terminal side column.

    source
    @[simp]
    theorem TauCeti.GridRectangleBetween.relabelRowsEquiv_apply_bottom {n : ℕ} {x y : GridState n} (ρ : Equiv.Perm (Fin n)) (R : GridRectangleBetween x y) :
    ((relabelRowsEquiv ρ x y) R).bottom = ρ R.bottom

    Row relabeling renames the initial side row.

    source
    @[simp]
    theorem TauCeti.GridRectangleBetween.relabelRowsEquiv_apply_top {n : ℕ} {x y : GridState n} (ρ : Equiv.Perm (Fin n)) (R : GridRectangleBetween x y) :
    ((relabelRowsEquiv ρ x y) R).top = ρ R.top

    Row relabeling renames the terminal side row.

    source
    @[simp]
    theorem TauCeti.GridRectangleBetween.relabelRowsEquiv_symm_apply_bottom {n : ℕ} {x y : GridState n} (ρ : Equiv.Perm (Fin n)) (S : GridRectangleBetween (GridState.relabelRows ρ x) (GridState.relabelRows ρ y)) :
    ((relabelRowsEquiv ρ x y).symm S).bottom = (Equiv.symm ρ) S.bottom

    The inverse of row relabeling renames the initial side row back.

    source
    @[simp]
    theorem TauCeti.GridRectangleBetween.relabelRowsEquiv_symm_apply_top {n : ℕ} {x y : GridState n} (ρ : Equiv.Perm (Fin n)) (S : GridRectangleBetween (GridState.relabelRows ρ x) (GridState.relabelRows ρ y)) :
    ((relabelRowsEquiv ρ x y).symm S).top = (Equiv.symm ρ) S.top

    The inverse of row relabeling renames the terminal side row back.

    source
    @[simp]
    theorem TauCeti.GridRectangleBetween.isEmpty_relabelRowsEquiv_finRotate {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) :
    ((relabelRowsEquiv (finRotate n) x y) R).IsEmpty ↔ R.IsEmpty

    A cyclic permutation of the rows preserves and reflects emptiness of a rectangle.

    source
    theorem TauCeti.GridRectangleBetween.mem_coveredSquares_relabelRowsEquiv_finRotate {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (p : Fin n × Fin n) :
    p ∈ ((relabelRowsEquiv (finRotate n) x y) R).toGridRectangle.coveredSquares ↔ (p.1, (Equiv.symm (finRotate n)) p.2) ∈ R.toGridRectangle.coveredSquares

    A cyclic permutation of the rows rotates the squares a rectangle covers in the row direction.

    Column relabeling #

    source
    def TauCeti.GridRectangleBetween.relabelColumnsEquiv {n : ℕ} (κ : Equiv.Perm (Fin n)) (x y : GridState n) :
    GridRectangleBetween x y ≃ GridRectangleBetween (GridState.relabelColumns κ x) (GridState.relabelColumns κ y)

    Relabeling the columns of two grid states transports the oriented rectangles between them: the relabeled states exchange rows at the renamed side columns.

    Instances For
      source
      @[simp]
      theorem TauCeti.GridRectangleBetween.relabelColumnsEquiv_apply_left {n : ℕ} {x y : GridState n} (κ : Equiv.Perm (Fin n)) (R : GridRectangleBetween x y) :
      ((relabelColumnsEquiv κ x y) R).left = κ R.left

      Column relabeling renames the initial side column.

      source
      @[simp]
      theorem TauCeti.GridRectangleBetween.relabelColumnsEquiv_apply_right {n : ℕ} {x y : GridState n} (κ : Equiv.Perm (Fin n)) (R : GridRectangleBetween x y) :
      ((relabelColumnsEquiv κ x y) R).right = κ R.right

      Column relabeling renames the terminal side column.

      source
      @[simp]
      theorem TauCeti.GridRectangleBetween.relabelColumnsEquiv_symm_apply_left {n : ℕ} {x y : GridState n} (κ : Equiv.Perm (Fin n)) (S : GridRectangleBetween (GridState.relabelColumns κ x) (GridState.relabelColumns κ y)) :
      ((relabelColumnsEquiv κ x y).symm S).left = (Equiv.symm κ) S.left

      The inverse of column relabeling renames the initial side column back.

      source
      @[simp]
      theorem TauCeti.GridRectangleBetween.relabelColumnsEquiv_symm_apply_right {n : ℕ} {x y : GridState n} (κ : Equiv.Perm (Fin n)) (S : GridRectangleBetween (GridState.relabelColumns κ x) (GridState.relabelColumns κ y)) :
      ((relabelColumnsEquiv κ x y).symm S).right = (Equiv.symm κ) S.right

      The inverse of column relabeling renames the terminal side column back.

      source
      @[simp]
      theorem TauCeti.GridRectangleBetween.relabelColumnsEquiv_apply_bottom {n : ℕ} {x y : GridState n} (κ : Equiv.Perm (Fin n)) (R : GridRectangleBetween x y) :
      ((relabelColumnsEquiv κ x y) R).bottom = R.bottom

      Column relabeling keeps the initial side row.

      source
      @[simp]
      theorem TauCeti.GridRectangleBetween.relabelColumnsEquiv_apply_top {n : ℕ} {x y : GridState n} (κ : Equiv.Perm (Fin n)) (R : GridRectangleBetween x y) :
      ((relabelColumnsEquiv κ x y) R).top = R.top

      Column relabeling keeps the terminal side row.

      source
      @[simp]
      theorem TauCeti.GridRectangleBetween.relabelColumnsEquiv_symm_apply_bottom {n : ℕ} {x y : GridState n} (κ : Equiv.Perm (Fin n)) (S : GridRectangleBetween (GridState.relabelColumns κ x) (GridState.relabelColumns κ y)) :
      ((relabelColumnsEquiv κ x y).symm S).bottom = S.bottom

      The inverse of column relabeling keeps the initial side row.

      source
      @[simp]
      theorem TauCeti.GridRectangleBetween.relabelColumnsEquiv_symm_apply_top {n : ℕ} {x y : GridState n} (κ : Equiv.Perm (Fin n)) (S : GridRectangleBetween (GridState.relabelColumns κ x) (GridState.relabelColumns κ y)) :
      ((relabelColumnsEquiv κ x y).symm S).top = S.top

      The inverse of column relabeling keeps the terminal side row.

      source
      @[simp]
      theorem TauCeti.GridRectangleBetween.isEmpty_relabelColumnsEquiv_finRotate {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) :
      ((relabelColumnsEquiv (finRotate n) x y) R).IsEmpty ↔ R.IsEmpty

      A cyclic permutation of the columns preserves and reflects emptiness of a rectangle.

      source
      theorem TauCeti.GridRectangleBetween.mem_coveredSquares_relabelColumnsEquiv_finRotate {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (p : Fin n × Fin n) :
      p ∈ ((relabelColumnsEquiv (finRotate n) x y) R).toGridRectangle.coveredSquares ↔ ((Equiv.symm (finRotate n)) p.1, p.2) ∈ R.toGridRectangle.coveredSquares

      A cyclic permutation of the columns rotates the squares a rectangle covers in the column direction.

      Half-turn #

      source
      def TauCeti.GridRectangleBetween.halfTurnEquiv {n : ℕ} (x y : GridState n) :
      GridRectangleBetween x y ≃ GridRectangleBetween x.halfTurn y.halfTurn

      The half-turn GridState.halfTurn transports the oriented rectangles between two grid states. It negates the side columns modulo n, which reverses their cyclic order, so the image of the terminal side column becomes the initial one: the rectangle is relabeled in its columns and rows by negation and then has its two sides exchanged.

      Instances For
        source
        @[simp]
        theorem TauCeti.GridRectangleBetween.halfTurnEquiv_apply_left {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) :
        ((halfTurnEquiv x y) R).left = (finRotate n) R.right.rev

        The initial side column of the half-turned rectangle is the negated terminal side column.

        source
        @[simp]
        theorem TauCeti.GridRectangleBetween.halfTurnEquiv_apply_right {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) :
        ((halfTurnEquiv x y) R).right = (finRotate n) R.left.rev

        The terminal side column of the half-turned rectangle is the negated initial side column.

        source
        @[simp]
        theorem TauCeti.GridRectangleBetween.halfTurnEquiv_symm_apply_left {n : ℕ} {x y : GridState n} (S : GridRectangleBetween x.halfTurn y.halfTurn) :
        ((halfTurnEquiv x y).symm S).left = (finRotate n) S.right.rev

        The inverse half-turn negates the terminal side column into the initial one.

        source
        @[simp]
        theorem TauCeti.GridRectangleBetween.halfTurnEquiv_symm_apply_right {n : ℕ} {x y : GridState n} (S : GridRectangleBetween x.halfTurn y.halfTurn) :
        ((halfTurnEquiv x y).symm S).right = (finRotate n) S.left.rev

        The inverse half-turn negates the initial side column into the terminal one.

        source
        @[simp]
        theorem TauCeti.GridRectangleBetween.halfTurnEquiv_apply_bottom {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) :
        ((halfTurnEquiv x y) R).bottom = (finRotate n) R.top.rev

        The initial side row of the half-turned rectangle is the negated terminal side row.

        source
        @[simp]
        theorem TauCeti.GridRectangleBetween.halfTurnEquiv_apply_top {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) :
        ((halfTurnEquiv x y) R).top = (finRotate n) R.bottom.rev

        The terminal side row of the half-turned rectangle is the negated initial side row.

        source
        @[simp]
        theorem TauCeti.GridRectangleBetween.isEmpty_halfTurnEquiv {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) :
        ((halfTurnEquiv x y) R).IsEmpty ↔ R.IsEmpty

        The half-turn preserves and reflects emptiness of a rectangle.

        source
        theorem TauCeti.GridRectangleBetween.mem_coveredSquares_halfTurnEquiv {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (p : Fin n × Fin n) :
        p ∈ ((halfTurnEquiv x y) R).toGridRectangle.coveredSquares ↔ (p.1.rev, p.2.rev) ∈ R.toGridRectangle.coveredSquares

        The half-turn reverses both coordinates of the squares a rectangle covers.

        source
        theorem TauCeti.GridRectangleBetween.card_pointSet_inter_interior_halfTurnEquiv {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (m : GridState n) :
        (m.halfTurn.pointSet ∩ ((halfTurnEquiv x y) R).toGridRectangle.interior).card = (m.pointSet ∩ R.toGridRectangle.interior).card

        The half-turn preserves the number of grid-state points in a rectangle's interior.

        source
        theorem TauCeti.GridRectangleBetween.card_source_pointSet_inter_halfTurnEquiv {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) :
        (x.halfTurn.pointSet ∩ ((halfTurnEquiv x y) R).toGridRectangle.coveredSquares).card = (x.pointSet ∩ R.toGridRectangle.coveredSquares).card

        The half-turn preserves the number of occupied source-state squares of a rectangle. The lower-left corner is counted separately from the interior grid points.

        source
        theorem TauCeti.GridRectangleBetween.card_pointSet_inter_halfTurnEquiv {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (m : GridState n) :
        (m.rotate.pointSet ∩ ((halfTurnEquiv x y) R).toGridRectangle.coveredSquares).card = (m.pointSet ∩ R.toGridRectangle.coveredSquares).card

        The half-turn preserves the number of marking squares covered by a rectangle. Marking square coordinates use rotate, whereas rectangle corners use halfTurn.