Two-step decompositions of grid domains

Many identities in grid homology compare sums over composite domains: a domain of one kind from a grid state x to an intermediate grid state, followed by a domain of another kind from there to a grid state z. This file packages such a pair, for arbitrary families of domains indexed by their source and target states, as TauCeti.GridTwoStepDecomposition. The two-step rectangle decompositions of the square of the grid differential and the rectangle--pentagon, hexagon--rectangle and pentagon--pentagon decompositions of grid commutation all specialize it.

Main definitions

• TauCeti.GridTwoStepDecomposition: a domain followed by a second domain through an intermediate grid state.
• TauCeti.GridTwoStepDecomposition.decompositionsOf: the finite family of two-step decompositions whose constituent domains lie in prescribed finite families.

Main results

• TauCeti.GridTwoStepDecomposition.mem_decompositionsOf characterizes membership in decompositionsOf.
• TauCeti.GridTwoStepDecomposition.card_decompositionsOf counts decompositionsOf.
• TauCeti.GridTwoStepDecomposition.sum_decompositionsOf rewrites a sum over decompositionsOf as the iterated sum over the intermediate state and the two constituent domains.

structure TauCeti.GridTwoStepDecomposition {n : ℕ} (A : GridState n → GridState n → Type u_1) (B : GridState n → GridState n → Type u_2) (x z : GridState n) : Type (max u_1 u_2)

A pair of composable domains through an intermediate grid state.

• middle : GridState n

  The grid state at which the two domains meet.

• first : A x self.middle

  The first domain, from the source to the intermediate state.

• second : B self.middle z

  The second domain, from the intermediate state to the target.

theorem TauCeti.GridTwoStepDecomposition.ext {n : ℕ} {A : GridState n → GridState n → Type u_1} {B : GridState n → GridState n → Type u_2} {x z : GridState n} {D E : GridTwoStepDecomposition A B x z} (hmiddle : D.middle = E.middle) (hfirst : D.first ≍ E.first) (hsecond : D.second ≍ E.second) : D = E

Two two-step decompositions are equal when their intermediate states and domains agree.

theorem TauCeti.GridTwoStepDecomposition.ext_iff {n : ℕ} {A : GridState n → GridState n → Type u_1} {B : GridState n → GridState n → Type u_2} {x z : GridState n} {D E : GridTwoStepDecomposition A B x z} : D = E ↔ D.middle = E.middle ∧ D.first ≍ E.first ∧ D.second ≍ E.second

noncomputable def TauCeti.GridTwoStepDecomposition.decompositionsOf {n : ℕ} {A : GridState n → GridState n → Type u_1} {B : GridState n → GridState n → Type u_2} (first : (u v : GridState n) → Finset (A u v)) (second : (u v : GridState n) → Finset (B u v)) (x z : GridState n) : Finset (GridTwoStepDecomposition A B x z)

The finite family of two-step decompositions selected by prescribed domain families.

@[simp]

theorem TauCeti.GridTwoStepDecomposition.mem_decompositionsOf {n : ℕ} {A : GridState n → GridState n → Type u_1} {B : GridState n → GridState n → Type u_2} {x z : GridState n} (first : (u v : GridState n) → Finset (A u v)) (second : (u v : GridState n) → Finset (B u v)) (D : GridTwoStepDecomposition A B x z) : D ∈ decompositionsOf first second x z ↔ D.first ∈ first x D.middle ∧ D.second ∈ second D.middle z

Membership in decompositionsOf is membership of both constituent domains.

theorem TauCeti.GridTwoStepDecomposition.card_decompositionsOf {n : ℕ} {A : GridState n → GridState n → Type u_1} {B : GridState n → GridState n → Type u_2} (first : (u v : GridState n) → Finset (A u v)) (second : (u v : GridState n) → Finset (B u v)) (x z : GridState n) : (decompositionsOf first second x z).card = ∑ y : GridState n, (first x y).card * (second y z).card

The number of selected two-step decompositions is the sum, over intermediate states, of the products of the numbers of selected constituent domains.

theorem TauCeti.GridTwoStepDecomposition.sum_decompositionsOf {n : ℕ} {A : GridState n → GridState n → Type u_1} {B : GridState n → GridState n → Type u_2} {x z : GridState n} {M : Type u_3} [AddCommMonoid M] (first : (u v : GridState n) → Finset (A u v)) (second : (u v : GridState n) → Finset (B u v)) (w : (y : GridState n) → A x y → B y z → M) : ∑ D ∈ decompositionsOf first second x z, w D.middle D.first D.second = ∑ y : GridState n, ∑ P ∈ first x y, ∑ Q ∈ second y z, w y P Q

A sum over selected two-step decompositions is the corresponding iterated sum.