Planar Rook Diagrams

A rook diagram on a $n \times m$ board is a collection of mutually non-attacking rooks. It is planar if no rook is "North-East" or "South-West" of any other.

Diagramatically, we can assign each rook to two numbers indicating its row and column. Due to the non-attacking condition, these numbers are unique to each rook. We can then draw this as two columns of vertices (one of $n$ points and one of $m$) with lines connecting a vertex on the left and on the right if they label the row and column of the same rook. The planarity condition is then equivalent to the condition that these lines do not cross.

structure PlanarRook.Diagram (n m : ℕ) : Type

A planar rook diagram with n left vertices and m right vertices is given by specifying which left and right vertices are "defects" (connected to eachother)

• left_defects : Finset (Fin n)
• right_defects : Finset (Fin m)
• consistant : self.left_defects.card = self.right_defects.card

theorem PlanarRook.Diagram.ext_iff {n m : ℕ} {x y : Diagram n m} : x = y ↔ x.left_defects = y.left_defects ∧ x.right_defects = y.right_defects

theorem PlanarRook.Diagram.ext {n m : ℕ} {x y : Diagram n m} (left_defects : x.left_defects = y.left_defects) (right_defects : x.right_defects = y.right_defects) : x = y

def PlanarRook.instDecidableEqDiagram.decEq {n✝ m✝ : ℕ} (x✝ x✝¹ : Diagram n✝ m✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

instance PlanarRook.instDecidableEqDiagram {n✝ m✝ : ℕ} : DecidableEq (Diagram n✝ m✝)

Equations

• PlanarRook.instDecidableEqDiagram = PlanarRook.instDecidableEqDiagram.decEq

def PlanarRook.Diagram.pi_iso {n m : ℕ} : Diagram n m ≃ (k : ℕ) × { S : Finset (Fin n) // S.card = k } × { S : Finset (Fin m) // S.card = k }

Equations

• One or more equations did not get rendered due to their size.

def PlanarRook.Diagram.pi_iso' {n m : ℕ} : (k : ℕ) × { S : Finset (Fin n) // S.card = k } × { S : Finset (Fin m) // S.card = k } ≃ (k : Fin (n + 1)) × { S : Finset (Fin n) // S.card = ↑k } × { S : Finset (Fin m) // S.card = ↑k }

Equations

• One or more equations did not get rendered due to their size.

def PlanarRook.Diagram.pi_iso₂ {n m : ℕ} : Diagram n m ≃ (k : Fin (n + 1)) × { S : Finset (Fin n) // S.card = ↑k } × { S : Finset (Fin m) // S.card = ↑k }

Equations

• PlanarRook.Diagram.pi_iso₂ = PlanarRook.Diagram.pi_iso.trans PlanarRook.Diagram.pi_iso'

instance PlanarRook.Diagram.instFinite {n m : ℕ} : Finite (Diagram n m)

instance PlanarRook.Diagram.instFintype {n m : ℕ} : Fintype (Diagram n m)

Equations

• PlanarRook.Diagram.instFintype = { elems := Finset.image PlanarRook.Diagram.pi_iso₂.invFun Finset.univ, complete := ⋯ }

Examples

def PlanarRook.Diagram.empty (n m : ℕ) : Diagram n m

The empty diagram has no defects

Equations

• PlanarRook.Diagram.empty n m = { left_defects := ∅, right_defects := ∅, consistant := PlanarRook.Diagram.empty._proof_1 }

def PlanarRook.Diagram.id (n : ℕ) : Diagram n n

The identity diagram has all vertices as defects

Equations

• PlanarRook.Diagram.id n = { left_defects := Finset.univ, right_defects := Finset.univ, consistant := ⋯ }

def PlanarRook.Diagram.example_1 : Diagram 4 5

This is the diagram

──────╮    ╾─
────╮ │    ╾─
─╼  │ ╰-─────
─╼  ╰-───────
           ╾─

Equations

• PlanarRook.Diagram.example_1 = { left_defects := {0, 2}, right_defects := {2, 3}, consistant := PlanarRook.Diagram.example_1._proof_3 }

def PlanarRook.Diagram.example_2 : Diagram 5 3

Equations

• PlanarRook.Diagram.example_2 = { left_defects := {0, 1}, right_defects := {1, 2}, consistant := PlanarRook.Diagram.example_2._proof_2 }

Through indices

A diagram has a "through-index": the number of defects on each side Diagrammatically, this is the number of lines connecting left and right vertices, or equivalently the number of rooks.

def PlanarRook.Diagram.through_index {n m : ℕ} (d : Diagram n m) : ℕ

The through index of a diagram is the size of its left (or right) defects.

Equations

• d.through_index = d.left_defects.card

def PlanarRook.Diagram.through_index_of_iso {n m : ℕ} (k : ℕ) (s₁ : { S : Finset (Fin n) // S.card = k }) (s₂ : { S : Finset (Fin m) // S.card = k }) : (pi_iso.symm ⟨k, (s₁, s₂)⟩).through_index = k

Equations

• ⋯ = ⋯

theorem PlanarRook.Diagram.through_index_eq_left {n m : ℕ} (d : Diagram n m) : d.through_index = d.left_defects.card

theorem PlanarRook.Diagram.through_index_eq_right {n m : ℕ} (d : Diagram n m) : d.through_index = d.right_defects.card

theorem PlanarRook.Diagram.through_index_le_left {n m : ℕ} (d : Diagram n m) : d.through_index ≤ n

Through indices are bounded by the size of the left defects.

theorem PlanarRook.Diagram.through_index_le_right {n m : ℕ} (d : Diagram n m) : d.through_index ≤ m

Through indices are bounded by the size of the right defects.

theorem PlanarRook.Diagram.through_index_of_id {n : ℕ} : (id n).through_index = n

theorem PlanarRook.Diagram.through_index_of_empty {n m : ℕ} : (empty n m).through_index = 0

Diagrams as partial bijections

def PlanarRook.Diagram.bijection {n m : ℕ} (d : Diagram n m) : ↥d.left_defects ≃o ↥d.right_defects

A diagram defines a bijection between left and right defects

Equations

• d.bijection = default

@[simp]

def PlanarRook.Diagram.bijection_of_id_is_id {n : ℕ} : (id n).bijection = OrderIso.refl ↥(id n).left_defects

Equations

• ⋯ = ⋯

def PlanarRook.Diagram.of_bijection {n m : ℕ} (left_defects : Finset (Fin n)) (right_defects : Finset (Fin m)) (bijection : ↥left_defects ≃o ↥right_defects) : Diagram n m

Equations

• PlanarRook.Diagram.of_bijection left_defects right_defects bijection = { left_defects := left_defects, right_defects := right_defects, consistant := ⋯ }

def PlanarRook.Diagram.bijection_of_bijection {n m : ℕ} (d : Diagram n m) : of_bijection d.left_defects d.right_defects d.bijection = d

Equations

• ⋯ = ⋯

def PlanarRook.Diagram.bijection_of_of_bijection {n m : ℕ} (left_defects : Finset (Fin n)) (right_defects : Finset (Fin m)) (bijection : ↥left_defects ≃o ↥right_defects) : (of_bijection left_defects right_defects bijection).bijection = bijection

Equations

• ⋯ = ⋯

def PlanarRook.Diagram.bijections_are_diagrams {n m : ℕ} : Diagram n m ≃ (left_defects : Finset (Fin n)) × (right_defects : Finset (Fin m)) × (↥left_defects ≃o ↥right_defects)

Equations

• One or more equations did not get rendered due to their size.

def PlanarRook.Diagram.act {n m : ℕ} (d : Diagram n m) (i : Fin n) : Option (Fin m)

Equations

• d.act i = if h : i ∈ d.left_defects then some ↑(d.bijection ⟨i, h⟩) else none

def PlanarRook.Diagram.act_of_id {n : ℕ} (i : Fin n) : (id n).act i = some i

Equations

• ⋯ = ⋯

def PlanarRook.Diagram.act_of_empty {n m : ℕ} (i : Fin n) : (empty n m).act i = none

Equations

• ⋯ = ⋯

Multiplication of diagrams

def PlanarRook.Diagram.mul {n m k : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) : Diagram n k

Equations

• One or more equations did not get rendered due to their size.

instance PlanarRook.Diagram.has_hmul {n m k : ℕ} : HMul (Diagram n m) (Diagram m k) (Diagram n k)

Equations

• PlanarRook.Diagram.has_hmul = { hMul := PlanarRook.Diagram.mul }

@[simp]

def PlanarRook.Diagram.hmul_left_defects {n m k : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) : (d₁ * d₂).left_defects = {x : Fin n | ∃ (h : x ∈ d₁.left_defects), ↑(d₁.bijection ⟨x, h⟩) ∈ d₂.left_defects}

Equations

• ⋯ = ⋯

@[simp]

def PlanarRook.Diagram.hmul_right_defects {n m k : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) : (d₁ * d₂).right_defects = {y : Fin k | ∃ (h : y ∈ d₂.right_defects), ↑(d₂.bijection.symm ⟨y, h⟩) ∈ d₁.right_defects}

Equations

• ⋯ = ⋯

@[simp]

def PlanarRook.Diagram.mul_id {n m : ℕ} (d : Diagram n m) : d * id m = d

Equations

• ⋯ = ⋯

@[simp]

def PlanarRook.Diagram.id_mul {n m : ℕ} (d : Diagram n m) : id n * d = d

Equations

• ⋯ = ⋯

Simple results about multiplication

def PlanarRook.Diagram.mul_left_of_right_arbitrary {n m k : ℕ} {d₁ : Diagram n m} (d₂ d₃ : Diagram m k) (h : d₂.left_defects = d₃.left_defects) : (d₁ * d₂).left_defects = (d₁ * d₃).left_defects

The left defects of a product do not change if you only change the right defects of the right factor.

Equations

• ⋯ = ⋯

def PlanarRook.Diagram.mul_right_subset {n m k : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) : (d₁ * d₂).right_defects ⊆ d₂.right_defects

Equations

• ⋯ = ⋯

def PlanarRook.Diagram.mul_left_subset {n m k : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) : (d₁ * d₂).left_defects ⊆ d₁.left_defects

Equations

• ⋯ = ⋯

Through degree of multiplication

theorem PlanarRook.Diagram.through_degree_of_mul {n m k : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) : (d₁ * d₂).through_index = (d₁.right_defects ∩ d₂.left_defects).card

theorem PlanarRook.Diagram.mul_not_increase_through_degree {n m k : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) : (d₁ * d₂).through_index ≤ min d₁.through_index d₂.through_index

Multiplication does not increase the through degree of either diagram.

def PlanarRook.Diagram.through_index_of_mul_independent_of_right {n m k : ℕ} (d₁ : Diagram n m) (d₂ d₃ : Diagram m k) (h : d₂.left_defects = d₃.left_defects) : (d₁ * d₂).through_index = (d₁ * d₃).through_index

Equations

• ⋯ = ⋯

Lemmata for proving associativity of multiplication

def PlanarRook.Diagram.restate_mul₃ {n m k : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) (x : ↥d₁.left_defects) (hxx : ↑(d₁.bijection x) ∈ d₂.left_defects) : ↑((d₁ * d₂).bijection ⟨↑x, ⋯⟩) = ↑(d₂.bijection ⟨↑(d₁.bijection x), hxx⟩)

Equations

• ⋯ = ⋯

def PlanarRook.Diagram.restate_mul₅ {n m k : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) (x : ↥d₂.right_defects) (hx : ↑(d₂.bijection.symm x) ∈ d₁.right_defects) : (d₁ * d₂).bijection.symm ⟨↑x, ⋯⟩ = ⟨↑(d₁.bijection.symm ⟨↑(d₂.bijection.symm x), hx⟩), ⋯⟩

Equations

• ⋯ = ⋯

Associativity of multiplication

def PlanarRook.Diagram.mul_assoc {n m k l : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) (d₃ : Diagram k l) : d₁ * d₂ * d₃ = d₁ * (d₂ * d₃)

Equations

• ⋯ = ⋯

The monoid of planar rook diagrams

We can now show that the planar rook diagrams with n vertices on each side form a monoid under multiplication.

instance PlanarRook.Monoid {n : ℕ} : _root_.Monoid (Diagram n n)

Equations

• PlanarRook.Monoid = { mul := HMul.hMul, mul_assoc := ⋯, one := PlanarRook.Diagram.id n, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

theorem PlanarRook.Monoid.one_def {n : ℕ} : 1 = Diagram.id n

The twist factor in the monoid

There is a natural number that arises when multiplying two diagrams, PlanarRook.Monoid.mul_exponent, which counts the number of disconnected components in the resulting diagram. This can be used when defining PlanarRook.Algebra to determine the "twist": the power of δ that appears. Here we collate some results about this number.

def PlanarRook.Monoid.mul_exponent {n m k : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) : ℕ

Equations

• PlanarRook.Monoid.mul_exponent d₁ d₂ = (d₁.right_defects ∪ d₂.left_defects)ᶜ.card

theorem PlanarRook.Monoid.mul_exponent' {n m k : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) : ↑(mul_exponent d₁ d₂) = ↑m - ↑d₁.through_index - ↑d₂.through_index + ↑(d₁ * d₂).through_index

def PlanarRook.Monoid.mul_exponent_eq_zero_of_id {n m : ℕ} (d : Diagram n m) : mul_exponent d (Diagram.id m) = 0

The identity diagram invokes zero twist when multiplied on the right.

Equations

• ⋯ = ⋯

def PlanarRook.Monoid.mul_exponent_eq_zero_of_id' {n m : ℕ} (d : Diagram n m) : mul_exponent (Diagram.id n) d = 0

The identity diagram invokes zero twist when multiplied on the left.

Equations

• ⋯ = ⋯

def PlanarRook.Monoid.mul_exponent_assoc' {n m k l : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) (d₃ : Diagram k l) : ↑(mul_exponent d₁ d₂) + ↑(mul_exponent (d₁ * d₂) d₃) = ↑(mul_exponent d₁ (d₂ * d₃)) + ↑(mul_exponent d₂ d₃)

The twist is additive over associated multipliation as an integer.

Equations

• ⋯ = ⋯

def PlanarRook.Monoid.mul_exponent_ge_zero {n m k : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) : 0 ≤ mul_exponent d₁ d₂

The twist is non-negative.

Equations

• ⋯ = ⋯

def PlanarRook.Monoid.mul_exponent_assoc {n m k l : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) (d₃ : Diagram k l) : mul_exponent d₁ d₂ + mul_exponent (d₁ * d₂) d₃ = mul_exponent d₁ (d₂ * d₃) + mul_exponent d₂ d₃

The twist is additive over associated multiplication as a natural number.

Equations

• ⋯ = ⋯

def PlanarRook.Monoid.mul_exponent_of_right_arbitrary {n m k : ℕ} (d₁ : Diagram n m) (d₂ d₃ : Diagram m k) (h₁ : d₂.left_defects = d₃.left_defects) : mul_exponent d₁ d₂ = mul_exponent d₁ d₃

Equations

• ⋯ = ⋯

The monoid involution

There is a natural involution on diagrams, given by reflecting them across the vertical axis. This sends left defects to right defects and vice versa, and reverses the order of multiplication.

def PlanarRook.Diagram.ι {n m : ℕ} : Diagram n m → Diagram m n

Equations

• d.ι = { left_defects := d.right_defects, right_defects := d.left_defects, consistant := ⋯ }

def PlanarRook.Diagram.ι_involutive {n m : ℕ} (d : Diagram n m) : d.ι.ι = d

Equations

• ⋯ = ⋯

def PlanarRook.Diagram.ι_Involutive {n : ℕ} : Function.Involutive ι

Equations

• ⋯ = ⋯

def PlanarRook.Diagram.ι_bijection {n m : ℕ} (d : Diagram n m) : d.ι.bijection = d.bijection.symm

Equations

• ⋯ = ⋯

def PlanarRook.Diagram.ι_mul {n m k : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) : (d₁ * d₂).ι = d₂.ι * d₁.ι

The involution reverses the order of multiplication.

Equations

• ⋯ = ⋯

theorem PlanarRook.Monoid.ι_through_index {n m : ℕ} (d : Diagram n m) : d.ι.through_index = d.through_index

The involution preserves the through index.

@[simp]

theorem PlanarRook.Monoid.mul_exponent_of_ι {n m k : ℕ} (d₁ : Diagram n m) (d₂ : Diagram m k) : mul_exponent d₂.ι d₁.ι = mul_exponent d₁ d₂

The involution preserves the multiplication exponent.

def PlanarRook.Diagram.ι_of_iso {n m : ℕ} (k : ℕ) (s₁ : { S : Finset (Fin n) // S.card = k }) (s₂ : { S : Finset (Fin m) // S.card = k }) : (pi_iso.symm ⟨k, (s₁, s₂)⟩).ι = pi_iso.symm ⟨k, (s₂, s₁)⟩

Equations

• ⋯ = ⋯

def PlanarRook.Diagram.ι_of_iso₂ {n : ℕ} (k : Fin (n + 1)) (s₁ s₂ : { S : Finset (Fin n) // S.card = ↑k }) : (pi_iso.symm ⟨↑k, (s₁, s₂)⟩).ι = pi_iso₂.symm ⟨k, (s₂, s₁)⟩

Equations

• ⋯ = ⋯