Documentation

TauCeti.KnotTheory.Grid.Differential.Square.Repartition

Repartitions of two-step grid rectangle domains #

Two two-step grid rectangle decompositions are repartitions when the rectangles in each decomposition cover disjoint sets of squares and the unions of those sets agree. This is the domain relation used by the juxtaposition proof of ∂⁻ ∘ ∂⁻ = 0: it transports multiplicative weights and avoidance of marked squares without requiring the two cuts to be distinct.

Main definitions #

Main results #

References #

The repartition argument follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.6.

source
structure TauCeti.GridRectangleDecomposition.IsRepartition {n : ℕ} {x z : GridState n} (D E : GridRectangleDecomposition x z) :
Prop

E is a repartition of D: the rectangles in each decomposition cover disjoint sets of squares, and the two unions agree.

Instances For
    source
    theorem TauCeti.GridRectangleDecomposition.IsRepartition.symm {n : ℕ} {x z : GridState n} {D E : GridRectangleDecomposition x z} (h : D.IsRepartition E) :
    E.IsRepartition D

    Being a repartition is a symmetric relation.

    source
    theorem TauCeti.GridRectangleDecomposition.IsRepartition.transpose {n : ℕ} {x z : GridState n} {D E : GridRectangleDecomposition x z} (h : D.IsRepartition E) :
    D.transpose.IsRepartition E.transpose

    Diagonal reflection preserves a repartition of two-step rectangle domains.

    source
    @[simp]
    theorem TauCeti.GridRectangleDecomposition.IsRepartition.transpose_iff {n : ℕ} {x z : GridState n} {D E : GridRectangleDecomposition x z} :
    D.transpose.IsRepartition E.transpose ↔ D.IsRepartition E

    Two decompositions are repartitions exactly when their diagonal reflections are.

    source
    theorem TauCeti.GridRectangleDecomposition.IsRepartition.prod_coveredSquares_mul_prod_coveredSquares {n : ℕ} {x z : GridState n} {D E : GridRectangleDecomposition x z} (h : D.IsRepartition E) {M : Type u_1} [CommMonoid M] (f : Fin n × Fin n → M) :
    (∏ p ∈ E.first.toGridRectangle.coveredSquares, f p) * ∏ p ∈ E.second.toGridRectangle.coveredSquares, f p = (∏ p ∈ D.first.toGridRectangle.coveredSquares, f p) * ∏ p ∈ D.second.toGridRectangle.coveredSquares, f p

    A repartition preserves the product of any multiplicative weight on squares: both decompositions partition the same finite set of covered squares.

    source
    theorem TauCeti.GridRectangleDecomposition.IsRepartition.OMonomial_mul_OMonomial {n : ℕ} {x z : GridState n} {D E : GridRectangleDecomposition x z} (h : D.IsRepartition E) (G : GridDiagram n) (R : Type u_1) [CommSemiring R] :
    G.OMonomial R E.first.toGridRectangle * G.OMonomial R E.second.toGridRectangle = G.OMonomial R D.first.toGridRectangle * G.OMonomial R D.second.toGridRectangle

    A repartition preserves the product of the O-monomial weights that the unblocked differential attaches to its two rectangles.

    source
    theorem TauCeti.GridRectangleDecomposition.IsRepartition.val_add_val_eq {n : ℕ} {x z : GridState n} {D E : GridRectangleDecomposition x z} (h : D.IsRepartition E) :
    E.first.toGridRectangle.coveredSquares.val + E.second.toGridRectangle.coveredSquares.val = D.first.toGridRectangle.coveredSquares.val + D.second.toGridRectangle.coveredSquares.val

    A repartition covers the same squares with the same multiplicities on both sides.

    source
    theorem TauCeti.GridRectangleDecomposition.IsRepartition.disjoint_coveredSquares_union {n : ℕ} {x z : GridState n} {D E : GridRectangleDecomposition x z} (h : D.IsRepartition E) {s : Finset (Fin n × Fin n)} (h₁ : Disjoint D.first.toGridRectangle.coveredSquares s) (h₂ : Disjoint D.second.toGridRectangle.coveredSquares s) :
    Disjoint (E.first.toGridRectangle.coveredSquares ∪ E.second.toGridRectangle.coveredSquares) s

    If neither rectangle of the left-hand decomposition meets a set of squares, then the union of the right-hand decomposition does not meet it either.

    source
    theorem TauCeti.GridRectangleDecomposition.IsRepartition.disjoint_coveredSquares_first {n : ℕ} {x z : GridState n} {D E : GridRectangleDecomposition x z} (h : D.IsRepartition E) {s : Finset (Fin n × Fin n)} (h₁ : Disjoint D.first.toGridRectangle.coveredSquares s) (h₂ : Disjoint D.second.toGridRectangle.coveredSquares s) :
    Disjoint E.first.toGridRectangle.coveredSquares s

    If neither rectangle of the left-hand decomposition meets a set of squares, then neither does the first rectangle of the right-hand decomposition.

    source
    theorem TauCeti.GridRectangleDecomposition.IsRepartition.disjoint_coveredSquares_second {n : ℕ} {x z : GridState n} {D E : GridRectangleDecomposition x z} (h : D.IsRepartition E) {s : Finset (Fin n × Fin n)} (h₁ : Disjoint D.first.toGridRectangle.coveredSquares s) (h₂ : Disjoint D.second.toGridRectangle.coveredSquares s) :
    Disjoint E.second.toGridRectangle.coveredSquares s

    If neither rectangle of the left-hand decomposition meets a set of squares, then neither does the second rectangle of the right-hand decomposition.