Rectangles under grid-point insertion

This file transports an oriented rectangle between grid states along the insertion of a common point into its source and target. It characterizes the sides and covered squares of the transported rectangle, proves that transport is a bijection onto the rectangles between states containing the inserted point, and compares emptiness before and after transport.

Main definitions

• TauCeti.GridRectangleBetween.insertPoint: an oriented rectangle between two grid states, transported to the states obtained by inserting one point.

Main results

• TauCeti.GridRectangleBetween.exists_insertPoint_eq: every rectangle between two states with a common inserted point is transported from the smaller grid.
• TauCeti.GridRectangleBetween.mem_coveredSquares_insertPoint: transport preserves membership of embedded squares in the covered region.
• TauCeti.GridRectangleBetween.mem_coveredSquares_insertPoint_succ_succ: covered-square membership for insertion immediately after specified coordinates is detected by collapsing those coordinates with Fin.predAbove.
• TauCeti.GridRectangleBetween.isEmpty_insertPoint_iff: a transported rectangle is empty exactly when the original one is and the inserted point is not in its interior.

References

For the analogous rectangle correspondence under cyclic permutation of a grid diagram, see TauCeti/KnotTheory/Grid/Differential/CyclicPermutation.lean.

def TauCeti.GridRectangleBetween.insertPoint {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (p q : Fin (n + 1)) : GridRectangleBetween (x.insertPoint p q) (y.insertPoint p q)

An oriented rectangle from x to y, transported to the states obtained from x and y by inserting the point (p, q). Its side columns are the embedded side columns.

@[simp]

theorem TauCeti.GridRectangleBetween.insertPoint_left {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (p q : Fin (n + 1)) : (R.insertPoint p q).left = p.succAbove R.left

The initial side of a transported rectangle is the embedded initial side.

@[simp]

theorem TauCeti.GridRectangleBetween.insertPoint_right {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (p q : Fin (n + 1)) : (R.insertPoint p q).right = p.succAbove R.right

The terminal side of a transported rectangle is the embedded terminal side.

@[simp]

theorem TauCeti.GridRectangleBetween.insertPoint_bottom {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (p q : Fin (n + 1)) : (R.insertPoint p q).bottom = q.succAbove R.bottom

The bottom row of a transported rectangle is the embedded bottom row.

@[simp]

theorem TauCeti.GridRectangleBetween.insertPoint_top {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (p q : Fin (n + 1)) : (R.insertPoint p q).top = q.succAbove R.top

The top row of a transported rectangle is the embedded top row.

theorem TauCeti.GridRectangleBetween.insertPoint_injective {n : ℕ} {x y : GridState n} (p q : Fin (n + 1)) : Function.Injective fun (R : GridRectangleBetween x y) => R.insertPoint p q

Transporting rectangles along an inserted point is injective.

theorem TauCeti.GridRectangleBetween.exists_insertPoint_eq {n : ℕ} {x y : GridState n} {p q : Fin (n + 1)} (S : GridRectangleBetween (x.insertPoint p q) (y.insertPoint p q)) : ∃ (R : GridRectangleBetween x y), R.insertPoint p q = S

Every rectangle between two states containing the same inserted point is transported from a rectangle of the smaller grid. The inserted column is not a side column, since both states use the inserted row there.

theorem TauCeti.GridRectangleBetween.mem_coveredSquares_insertPoint {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (p q : Fin (n + 1)) (c r : Fin n) : (p.succAbove c, q.succAbove r) ∈ (R.insertPoint p q).toGridRectangle.coveredSquares ↔ (c, r) ∈ R.toGridRectangle.coveredSquares

A transported rectangle covers the embedded image of a square exactly when the original rectangle covers that square.

theorem TauCeti.GridRectangleBetween.mem_coveredSquares_insertPoint_succ_succ {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (i j : Fin n) (a : Fin (n + 1) × Fin (n + 1)) : a ∈ (R.insertPoint i.succ j.succ).toGridRectangle.coveredSquares ↔ (i.predAbove a.1, j.predAbove a.2) ∈ R.toGridRectangle.coveredSquares

When the point is inserted immediately after the column i and the row j, a square of the larger grid is covered by a transported rectangle exactly when its collapse under Fin.predAbove is covered by the original rectangle.

@[simp]

theorem TauCeti.GridRectangleBetween.isEmpty_insertPoint_iff {n : ℕ} {x y : GridState n} (R : GridRectangleBetween x y) (p q : Fin (n + 1)) : (R.insertPoint p q).IsEmpty ↔ R.IsEmpty ∧ (p, q) ∉ (R.insertPoint p q).toGridRectangle.interior

A transported rectangle is empty exactly when the original rectangle is empty and the inserted point does not lie in the interior of the transported rectangle.