Row and column relabelings of grid chains

Grid moves relabel the cyclic row or column labels of a grid diagram. The diagram API already has the corresponding operations on grid states, but the free chain module also needs the induced linear equivalences on generators. This file supplies those equivalences for arbitrary permutations; cyclic relabelings are the special case used by GridDiagram.IsMove.

The equivalences are defined by transporting the domain of a finitely supported function. Thus they do not introduce a second chain representation, and their action on generators and coefficients is exposed by simp lemmas. No differential is used here; compatibility with a differential is a separate property proved where a differential is defined.

Main definitions

• TauCeti.GridChain.relabelRowsEquiv: the linear equivalence induced by relabeling rows.
• TauCeti.GridChain.relabelColumnsEquiv: the linear equivalence induced by relabeling columns.

Main results

• TauCeti.GridChain.relabelRowsEquiv_single and TauCeti.GridChain.relabelColumnsEquiv_single: the action on a basis generator.
• TauCeti.GridChain.relabelRowsEquiv_apply and TauCeti.GridChain.relabelColumnsEquiv_apply: the coefficient formulas.
• TauCeti.GridChain.relabelRowsEquiv_apply_relabelRows and TauCeti.GridChain.relabelColumnsEquiv_apply_relabelColumns: the coefficient at a relabeled state.
• TauCeti.GridChain.relabelRowsEquiv_symm and TauCeti.GridChain.relabelColumnsEquiv_symm: inverse relabelings use inverse permutations.

References

The construction uses Mathlib's Finsupp.domLCongr and Finsupp.equivMapDomain_apply. The relabeling convention follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

noncomputable def TauCeti.GridChain.relabelRowsEquiv {R : Type u_1} [Semiring R] {n : ℕ} (ρ : Equiv.Perm (Fin n)) : GridChain R n ≃ₗ[R] GridChain R n

The linear equivalence on grid chains induced by a permutation of the row labels.

noncomputable def TauCeti.GridChain.relabelColumnsEquiv {R : Type u_1} [Semiring R] {n : ℕ} (κ : Equiv.Perm (Fin n)) : GridChain R n ≃ₗ[R] GridChain R n

The linear equivalence on grid chains induced by a permutation of the column labels.

@[simp]

theorem TauCeti.GridChain.relabelRowsEquiv_single {R : Type u_1} [Semiring R] {n : ℕ} (ρ : Equiv.Perm (Fin n)) (x : GridState n) (a : R) : (relabelRowsEquiv ρ) (Finsupp.single x a) = Finsupp.single (GridState.relabelRows ρ x) a

Row relabeling sends a basis generator to the correspondingly relabeled generator.

@[simp]

theorem TauCeti.GridChain.relabelColumnsEquiv_single {R : Type u_1} [Semiring R] {n : ℕ} (κ : Equiv.Perm (Fin n)) (x : GridState n) (a : R) : (relabelColumnsEquiv κ) (Finsupp.single x a) = Finsupp.single (GridState.relabelColumns κ x) a

Column relabeling sends a basis generator to the correspondingly relabeled generator.

@[simp]

theorem TauCeti.GridChain.relabelRowsEquiv_apply {R : Type u_1} [Semiring R] {n : ℕ} (ρ : Equiv.Perm (Fin n)) (f : GridChain R n) (y : GridState n) : ((relabelRowsEquiv ρ) f) y = f (GridState.relabelRows (Equiv.symm ρ) y)

The coefficient at a state after row relabeling is read at the inverse-relabelled state.

@[simp]

theorem TauCeti.GridChain.relabelColumnsEquiv_apply {R : Type u_1} [Semiring R] {n : ℕ} (κ : Equiv.Perm (Fin n)) (f : GridChain R n) (y : GridState n) : ((relabelColumnsEquiv κ) f) y = f (GridState.relabelColumns (Equiv.symm κ) y)

The coefficient at a state after column relabeling is read at the inverse-relabelled state.

theorem TauCeti.GridChain.relabelRowsEquiv_apply_relabelRows {R : Type u_1} [Semiring R] {n : ℕ} (ρ : Equiv.Perm (Fin n)) (f : GridChain R n) (y : GridState n) : ((relabelRowsEquiv ρ) f) (GridState.relabelRows ρ y) = f y

The coefficient of a row-relabeled chain at a relabeled state is the original coefficient.

theorem TauCeti.GridChain.relabelColumnsEquiv_apply_relabelColumns {R : Type u_1} [Semiring R] {n : ℕ} (κ : Equiv.Perm (Fin n)) (f : GridChain R n) (y : GridState n) : ((relabelColumnsEquiv κ) f) (GridState.relabelColumns κ y) = f y

The coefficient of a column-relabeled chain at a relabeled state is the original coefficient.

@[simp]

theorem TauCeti.GridChain.relabelRowsEquiv_symm {R : Type u_1} [Semiring R] {n : ℕ} (ρ : Equiv.Perm (Fin n)) : (relabelRowsEquiv ρ).symm = relabelRowsEquiv (Equiv.symm ρ)

The inverse of a row relabeling is induced by the inverse row permutation.

@[simp]

theorem TauCeti.GridChain.relabelColumnsEquiv_symm {R : Type u_1} [Semiring R] {n : ℕ} (κ : Equiv.Perm (Fin n)) : (relabelColumnsEquiv κ).symm = relabelColumnsEquiv (Equiv.symm κ)

The inverse of a column relabeling is induced by the inverse column permutation.

theorem TauCeti.GridChain.relabelRowsEquiv_symm_apply {R : Type u_1} [Semiring R] {n : ℕ} (ρ : Equiv.Perm (Fin n)) (f : GridChain R n) (y : GridState n) : ((relabelRowsEquiv ρ).symm f) y = f (GridState.relabelRows ρ y)

The inverse row relabeling has the expected coefficient formula.

theorem TauCeti.GridChain.relabelColumnsEquiv_symm_apply {R : Type u_1} [Semiring R] {n : ℕ} (κ : Equiv.Perm (Fin n)) (f : GridChain R n) (y : GridState n) : ((relabelColumnsEquiv κ).symm f) y = f (GridState.relabelColumns κ y)

The inverse column relabeling has the expected coefficient formula.

@[simp]

theorem TauCeti.GridChain.relabelRowsEquiv_refl {R : Type u_1} [Semiring R] {n : ℕ} : relabelRowsEquiv (Equiv.refl (Fin n)) = LinearEquiv.refl R (GridChain R n)

Relabeling by the identity row permutation is the identity linear equivalence.

@[simp]

theorem TauCeti.GridChain.relabelColumnsEquiv_refl {R : Type u_1} [Semiring R] {n : ℕ} : relabelColumnsEquiv (Equiv.refl (Fin n)) = LinearEquiv.refl R (GridChain R n)

Relabeling by the identity column permutation is the identity linear equivalence.

theorem TauCeti.GridChain.relabelRowsEquiv_trans_apply {R : Type u_1} [Semiring R] {n : ℕ} (ρ σ : Equiv.Perm (Fin n)) (f : GridChain R n) : (relabelRowsEquiv σ) ((relabelRowsEquiv ρ) f) = (relabelRowsEquiv (Equiv.trans ρ σ)) f

Row relabeling equivalences compose in the same order as state relabelings.

@[simp]

theorem TauCeti.GridChain.relabelRowsEquiv_trans {R : Type u_1} [Semiring R] {n : ℕ} (ρ σ : Equiv.Perm (Fin n)) : relabelRowsEquiv ρ ≪≫ₗ relabelRowsEquiv σ = relabelRowsEquiv (Equiv.trans ρ σ)

Row relabeling equivalences compose in the same order as state relabelings.

theorem TauCeti.GridChain.relabelColumnsEquiv_trans_apply {R : Type u_1} [Semiring R] {n : ℕ} (κ τ : Equiv.Perm (Fin n)) (f : GridChain R n) : (relabelColumnsEquiv τ) ((relabelColumnsEquiv κ) f) = (relabelColumnsEquiv (Equiv.trans κ τ)) f

Column relabeling equivalences compose in the same order as state relabelings.

@[simp]

theorem TauCeti.GridChain.relabelColumnsEquiv_trans {R : Type u_1} [Semiring R] {n : ℕ} (κ τ : Equiv.Perm (Fin n)) : relabelColumnsEquiv κ ≪≫ₗ relabelColumnsEquiv τ = relabelColumnsEquiv (Equiv.trans κ τ)

Column relabeling equivalences compose in the same order as state relabelings.